Merge branch 'main' into v8.16

.gitmodules

@@ -1,8 +0,0 @@
-[submodule "coq"]
-	path = vendor/coq
-	url = https://github.com/ejgallego/coq.git
-	branch = proof+no_global_partial
-[submodule "coq-serapi"]
-	path = vendor/coq-serapi
-	url = https://github.com/ejgallego/coq-serapi.git
-	branch = v8.17

CHANGES.md

@@ -1,3 +1,29 @@
+# coq-lsp 0.1.3: Event
+----------------------
+
+ - Much improved handling of Coq fatal errors, the server is now
+   hardened against them (@ejgallego, #155, #157, #160, fixes #91)
+ - `coq-lsp` now follows the LSP specification regarding
+   initialization strictly (@ejgallego, #168)
+ - New setting for goals to be updated when the selection changes due
+   to a command; this makes VsCodeVim cursor tracking work; thanks to
+   Cactus (Anton) Golov for detailed bug reporting and testing
+   (@ejgallego, @jesyspa, #170, fixes #163)
+ - `coq-lsp` will now warn the user when two files have been opened
+   simultaneously and the parser may go into a broken state :/
+   (@ejgallego, #169)
+ - Implement request postponement and cancellation. Thus
+   `documentSymbols` will now be postponed until the document is
+   ready, (@ejgallego, #141, #146, fixes #124)
+ - Protocol and VS Code interfaces now support shelved and given_up
+   goals (@ejgallego, #175)
+ - Allow to postpone requests to wait for data to become available on
+   document points; this is implemented to provide a nicer "show goals
+   while I type" experience. Client default has been changed to "show
+   goals on mouse, click, typing, and cursor movement) (@ejgallego,
+   #177, #179)
+ - Store stats per document (@ejgallego, #180, fixes #173)
+
 # coq-lsp 0.1.2: Message
 ------------------------
 

Makefile

@@ -1,10 +1,6 @@
 COQ_BUILD_CONTEXT=../_build/default/coq
 
-PKG_SET= \
-vendor/coq/coq-core.install \
-vendor/coq/coq-stdlib.install \
-vendor/coq-serapi/coq-serapi.install \
-coq-lsp.install
+PKG_SET=coq-lsp.install
 
 # Get the ocamlformat version from the .ocamlformat file
 OCAMLFORMAT=ocamlformat.$$(awk -F = '$$1 == "version" {print $$2}' .ocamlformat)
@@ -15,7 +11,7 @@ $(OCAMLFORMAT) \
 ocaml-lsp-server
 
 .PHONY: build
-build: coq_boot
+build:
 	dune build $(DUNEOPT) $(PKG_SET)
 
 .PHONY: check
@@ -83,3 +79,11 @@ submodules-deinit:
 .PHONY: extension
 extension:
 	cd editor/code && npm i && npm run compile
+
+# Run prettier
+.PHONY: ts-fmt
+ts-fmt:
+	cd editor/code && npx prettier -w .
+
+.PHONY: make-fmt
+make-fmt: build fmt

README.md

@@ -27,12 +27,19 @@ to stop by.
   https://marketplace.visualstudio.com/items?itemName=ejgallego.coq-lsp
 - GNU Emacs: `M-x eglot [Enter] coq-lsp [Enter]`
 
+## FAQ
+
+See our [list of frequently-asked questions](./etc/FAQ.md).
+
 ## Troubleshooting
 
 - Most problems can be resolved by restarting `coq-lsp`, in Visual Studio Code,
   `Ctrl+Shift+P` will give you access to the `coq-lsp.restart` command.
 - In VSCode, the "Output" window will have a "Coq LSP Server Events"
   channel which should contain some important information.
+- As of today, `coq-lsp` may have trouble when more than one file is open at
+  the same time, this is a problem upstream. For now, you are advised to
+  work on a single file if this problem appears.
 
 ## Features
 
@@ -52,7 +59,7 @@ should not, please file a bug!
 
 ### Smart, Cache-aware Error recovery
 
-`coq-lsp` won't stop checking on errors, but support (and encourages) working
+`coq-lsp` won't stop checking on errors, but supports (and encourages) working
 with proof documents that are only partially working. Moreover, error recovery
 integrates with the incremental cache, and will recognize proof structure.
 
@@ -252,6 +259,10 @@ inspirations, and sharing of ideas from colleagues. In particular, we'd like to
 thank Rudi Grinberg, Andrey Mokhov, Clément Pit-Claudel, and Makarius Wenzel
 for their help and advice.
 
+As noted above, the original implementation was based on the Lambdapi LSP
+server, thanks to all our collaborators in that project!
+
+
 <!-- Local Variables: -->
 <!-- mode: Markdown -->
 <!-- fill-column: 80 -->

controller/cache.ml

@@ -0,0 +1,47 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(************************************************************************)
+(* Coq Language Server Protocol                                         *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+module LIO = Lsp.Io
+
+(* Cache stuff *)
+let memo_cache_file = ".coq-lsp.cache"
+
+let memo_save_to_disk () =
+  try
+    Fleche.Memo.save_to_disk ~file:memo_cache_file;
+    LIO.trace "memo" "cache saved to disk"
+  with exn ->
+    LIO.trace "memo" (Printexc.to_string exn);
+    Sys.remove memo_cache_file;
+    ()
+
+(* We disable it for now, see todo.org for more information *)
+let save_to_disk () = if false then memo_save_to_disk ()
+
+let memo_read_from_disk () =
+  try
+    if Sys.file_exists memo_cache_file then (
+      LIO.trace "memo" "trying to load cache file";
+      Fleche.Memo.load_from_disk ~file:memo_cache_file;
+      LIO.trace "memo" "cache file loaded")
+    else LIO.trace "memo" "cache file not present"
+  with exn ->
+    LIO.trace "memo" ("loading cache failed: " ^ Printexc.to_string exn);
+    Sys.remove memo_cache_file;
+    ()
+
+let read_from_disk () = if false then memo_read_from_disk ()

controller/cache.mli

@@ -0,0 +1,19 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(************************************************************************)
+(* Coq Language Server Protocol                                         *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2019-2023 Inria      -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+
+val save_to_disk : unit -> unit
+val read_from_disk : unit -> unit