Emilio Jesús Gallego Arias
Emilio Jesús Gallego Arias
It makes a lot more sense for us to develop `serlib` natively here, as we need new exclusive functionalities and the submodules are not bringing us a lot. I guess...
It seems that the image we used in the demo may not be free for us to even include here. Let's resolve this by using a free image.
Stats seem a bit mixed, more research is needed. We will improve the analysis shortly, for now we do two kind of analysis: - on hover, we print the number...
For now we just host the code here, and compile it. We will add the selection method later on. CC: #72 Replaces: https://github.com/jscoq/jscoq/pull/282
This issue tries to track upstream Coq issues that are affecting coq-lsp. The order is from most critical to less critical. - Problems with managing `memprof-limits` exns https://github.com/coq/coq/issues/17760 - Problems...
As of today we are not handling the proof mode for parsing safely, current code does: ```ocaml let mode ~st = Option.map (fun _ -> Synterp.get_default_proof_mode ()) st.Vernacstate.interp.lemmas ``` which...
See https://github.com/ejgallego/coq-lsp/pull/698
The `abstract` tactic is a notorious example of incomplete functionality in the Coq system. The tactic itself doesn't work in many contexts, and indeed this fact is not properly documented...
We have some expect Coq tests that produce output, the output will include backtrace information the flag is set in the runtime. These tests live under the runtest alias, together...