Visual Studio Code Extension and Language Server Protocol for Coq
License: GNU Lesser General Public License v2.1
I work on making interactive theorem provers easier to use, with a particular interest in using state-of-the-art progamming language techniques to facilitate HCI and ML research! See my personal page for more information about me and my projects.
Don't hesitate to get in touch with me via Coq's Zulip! Have fun hacking!
My usual pronoums are he/him/él tho I'm very happy to be addressed by other pronoums too.
![dependabot[bot] avatar](https://avatars.githubusercontent.com/in/29110?v=4 "dependabot[bot]")
For example, (Query (TypeOf "S")) returns the correct result, however (Query (TypeOf "S O")) results in the error (CErrors.UserError ("" "Invalid character ' ' in identifier \"S O\".")))
The idea is to allow users to delay proof checking, and do so only under demand, for example when clicking a gutter.
There are many heuristics involved here, for example we could schedule for checking the proofs that are in view, but we need #49 and LSP 3.18 for that to be implemented relialby.
For now, we can start implementing the infrastructure to do so. The idea was that actually Coq upstream API would allow clients to re-implement vernacinterp, upstream diverged a bit on that matter, but I think we can still proceed with the original plan.
Implement the basic workspace panel for code
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 coq/coq#17760
Problems with the current venacular API (c.f. failures in coq/coq#16190 )
This is a complex issue regarding Coq's API; we have been working for 4 years on it. I hope to make a CEP / more complete status report when we can; some easier sub-tasks:
An instance of the previous problem is that could have certain commands (such as Search / Query) be really read-only on the state, as to have the cache work for them.
Lack of metadata in .vo files (c.f. coq/coq#16484)
This makes many things just as jump to definition impossible. A working proposal exists in the above PR.
There are some users of Loc.make_loc which creates bogus locations, we must fix that and remove all users.
This issue is critical and affects all IDEs, it means that supporting multiple documents in a single server or removing a Require is not going to work well as we will eventually get conflicts.
Likely related coq/coq#10146
The client on the store does not seem to work. I have coq-lsp in my PATH but restarting it in VSCode gives:
Something seems to be missing. @ejgallego
In order to try the repair code feature, we can suggest users two hints for Qed / Admitted proofs:
Admitted.Admitted, suggest switching it to Qed.Whether having Admitted upstream is a good thing, I don't know.
We have a few choices on what to do here. ocaml-lsp also has integration with Dune, for example watch builds (which are RPC) can be viewed.
Newer LSP versions allow us to provide hierarchical information about symbols.
This requires that we store the document structure in Doc.t, which is a 0.2 milestone.
Code completion gives suggestions about what the user might want to type. We need to investigate groups of objects and priorities.
Our current approach w.r.t. threading / interruptions is likely not working on Windows; we first need someone interested in helping us fix that.
This issue is for tracking the integration of coq-layout-engine into coq-lsp.
coq-layout-engine ?coq-layout-engine is a new printer for Coq documents that targets a box model similar to the one of LaTeX or the DOM, with a focus on this last media. The idea of printing Coq terms in a different format appeared early in the jsCoq development, but only until recently we figured out the right way we'd like to proceed.
The early wishes for a different goal rendering system arose early in the development of jsCoq as to do some "point and click" proving. Moreover, there are many common use cases, for example, linking identifiers to their location, unfolding notations on the go, displaying implicit arguments, outputting to TeX, etc...
While many of these issues can be solved by other means, including this information in a rich printer setting seems to work pretty well. Isabelle realized about this quite some time ago, and they use what is called, "Semantic Printing". Unfortunately Coq current printer doesn't preserve the required structure.
An overview of the issues and first implementation effort was given in a talk at IRIF in Oct 2021, see the slides , the corresponding code is at jscoq/jscoq#28
Thus, coq-layout-engine is very similar in spirit to Isabelle's printer, but using a different tech stack, in particular, we output to something very close to HTML / Web Components.
For the last year, the development of coq-layout-engine has been waiting for coq-lsp and jsCoq to modernize other parts of their stack, but we are reaching a point where we can experiment a bit more. The current TODO list is:
Pp.t printer and test-suite in jsCoq (and port to vsCode ongoing in ejgallego/coq-serapi#143Since the inception of SerAPI providing a way to query dependency data was a goal. In fact, this is possible to do now by clients and you can dump the actual proof term in sexp format and then perform the analysis yourself.
However, the very nice work on regression testing coq/coq#9262 could indeed benefit from having specific support for dependency data. In particular, we may want to provide two calls:
(Query opts (Deps id)) : Output dependencies of identified id,(Query opts (Digest id)): Output digest of id's body,(Query opts (RangeDigest range)): Output digest + deps for identifiers in a document range [in icoq style]The interface for updating a prior proof is not clear yet, but likely the easiest for now is to piggyback on the .vio interface.
There are many open questions about how to better do this, a start will be to embed the dep-tracking computation of https://github.com/Karmaki/coq-dpdgraph , and implement 1 and 2 so we can start experimenting.
cc: @palmskog
We want to handle this case:
Proof.
tac1, tacn
Qed.
Better, so we just don't skip to dot, but can detect the Qed and be smarter here.
Note the lack of doc after tacn
This is a follow up of #100 , in particular, to optimize the request queue when a new document version is submitted. In particular, we should:
process_input, check if the incoming request is a new version for a documentrequest_queue all requests referring to the old version of the documentThis is a pretty minor optimization for now (we serve all request quite fast), so not urgent to do.
Changes at #99 implement a sane queue handling, but it is still very unoptimized, in particular:
What to do in the previous case is not easy, but as these request have a document position, I think that actually the most sane thing to do for now is to actually check if checking has reached the requested position, and otherwise cancel / postpone.
Hey @ejgallego,
How hard would it be to expose parent-child relationships between goals in the API? At the moment SerAPI prints less information than coqtop -emacs (the latter has a unique ID for each goal, printed after the goal number in PG, which is robust to things like cycling goals, etc), but even the information that coqtop -emacs contains isn't sufficient when a command affects multiple goals.
Here are some benchmarks:
Axiom P111 P112 P113 P121 P211 : Prop.
Axiom magic: forall {A}, A.
Goal ((P111 /\ P112 /\ P113) /\ P121) /\ P211.
split.
- split.
+ repeat split.
* refine ?[G111]. exact magic.
* refine ?[G112]. exact magic.
* refine ?[G113]. exact magic.
+ refine ?[G121]. exact magic.
- refine ?[G211]. exact magic.
Qed.
Goal ((P111 /\ P112 /\ P113) /\ P121) /\ P211.
split.
split.
repeat split.
refine ?[G111]. exact magic.
refine ?[G112]. exact magic.
refine ?[G113]. exact magic.
refine ?[G121]. exact magic.
refine ?[G211]. exact magic.
Qed.
Goal (P111 /\ P112 /\ P113) /\ (P121 /\ P211).
split.
all: cycle 1; repeat split.
all: cycle 1.
all: exact magic.
Qed.
I think we can already handle most of these as long as there are no reorderings, but things break as soon as there's a cycle command. Exposing Coqtop's goal IDs would partly fix the problem, but it wouldn't help with things like all: split.
In all these cases we'd like to generate the same proof tree; ideally that would be done by adding a unique id to each goal and unique parent field pointing to that goal's parent.
CC @hendriktews; Hendrik (hi!), how do you handle commands like all: split in prooftree?
Begin using the LSP bindings ready made in the ocaml-lsp project.
Diagnostics should be pulled on demand rather than all given at once.
Unlikely to solve general performance issues around them however.
Problems with current setup:
ok_diagnosticsIf we get an anomaly from Fleche (usually from Coq), the way the server behaves is far from ideal.
We are also not very well protected for exceptions happening in the request code.
This is a frequent request by for example @cpitclaudel or @JasonGross ; I already have something in my document manager implementation that does exactly this [so incremental checking can have something a bit better than a linear domain for the DAG]
I will extract it out to a library and expose it in SerAPI / pyCoq.
This will require libobject changes that @ejgallego was working on upstream in Coq. Should be straight forward to implement afterwards.
Hi! Is there a way to get sexp-formatted information about modules, like the one acquired by running Print Coq.Init.Datatypes in Vernac? I failed to find a way, and running several commands like (Query () (Definition Coq.Init.Datatypes)) yielded no results.
Right now, the code for search reads:
| Search -> [CoqString "Not Implemented"]
Names provides a very restricted subset of Search, however we should unify
A question is what kind of object we'd like to return from Search, right now we just return names, but certainly a richer information would be appreciated.
Merlin has its own LSP libraries, we should indeed share the code at some point.
Current goal printing is very basic and doesn't look good at all; in particular we didn't set indentation and margins on, also there is no coloring.
Best way to fix this is to use jsCoq's Pp.t -> Html routine (https://github.com/jscoq/jscoq/blob/2a60fd083b6b09cbe19f750f31a877740d140ea2/frontend/classic/js/format-pprint.js) , which is well-tested and provides some nice features.
Hi,
I would like to be able to print a given input sentence with the notation interpreted, all arguments explicit, and the scopes resolved by Coq's internalization process.
For example, after inputting (Add () "Lemma test: forall n:nat, n = n. Proof. assert (H: forall n, n + 0 = n).") and executing it, applying some query command to the sentence assert (H: forall n, n + 0 = n). would return assert (H : forall (n:nat), @eq nat (Nat.add n O) n).
(and nat would instead be Coq.Init.Datatypes.nat, Nat.add would be Coq.Init.Nat.add, etc.)
Since the beginning, the manual override / re-export of Coq's type using ppx_import has been done manually [with the help of some hacky scripting]. It was planned to use a more methodical method in the future.
It turns out such as solution by @thierry-martinez exists, https://github.com/thierry-martinez/override should allow for a much more compact derivation of serializes for Coq's types.
@artagnon had the idea of improving parsing error messages; this seems mostly upstream work. The originating example was this failing code from Bonak:
- now exact mkNTypeSn
Defined.which produces the error Syntax error: [ltac_use_default] expected after [tactic] (in [tactic_command]). for the range of Defined.
Indeed, for example in this case, the error could point to the user that Defined was not expected and instead they should use ltac_use_default which as of today is (from fullGrammar Coq's upstream file):
ltac_use_default: [
| "."
| "..."
]
that is to say, a dot set was expected.
As of today, most Coq parsing errors arise from the Gramlib parsing library (gramlib/grammar.ml) usually raising Gramlib.Stream.Error msg where msg is a string.
For the above error, the message is built in the gramlib/grammar.ml:tree_failed function.
Isabelle is able to check on editor scroll, including not checking the proofs that are not in view.
Still, skipping Qed. proofs that are not in view remains a TODO.
Newer LSP protocol versions allow us to provide much better metadata on symbols, such as range, types, etc...
Hi Emilio,
Hope you're doing OK despite the crazy times.
In the project I'm workig on, it would be very useful to be able to get comments boundaries in addition to code fragments; like this:
("query0" (Add () "Goal True.\n (* R1 *) (** D1 **) idtac. (* R2 *)"))
(Answer query0 Ack)
(Answer query0(Added 2((fname ToplevelInput)(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 0)(ep 10))NewTip))
(Answer query0(Added 3((fname ToplevelInput)(line_nb 2)(bol_pos 11)(line_nb_last 2)(bol_pos_last 11)(bp 34)(ep 40))NewTip))
(Answer query0 Completed)
It would be great if instead of two spans (0-10, 34-40), SerAPI could return 5: Goal True., (* R1 *), (** D1 **), idtac., (* R2 *).
Currently I have a mini-parser that I use after passing things through SerAPI, to detect comment boundaries.
WDYT?
Thanks!
Hi Emilio.
This is a follow up to coq/coq#4834 (comment) (thanks for the quick response!)
One thing Alectryon is missing compared to coqdoc is hyperlinking abilities. I'd like to (1) be able to link to definitions that appear in Alectryon blocks and (2) be able to link to documentation generated by coqdoc. To support this, I think I need to support two scenarios:
I have a bit of input code: Definition x := 1.; I need to realize that this defines the symbol MyFile.x (in turn this probably means that I need to pass SerAPI a -topname?
I have a bit of input code (Goal 1 + 1 = 2.) or a bit of output (1 + 1 = 2, part of a SerAPI Goal); I need to realize that "+" is Coq.Init.Nat.add.
I can almost get this information with SerAPI If I ask for CoqSer output (it gives me fully qualified names, which is great). But CoqSer results don't include info on notations, so I can't produce pretty-printed hyperlinked output with that.
There's also CoqPp output, and there the Pp_tags that say things like "notation". But there are no tags for FQNs.
Maybe we could have a separate mode that returns CoqPp structures with meta information in new Pp_Tags? (But then I'd have to reimplement the box layout algorithm on my side). Or maybe we could return meta info for spans of formatted output (but that might tricky to implement?). Or maybe there's something completely different that I didn't think of?
Going the annotated Pp_tag route means that we can also include stuff like syntax-highliting information with the same mechanism at a future point, which would be pretty sweet.
Looping in @Ptival who has stuff like this working on top of jsCoq in his cool online demo in the past.
Hope you're doing well!
Clément.
In my work-in-progress proof explorer GUI, I currently display diffs of goals by doing a diff on their string representations. It would be better to diff the term structure - which I'm assuming is something that other tools could benefit from as well, so it would be logical to provide that feature on the SerAPI end rather than having tools do their own ad-hoc approaches.
As witnessed by ejgallego/coq-serapi#68, we have a very important problem with the current situation of generic arguments in Coq. As of today, we need to add manually the serializers, which is cumbersome, and worse, won't fail until we find a generic argument we cannot handle.
Ideally we should add some support in Coq to notify SerAPI that a new generic argument has been defined, then SerAPI could look up its internal serializer table and register it.
Even better, it would be good if coqpp could generate some kind of boilerplate thus that we could be spared from writing the serializers manually, but this may have to wait for ppx_serlib to be ready tho.
All the "foo is defined" messages should not be displayed by default, that is too noisy; turn it into a server option.
Some sort of progress bar report, or status indicating checked build. We need to investigate what support in LSP there already is for this.
so we cover at least the stdlib plugins
Resumption from the interruption case seems to be working pretty well.
However, for document update, we just restart from the beginning. This can be improved by actually finding a common prefix.
The original idea was to memoize parsing (see #36 and #25 ), however, at least in the current implementation, a much simpler computation of a common prefix would bring the same benefits AFAICS.
We would like to have binary builds [at least for Windows] so coq-lsp can be installed from the market easily. A possible roadmap would be to use Github Actions on Windows.
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.