VsCoq 2, new foundations
summary
Full reimplementation of the VSCoq extension ships a standalone OCaml language server and a TypeScript React client with a reactive document model, a query panel, goals view and autocomplete. The design enforces a separation of parsing and execution so editing uses cheap parsing while proof steps use an execution manager; LSP is extended with verbs like vs/interpret_at_point. Released in September with three minor updates, it works but slow proofs still push users to manual mode.
AI-written summary · about
chapters (9)
- 0:00VsCoq 2 introduction
- 1:06IDE evolution for Coq
- 3:11LSP for theorem provers
- 4:55Parsing vs execution in VsCoq 2
- 5:59VsCoq 2 language server
- 7:03VsCoq 2 demo
- 12:44VsCoq 2 progress and plans
- 13:26Key takeaways
- 14:51Q&A
related talks
56mSession with the Coq Development Team
30mImproving the development experience with language servers
32mA New Era of OCaml Editing: Powered by Merlin, Delivered via LSP
07mIntroducing Volar, a Common Framework for Language Tooling
46mSix steps from zero to IDE
35mMaking a lot of things
40mIntegrating IDEs with Dotty the experimental Scala compiler
22mState of the OCaml Platform 2023