Coq Lsp Calls

When and Where

• https://rdv2.rendez-vous.renater.fr/coq-lsp Update, renater login seems broken, we meeting instead at https://wesleyan.zoom.us/j/94445291653?pwd=d1Y3enFZVW83b3lxaUZuczFIY0szZz09
• Monday January 9th, 5pm Paris time (tentative)

Topics

• General presentation, methodology, and roadmap
• Organization of calls, development
• Versioning / compat / release policy
  • Also, what is our base support targets for vscode, node, and Ocaml versions (c.f. https://github.com/ejgallego/coq-lsp/pull/135)
• Diagnostics vs Proof Assistants (c.f https://github.com/ejgallego/coq-lsp/pull/129)
• Build / vendoring setup (c.f. https://github.com/ejgallego/coq-lsp/pull/82#issuecomment-1366963101)
• HCI testing and design (c.f. https://github.com/ejgallego/coq-lsp/issues/132)
• Coq Pane / Workspace
• Search
• LSP Testing (fakeide style) (Ali)
• System Requirements (Ali)
  • We should warn users that using coq-lsp will be slightly heavier than regular coqc and give them a memory usage heuristic.
• Integration with the build system(s)
• Goals for 0.2

Notes for first meeting (09/01/2023)

• Add more on HCI and feedback from users (Ali) Maybe add a suggestion box to Coq panel?
• Code actions and hover, two points:
  • however for now locates the full sentence, you need an AST refiner (or a span refiner)