-
Notifications
You must be signed in to change notification settings - Fork 1
VsCoq weekly calls
VsCoq developers meet in a weekly call on Tuesdays, at 10:00 Paris time.
We use the RENATER rendez-vous service, which you can join using your browser: https://rendez-vous.renater.fr/vscoq-weekly
skipped
- The parsing / execution Coq PR has been merged
- The experiments on completion are converging
- Some VsCoq performance issues were encountered on large files that need to be fixed
- One of them is the sending of highlights. Try to see if the highlights state can be represented in a more compact way.
- The Coq patch on parsing / exec separation is converging
- We should monitor the Coq 8.18 release, to align the VsCoq ones
- Mentioned the UI meeting on April 12th. It would be nice to add a completion demo to the ones for more basic features.
- unit tests (Enrico)
skipped
Summary of activity:
- Experiment developing a tool to measure how good completion is, not easy to make Python & language server communicate
- Manual / continuous checking mode
- More queries in the panel (Locate, Print)
- Client / server version
- Detection of Coq binaries: Coq PR opened, some fixes still needed
- Integration of the parsing / execution separation in Coq almost done, some work remains for
Load - Starting refactoring the protocol encoding using ADTs in the language server
For ranking completions, computation of intersection of types can be refined to distinguish premises and conclusion of lemmas. Suggestion to use the EConstr.decompose_prod_n_decls API.
Enrico went through these slides talking about the mechanisms in Coq.
We will move the VsCoq 2 development activity to a branch named main which will be the default, and the VsCoq 1 dev to a vscoq1 branch (or with a better name if we find one :) ).
The README should more clearly mention that the plan is to ship a first production-ready version at the time Coq 8.18 is released.
The VsCoq 1 PRs will be prefixed by [VsCoq1] in their title so that they can quickly be spotted by VsCoq 1 maintainers (including in notifications).
Small demo from ITU. Completion works, with no particular filtering or ranking yet. The whole list of objets is currently fetched from Coq. Suggestion to split off the hover feature (as it is being implemented in https://github.com/coq-community/vscoq/issues/343) and to prepare a first prototype of auto completion that can be integrated (as long as it is not triggered too eagerly while typing).
Nobody has looked at it yet, so item postponed for next week.
We will make all the dev go through PRs and issues tracked in the roadmap (including intermediate steps of the ongoing work on autocompletion).
vscoqtop debug flags should be documented.