-
Notifications
You must be signed in to change notification settings - Fork 74
The VsCoq VsRocq roadmap 2024 2025
Its the start of the academic year and we thought we would kick it off with writing a roadmap for VsCoq.
Note that the features / issues highlighted in this document are those we guarantee we will tackle in the coming year. It is not an exhaustive list.
VsCoq aims to make programming in Coq easy, efficient and rock solid by:
- helping core users to optimize their workflows
- helping teachers build better learning tools for their students
- helping students to get started in the world of Coq
The main focus of the year 2023/2024 was to bring VsCoq to a "stable" state and with a VsCoq Legacy feature parity. We estimate this task is around 70-80% complete. The biggest blocking bugs have been resolved, most of the features of VsCoq Legacy are back and we even have a host of new features. This puts us in a place where we can start thinking about what's next in terms of features.
We categorize the improvements to VsCoq that we wish to focus on in the following broad themes.
This includes anything pertaining to the editor functions of our extension. Things such as:
- automatic formatting
- of formulas (e.g. statements)
- of tactics (e.g. indentation/bulleting, linearization of compound ltac expressions)
- better syntax coloration
- given by the language server, not by an approximated grammar on the editor side
- code actions (e.g symbol renaming)
- inspection
- jump to definition
- docstrings
But also improving the build system to have a watch feature, etc...
The goal view is in a stable enough state that we can start thinking of interactive actions from the goal view.
- Hover on goal view terms to inspect them
- Click on actions (operate a tactic on a sub term, etc..)
- Optimization -> We can always aim at making Pretty printing faster
- Fancy notations (mathjax)
VsCoq introduces the concept of a query panel. This is suited to a more traditional Search function in which a search is global. Coq does not work this way and a Query is typically tied to a file and execution state.
In the coming year we plan to improve upon both of these ideas:
- A more local query system tied to the goal view and only searches in the context of the displayed goal(s)
- A more global approach which searches the entire project (not only in the
Requirefiles, also inide docstrings, ...)
The subject of onboarding is extremely pertinent to VsCoq. This covers two broad areas:
- A one click install experience, dependant on the coq platform
- A better access to documentation and tutorials
- Ability to run in the browser (e.g. vscode.dev)
These are used to qualify changes that will impact the user but not in a direct way (code re-architecture, optimisations)
| Mark | Description |
|---|---|
| ⭐ | Priority |
| 🐓 | Requires changes in Coq |
| 🏃 | Stretch goal |
| [ ] | WIP |
| [x] | DONE |
- Fixing most of the remaining bugs ⭐
- Having a formatter (248, 247) ⭐
- Handling syntaxic coloring in the server (578)
- Preliminary build watch feature: notify when a dependency has changed and offer him to reload (768) ⭐
- Proper watch system with dynamic registration of errors in workspace (follows from above) 🐓
- Compile before require (252)
- Proof of concept for doc strings on hover(990):star:
- Proper doc string system 🐓
- Better outline / Folding ranges (799, 137) ⭐
- Jump to definition (214) ⭐
- Coq interruption (373) ⭐
- Better visualisation for continuous mode (743)
- Add timing information to decorations (231)
- Auto-completion (571, 792) 🏃
- Support for multi-root workspace (683)
- Better _CoqProject parsing (316) ⭐
- Proof of concept for hover in the goal view: the user should get an
Abouton the term he is hovering on ((992) ⭐ - Query shortcuts from symbols in the goal view (283)
- Make the query panel a part of the goal view ⭐ This will allow a number of improvements: make it clear in what state you are performing a query, easy access to results and space gain, lay the groundwork for more interactivity (apply a theorem on click) Issues linked to improving queries that will likely be solved by this: (659, 759, 906, 607)
- More info for queries with no results (153)
- Having seperate scrollable spaces for goals and hypotheses (133)
- Fold goals with an ellipsis depending on window size (872) 🏃
- Easy access to the documentation: a command that triggers a search in the documentation and displays it in a new buffer ((993) ⭐
- User manual for vscoq ((991) ⭐
- Bundle vscoq in the coq-platform (472) ⭐
- Get a one click install (after installing the extension) ((994) (Dependant on the previous goal) ⭐
While working on the language server and this road map, it has come to my attention that changes in Coq would make it extermely more efficient/easy to build a language server.
First of all, working on a concept of doc string and how it integrates with Coq. Working on documentation in of itself. This is partially addressed by several projects (such as coq platform docs ?).
Working on a "global" query system seems to be a very important topic as well. This would complement the context dependant system that is currently in place and should also work hand in hand with a better documentation system.
flowchart LR;
subgraph synterp
A[Raw Text] --parsing--> B[Expr];
end
subgraph interp
B1[Expr] --globalisation--> C[Glob]
C --type checking--> D[Constr]
end
subgraph pp
D1[Contr] --pretty printing--> E[Pp]
E --pp-display lib--> F[DOM]
end
synterp --> interp;
interp --> pp;
The previous diagram represents the full life cycle of a term in Coq from the raw text to the display in, say the VsCoq goal view.
Currently in vscoq we rely on the separation of parsing in execution which of course stops right after obtaining an AST (i.e. the Expr datatype, just before the globalisation stage).
Once we execute a sentence, we end up recording the information after type checking, i.e. Constr, in which we also loose a lot of information that was part of the transient Glob data (location for example). Oversimplifying a bit ("nat",loc) as Expr becomes ("Coq.Init.Logic.nat",loc) as Glob and finally "Coq.Init.Logic.nat" as Contr. The former data lacks the precise meaning of "nat", the latter its location in the input text.
flowchart LR;
B1("(nat,loc)") --globalisation--> C("(Coq.Init.Datatypes.nat,loc)")
C --type checking--> D("Coq.Init.Datatypes.nat")
It is my argument that we should push for separating the globalisation from the interp (type checking phase. This would allow to record a lot of meta-data which will allow us to do many elegant things with no hacks, e.g. hovering for info (even types), jump-to-def, renaming of a symbol... all this without executing the document.
With current Coq semantics this cannot be done in a sound way, but maybe could be approximated with the results updated to the sound info after executing. (example problem:
Definition X := hard to type term.
Module M. Inductive foo : Prop := Foo. End M.
Module N. Inductive foo : Prop := Foo (_:X). End M.
Import M. Import N.
Check foo_rect.
(* N.foo_rect if X : Prop or SProp, otherwise M.foo_rect *)in general any command which generates definitions based on a term cannot be predicted without execution)