Ramkumar Ramachandra

Results 54 comments of 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?