ratmice

13 ms·

121.
by ratmice 4y ago
It looks like gitea supports running a proc_receive hook which can be used to implement pull requests over git:// using a client like https://git-repo.info/en/ (full disclosure) I had written a proof of conce
122.
by ratmice 4y ago
The first thing that came to mind for slowly increasing worth looking into seemed like it might be the inverse ackermann function, which curiously I didn't find any OEIS entry for.
123.
by ratmice 4y ago
presumably https://developer.apple.com/documentation/coregraphics/cgwin...
124.
by ratmice 4y ago
> require extra compilation steps like practically every LR parser generator. It is worth noting that the author's lrpar tool (linked in the article) doesn't actually require extra compilation steps or code generation. This pe
125.
by ratmice 4y ago
I've hit this warning a few times where I expect to add additional match arms to be added in the future, always bugs me that clippy in that case steers you towards some change you know you'll end up undoing.
126.
by ratmice 4y ago
only if you intend to run the program though, if you want to just read the source code, perhaps to see if it contains malicious code you really don't want your editor doing such things by default, so something has to give.
127.
by ratmice 4y ago
With rust quite often (e.g. if you are running rust_analyzer) it will run `cargo check`, to produce errors. When `cargo check` is run, build.rs compiled and run. So quite often by step 1, just opening the file in your editor before even mak
128.
by ratmice 4y ago
The gnu coding standards has this to say: https://www.gnu.org/prep/standards/standards.html#index-beha... Please don’t make the behavior of a utility depend on the name used to invoke it. It is useful sometimes to
129.
by ratmice 4y ago
I have always done the opposite using SML/NJ's CompilationManager, then deriving mlb with cm2mlb -D MLton (in the mlton repo), with mlton specific code then wrapped in #if (defined(MLton)). That you can use CM as a library has alw
130.
by ratmice 4y ago
I'm not familiar with chrome debug protocol adaptor, I kind of assume it is not the same thing as https://microsoft.github.io/debug-adapter-protocol/ In the case that it is, I noticed that tromey had posted some
131.
by ratmice 4y ago
Nice writeup, been a while since I had used coq, it was nice to try and work it out from memory, but be able to refer back to your post when I got stuck. Also threw together a tiny lean proof without tactics, figured i would post a link to
132.
by ratmice 4y ago
looks exactly like U+29A2 https://en.wikipedia.org/wiki/Miscellaneous_Mathematical_Sym... Turned angle to me
133.
by ratmice 4y ago
There is also Levy's book https://homes.cs.washington.edu/~levy/capabook/
134.
by ratmice 4y ago
The simple fix for this is that you should use "```math render" or some such, the language is specified as the first word with everything after the space up to the newline currently ignored...
135.
by ratmice 4y ago
No it is when you know the size during runtime, or at time of construction. there is a 3rd class for constant strings known at compile time but it is mostly hidden behind @"" compiler syntax.
136.
by ratmice 4y ago
Hearsay, but I've read in the past that these were tailored specifically to the display, so difficult to actually collaborate since each display is a little different.
137.
by ratmice 5y ago
I believe I have seen it used as a symbol which indicates the discharge of an assumption, but never for "not".
138.
by ratmice 5y ago
Aircraft is a vastly different problem at a much smaller scale. Where did our ground traffic controllers go?
139.
by ratmice 5y ago
Standard Meta Language actually... for the origins of the name probably see the paper 'A metalanguage for interactive proof in LCF*'
140.
by ratmice 5y ago
I always wondered to what extent aphantasia affects mundane tasks, like setting something down, turning out the lights and picking it back up in the dark. I always seem to use a mental image of the thing in the space where I left it.
141.
by ratmice 5y ago
Yes, take a glass of water and fill your mouth, pretend to be a fountain spitting a stream of water, and breath through your nose. That is how I was tought to learn it anyways.
142.
by ratmice 5y ago
While you are technically correct, ldd is literally a bash script which runs ld-linux.so...
143.
by ratmice 5y ago
It seems strange not a mention of Darlingtonia californica (cobra lily), which also grows in the PNW albeit further south, but still not exotic and tropical.
144.
by ratmice 6y ago
I figure it can't hurt to also mention the Coq/software foundations style separation logic book. In it you build a sequential separation logic, and prove some properties such as soundness (rather than a concurrent separation logi
145.
by ratmice 6y ago
From this year I really liked the paper, Recovering Purity with Comonads and Capabilities, Vikraman Chaudhury and Neel Krishnaswami, https://arxiv.org/abs/1907.07283
146.
by ratmice 6y ago
I think the extra power comes with cognitive overhead, I.e. operators are now relative to some module, and you're stuck with that overhead whether or not you actually use the power or not. Trying to stay neutral, I think its no suprise
147.
by ratmice 6y ago
Seems like it, but typeclasses are inherently anti-modular, they provide a globally coherent unique instance. consider the Ord typeclass giving a single ordering for a specific type. To reverse the order you need to create a new type with a
148.
by ratmice 6y ago
yeah, that svn->git conversion was a one-time thing, and not fully kept in sync automatically. A bit unfortunate as recent releases have fixed one of the main for smlnj/reasons to use other compilers in that it now supports x86-64.
149.
by ratmice 6y ago
GDB has had that in the form of Multi-process debugging for a while. Multi-target I believe extends this different remote stubs and architectures, such as debugging both an x86 and x86-64 process. Besides that I agree it's really usef
150.
by ratmice 6y ago
ASLR doesn't prevent you from guessing, it merely makes it more difficult to guess. In general you could force the usage of any memory safe language. Here, In this paper they used/reference something call CARAT, Compiler and Runti

More ›