dunham

29 ms·

391.
by dunham 4y ago
I took a quick look at the github repository (because I'm on macos), and it looks like it is written in javascript (and xml) using "gjs", which exposes the gnome libraries to javascript. So I think it's a gtk/gnome
392.
by dunham 4y ago
Wow, I'd somehow never noticed that. I've just been looking at profile -> comments whenever the number in the top right corner changed.
393.
by dunham 4y ago
Yup, I got some nice documentation (minor syntax error) for a Http package in Lean that doesn't exist. I asked about Lean4 and it helpfully explained that the non-existent package had moved from Lean to Std.
394.
by dunham 4y ago
I did advent of code in Lean4 in 2022 and Idris2 in 2021. Lean4 was fairly similar to Idris code-wise. Minor differences: - On the Lean side I leveraged the fact that Arrays can mutate in place (if the refcount is 1). For Idris I'd us
395.
by dunham 4y ago
Also "Wingman" for Haskell does some type-driven code generation. (It might be part of the haskell language server now, I get it when I use the vscode plugin.) When the solution is ambiguous, Idris (and I believe wingman) will sup
396.
by dunham 4y ago
For what it's worth, last I checked (Nov 2021) the image was rendered client side. They send a collection of glyphs as SVG strings like "M31.9824,43.9453 L364.014,-719.971 L495.117,-719.971 L163.086,43.9453 L31.9824,43.9453
397.
by dunham 4y ago
Thanks, I'll take a look. I just now discovered that Noto Sans Mono has some math coverage. Ok yeah, at 11k glyphs, that's quite a font. I'm liking it - things like ⊎ are much more legible.
398.
by dunham 4y ago
Nice, I've been looking for a way to see what the math symbol coverage is for various fonts. (For writing Agda/Lean code.) The web page seems to hang a while for some fonts (e.g. JetBrainsMono-Regular), long enough to get a warnin
399.
by dunham 4y ago
Could be, but that's my recollection of the situation. I had added -ffloat-store on the Linux side, and I had read somewhere that was being done on the osx side. Note that this was back in January of 2011, possibly earlier. Back then g
400.
by dunham 4y ago
I had one issue where pdftotext would produce different output on different machines (Linux vs Mac). It broke some of our tests. I tracked down where it was happening (involving an ==), but it magically stopped when I added print statement
401.
by dunham 4y ago
My favorite is from Bob Atkey's Quantitative Type Theory paper: > This work is dedicated to Orwell the dog. Orwell was a good dog and knew well the difference between zero, one, and many https://bentnib.org/quantitat
402.
by dunham 4y ago
Yeah I do that a lot. And on macos, vi decides that :Wq is an error and returns a non-zero status code on my subsequent :wq, cancelling my git commit. So I get to type the commit message again.
403.
by dunham 4y ago
As I implied, I find the Haskell-like languages attractive. To the point that I am taking that approach in a toy language. But you are right, the cost of it is pretty high - not just copy/paste, but it's tricky to parse, auto-form
404.
by dunham 4y ago
This is why I like the underscores, it's easier for me to see the typo in: quota = 1000_000_000 than it is in: quota = 1000000000 And also when I'm typing the number, it's easier for me to be sure I got it r
405.
by dunham 4y ago
For Java, I used to write `list = yourFunctionReturningThatSet();` and then have the IDE fill in the type when it complains about the undefined variable.
406.
by dunham 4y ago
Agda does, but it also supports a plain ascii hyphen in identifiers. It allows operator characters inside identifiers and requires spaces around operators otherwise (as proposed in the article). So you can use x-y as an identifier: x-
407.
by dunham 4y ago
> Somewhat surprisngly, indentation-sensitivity in languages like Python and Haskell had me writing cleaner-looking and more readable code by default. Yeah, I've gone from hating this, to accepting it (after using Python), to wantin
408.
by dunham 4y ago
I did this with my CDs and books while making room for a nursery. But I regret getting rid of the hard-cover SICP. I have a PDF, but would like the book again and it no longer exists in hard cover.
409.
by dunham 4y ago
Do you have any further information on whether the USDA still intends to do something about this?
410.
by dunham 4y ago
I have no idea what features are "anti-user", but I would note that it is not free for commercial use. I'm paying for Obsidian sync and still can't use Obsidian for work. (At the moment, I'm using logseq there.) ht
411.
by dunham 4y ago
Which instance was a tricky point for me. And then suddenly one of my options wasn't accepting new members (turned out to be temporary). I now have an account that I'm not using on an instance that is semi-blocked by other instanc
412.
by dunham 4y ago
Also, a draft of book itself was used for the 2022 summer school: https://github.com/martinescardo/HoTTEST-Summer-School/tree/... https://www.uwo.ca/math/faculty/kapulkin/semina
413.
by dunham 4y ago
I've been doing advent of code in Lean this year. It's been fun, but yeah the documentation is still a WIP. I've been searching the lean code base (I leave it in a separate editor window) and Zulip to figure out how to do st
414.
by dunham 4y ago
Also https://flow.org/
415.
by dunham 4y ago
You can stick "partial" in front of a function definition if you want to live dangerously. I've had to do that in a couple of spots in my Advent of Code stuff.
416.
by dunham 4y ago
On iPad "secure shellfish" can do this over an ssh connection. You can grab a file out of an "ls" listing and drag it to another app. (You do have to highlight the name first, so not quite as ergonomic as iTerm.)
417.
by dunham 4y ago
Yeah, I've known and used "vi" for a couple of decades, saw someone use visual mode in a video a few months ago, and it blew my mind. I still don't know how to do project navigation in vi, as I mainly use it for editing
418.
by dunham 4y ago
I am curious whether it could pick GPT3 out of the crowd.
419.
by dunham 4y ago
> Is there any communities for programming language developers? Where do all the language developers meet up and talk theory and implementation? I am on eatonphil's discord and we talk there. There is a discord for that: https:&#x2
420.
by dunham 4y ago
Ahh, I’d played browser years ago and mobile more recently. I assumed it was a feature added since my browser play through.

More ›