LSP server
This issue aims at tracking what we would like to add to the current embryo of support of LSP for Why3
-
Automatic report of syntax errors and typing errors when saving the source file -
go to the definition of a global symbol -
fix: go to a module name : needs to fix why3doc glob tables
-
-
go to the definition of a local symbol - needs to fix why3doc glob tables so as they also include local symbols
-
show the type of a symbol - again, modify the glob so as to store lsymbols, psymbols, etc. instead of idents
-
utiliser user-setup dans opam pour installer le mode why3 -
simple proof mode : run split VC
thenAuto level 0
and report all VCs not proved, in the proper line of the source (like syntax errors) -
auto indentation of the current line (maybe create a separate issue) -
propose completion: show all symbols starting with current identifier, show their types -
important issue: make things, like go to def, work even on files with syntax errors (difficult to do, may need many changes in the parser. Investigate how menhir could do things automatically. Investigate how merlin does for OCaml)
Other secondary issues:
- discuss alternative to allowing passing options to the underlying why3 : the current solution is an extra config file named
.why3_lsp_server.conf
in the directory of the source See also #430 - PRIORITAIRE add additional support for VScode
- PRIORITAIRE put the code of LSP-why3 directly in Why3 repository