Ramkumar Ramachandra
Ramkumar Ramachandra
Yep, we should do exactly that, I think.
Yeah, I have to get rid of those error messages. In the meantime, just open another terminal, browse to the mountp/ directory, and start using it. The .git/ directory should...
Thanks for the report. I can reproduce this: it consistently crashes when there are more than 19 files in a single directory. I'm looking deeper into the problem.
Some of these questions are still open, because we have to figure out how to garbage collect using the `gc.statepoint` mechanism in LLVM; that requires gc'able (malloc'ed) pointer to be...
Does anyone have any insight on this one? The server code is much too hairy to debug, and I hope the DocumentManger fixes this.
I've never used CoqIDE, so I might be wrong about this, but is "extension.coq.interpretToEnd" the command you're looking for?
As far as I know, there are no build commands available in VSCoq. I personally just hit `make` or `dune build` in the integrated terminal in VSCode.
Can someone explain to me why this is a good idea? webpack adds extra bloat, along with a build-step. What does it buy us?
Nice. It's good for performance then.
I'm not sure, but for people with format-on-save toggled on (like me), this would be a good addition, yes?