Qiancheng Fu
Qiancheng Fu
When working with long files (over 1500 lines of code), I often encounter instances where vscoq refuses to step through the proof. Neither stepping one line at a time nor...
When using ocamlformat under emacs, a buffer pops up very often saying the following ``` ocamlformat errors: ocamlformat: SRC… arguments: no '117-117' file Usage: ocamlformat [OPTION]… [SRC]… Try 'ocamlformat --help'...
### What did you expect to happen? After pressing the spacebar, I expect a simple whitespace character typed to the file, nothing more, nothing less. ### What actually happened? After...
Is there any way to stop smlfmt from formatting comments? In particular, if I write a comment at the end of a file, it always gets formatted to occupy a...
I have been running into an issue with the goal display of the vscode client that's a bit annoying. The display for big case analysis does not collapse when entering...
I was trying to follow the examples shown in https://github.com/andreasabel/strong-normalization/tree/master/coq/well-scoped When trying to compile the examples, in reduction.v, coq reports that is does not know how to interpret notation `(_[_])`....
Using vscoq's interpret to point command, the current line of proof that the cursor is on is not interpreted. This causes a bit of inconvenience when using with the vscode...