Merge branch 'v8.20' into v8.19

.github/workflows/build.yml

@@ -117,7 +117,6 @@ jobs:
           opam install zarith_stubs_js js_of_ocaml-ppx -y
 
       - name: 💉💉💉 Patch Coq
-        if: false # FIXME, Coq is in opam but needs to be patched for the worker to be functional
         run: make patch-for-js
 
       - name: 🦏🧱🦏 Build coq-lsp JS version 🦏🦏🦏

CHANGES.md

@@ -15,11 +15,29 @@
    #883)
  - [general] [js] Adapt to Rocq stdlib split (@ejgallego, #890)
  - [ci] Bump setup-ocaml to v3 (@ejgallego, #890)
- - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, #815 #890)
+ - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, #815,
+   #890)
  - [petanque] `petanque/start` now fails when the theorem was parsed
    but not successfully executed (@ejgallego, reported by @gbdrt,
    #901, fixes #886)
  - [ci] Test Ocaml 5.3 (@ejgallego, #904)
+ - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
+   reduces the Stack Overflow in the proof engine (@ejgallego,
+   @corwin-of-amber, #905)
+ - [js worker] [build] Include Coq WaterProof in the default Web
+   Worker build (@ejgallego, waterproof team, #905, closes #888)
+ - [vscode] [web] Fix web extension not exporting the coq-lsp
+   extension API (@ejgallego, reported by @amblafont, #911, fixes
+   #877)
+ - [build] [general] Rename our internal `Lsp` library to
+   `Fleche_lsp`; this should help avoiding conflicts with the OCaml
+   `lsp` library (@ejgallego, reported by @blackbird1128, #912, fixes
+   #861)
+ - [workspace] Remove support legacy ML-search path semantics. These
+   were basically unused since Coq 8.16. As a consequence, `coq-lsp` /
+   `fcc` don't accept the `-I` flag anymore, use `OCAMLPATH` or the
+   `--ocamlpath=` option to pass extra `findlib` paths. We still
+   respect the -I flag in `_CoqMakefile` (@ejgallego, #916)
 
 # coq-lsp 0.2.2: To Virtual or not To Virtual
 ---------------------------------------------

Makefile

@@ -4,6 +4,10 @@ COQ_BUILD_CONTEXT=../_build/default/coq
 
 PKG_SET= coq-lsp.install
 
+PKG_SET_WEB=
+# This is disabled in stable versions
+# PKG_SET_WEB=$(PKG_SET) vendor/coq-waterproof/coq-waterproof.install
+
 # Get the ocamlformat version from the .ocamlformat file
 OCAMLFORMAT=ocamlformat.$$(awk -F = '$$1 == "version" {print $$2}' .ocamlformat)
 
@@ -74,10 +78,14 @@ winconfig:
 	&& cp theories/dune.disabled theories/dune \
 	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
 
+.PHONY: wp
+wp:
+	dune build vendor/coq-waterproof/coq-waterproof.install
+
 .PHONY: js
 js: COQVM = no
 js: coq_boot
-	dune build --profile=release --display=quiet $(PKG_SET) controller-js/coq_lsp_worker.bc.cjs
+	dune build --profile=release --display=quiet $(PKG_SET_WEB) controller-js/coq_lsp_worker.bc.cjs
 	mkdir -p editor/code/out/ && cp -a controller-js/coq_lsp_worker.bc.cjs editor/code/out/coq_lsp_worker.bc.js
 
 .PHONY: coq_boot
@@ -125,6 +133,8 @@ submodules-deinit:
 submodules-update:
 	(cd vendor/coq && git checkout master && git pull upstream master)
 	(cd vendor/coq-stdlib && git checkout master && git pull upstream master)
+# For now we update manually
+# (cd vendor/coq-waterproof && git checkout coq-master && git pull upstream coq-master)
 
 # Build the vscode extension
 .PHONY: extension
@@ -145,20 +155,39 @@ opam-update-and-reinstall:
 	git pull
 	opam install .
 
-.PHONY: patch-for-js
-patch-for-js:
-	cd vendor/coq && patch -p1 < ../../etc/0001-coq-lsp-patch.patch
-	cd vendor/coq && patch -p1 < ../../etc/0001-jscoq-lib-system.ml-de-unix-stat.patch
-
-_LIBROOT=$(shell opam var lib)
-
-# At some point this may be the better idea
+# These variables are exclusive of the JS build
 # Not true in this branch
 # VENDORED_SETUP:=true
 
-# This is rocq-runtime after 8.20
+# Used in git clone
+COQ_BRANCH=v8.20
+# Used in opam pin
+COQ_CORE_VERSION=8.20.1
+# Name of COQ_CORE_NAME is rocq-runtime after 8.20
 COQ_CORE_NAME=coq-core
 
+ifdef VENDORED_SETUP
+COQ_SRC_DIR=vendor/coq
+PATCH_DIR=../../etc/
+else
+COQ_SRC_DIR=../coq
+PATCH_DIR=$(shell pwd)/etc
+endif
+
+.PHONY: patch-for-js
+patch-for-js:
+ifndef VENDORED_SETUP
+	git clone --depth=1 https://github.com/coq/coq.git -b $(COQ_BRANCH) $(COQ_SRC_DIR)
+endif
+	cd $(COQ_SRC_DIR) && patch -p1 < $(PATCH_DIR)/0001-coq-lsp-patch.patch
+	cd $(COQ_SRC_DIR) && patch -p1 < $(PATCH_DIR)/0001-jscoq-lib-system.ml-de-unix-stat.patch
+	cd $(COQ_SRC_DIR) && patch -p1 < $(PATCH_DIR)/0001-engine-trampoline.patch
+ifndef VENDORED_SETUP
+	opam pin add $(COQ_CORE_NAME).$(COQ_CORE_VERSION) -k path $(COQ_SRC_DIR)
+endif
+
+_LIBROOT=$(shell opam var lib)
+
 ifdef VENDORED_SETUP
 _CCROOT=_build/install/default/lib/$(COQ_CORE_NAME)
 else
@@ -171,12 +200,14 @@ endif
 # Super-hack
 controller-js/coq-fs-core.js: COQVM = no
 controller-js/coq-fs-core.js: coq_boot
-	dune build --profile=release --display=quiet $(PKG_SET) etc/META.threads
+	dune build --profile=release --display=quiet $(PKG_SET_WEB) etc/META.threads
 	for i in $$(find $(_CCROOT)/plugins -name *.cma); do js_of_ocaml --dynlink $$i; done
 	for i in $$(find _build/install/default/lib/coq-lsp/serlib -wholename */*.cma); do js_of_ocaml --dynlink $$i; done
+	for i in $$(find _build/install/default/lib/coq-waterproof/plugin -name *.cma); do js_of_ocaml --dynlink $$i; done
 	js_of_ocaml build-fs -o controller-js/coq-fs-core.js \
 	    $$(find $(_CCROOT)/                          \( -wholename '*/plugins/*/*.js' -or -wholename '*/META' \) -printf "%p:/static/lib/$(COQ_CORE_NAME)/%P ") \
 	    $$(find _build/install/default/lib/coq-lsp/  \( -wholename '*/serlib/*/*.js'  -or -wholename '*/META' \) -printf "%p:/static/lib/coq-lsp/%P ") \
+	    $$(find _build/install/default/lib/coq-waterproof/  \( -wholename '*/plugin/*.js'  -or -wholename '*/META' \) -printf "%p:/static/lib/coq-waterproof/%P ") \
 	    ./etc/META.threads:/static/lib/threads/META \
 	    $$(find $(_LIBROOT) -wholename '*/str/META'                 -printf "%p:/static/lib/%P ") \
 	    $$(find $(_LIBROOT) -wholename '*/seq/META'                 -printf "%p:/static/lib/%P ") \

compiler/driver.ml

@@ -16,6 +16,7 @@ let sanitize_paths message =
   | None -> message
   | Some _ ->
     message
+    |> replace_test_path "findlib: "
     |> replace_test_path "coqlib is at: "
     |> replace_test_path "coqcorelib is at: "
     |> replace_test_path "findlib config: "

compiler/dune

@@ -2,7 +2,7 @@
  (name fcc_lib)
  (modules :standard \ fcc)
  ; LSP is used to print diagnostics, etc...
- (libraries fleche lsp))
+ (libraries fleche fleche_lsp))
 
 (executable
  (public_name fcc)

compiler/fcc.ml

@@ -2,19 +2,16 @@
 open Cmdliner
 open Fcc_lib
 
-let fcc_main int_backend roots display debug plugins files coqlib coqcorelib
-    findlib_config ocamlpath rload_path load_path require_libraries no_vo
-    max_errors coq_diags_level =
+let fcc_main int_backend roots display debug plugins files coqlib findlib_config
+    ocamlpath rload_path load_path require_libraries no_vo max_errors
+    coq_diags_level =
   let vo_load_path = rload_path @ load_path in
-  let ml_include_path = [] in
   let args = [] in
   let cmdline =
     { Coq.Workspace.CmdLine.coqlib
-    ; coqcorelib
     ; findlib_config
     ; ocamlpath
     ; vo_load_path
-    ; ml_include_path
     ; args
     ; require_libraries
     }
@@ -101,8 +98,8 @@ let fcc_cmd : int Cmd.t =
     let open Coq.Args in
     Term.(
       const fcc_main $ int_backend $ roots $ display $ debug $ plugins $ file
-      $ coqlib $ coqcorelib $ findlib_config $ ocamlpath $ rload_paths
-      $ qload_paths $ ri_from $ no_vo $ max_errors $ coq_diags_level)
+      $ coqlib $ findlib_config $ ocamlpath $ rload_paths $ qload_paths
+      $ ri_from $ no_vo $ max_errors $ coq_diags_level)
   in
   let exits = Exit_codes.[ fatal; stopped; scheduled; uri_failed ] in
   Cmd.(v (Cmd.info "fcc" ~exits ~version ~doc ~man) fcc_term)

compiler/output.ml

@@ -1,3 +1,5 @@
+module Lsp = Fleche_lsp
+
 let pp_diag fmt (d : Lang.Diagnostic.t) =
   Format.fprintf fmt "@[%a@]"
     (Yojson.Safe.pretty_print ~std:true)

controller-js/coq_lsp_worker.ml

@@ -10,7 +10,7 @@
  *)
 
 module U = Yojson.Safe.Util
-module LSP = Lsp.Base
+module Lsp = Fleche_lsp
 open Js_of_ocaml
 open Controller
 
@@ -178,11 +178,9 @@ let main () =
     let vo_load_path = List.map (fun f -> f coqlib) [ stdlib; user_contrib ] in
     Coq.Workspace.CmdLine.
       { coqlib
-      ; coqcorelib = "/static/lib/coq-core" (* deprecated upstream *)
       ; findlib_config
       ; ocamlpath
       ; vo_load_path
-      ; ml_include_path = []
       ; require_libraries = [ (None, "Coq.Init.Prelude") ]
       ; args = [ "-noinit"; "-boot" ]
       }

controller-js/dune

@@ -56,6 +56,8 @@
  (targets coq-fs.js)
  (deps
   (package coq-stdlib))
+ ; Not needed
+ ; (package coq-waterproof))
  (action
   (bash
    "export COQW=$(coqc -where) && js_of_ocaml build-fs -o coq-fs.js $(cd $COQW && find theories user-contrib \\( -wholename 'theories/*.vo' -or -wholename 'theories/*.glob' -or -wholename 'theories/*.v' -or -wholename 'user-contrib/*.vo' -or -wholename 'user-contrib/*.v' -or -wholename 'user-contrib/*.glob' \\) -printf \"$COQW/%p:/static/coqlib/%p \")")))

controller/coq_lsp.ml

@@ -81,8 +81,8 @@ let rec lsp_init_loop ~io ~ifn ~ofn ~cmdline ~debug =
     L.trace "read_request" "error: %s" err;
     lsp_init_loop ~io ~ifn ~ofn ~cmdline ~debug
 
-let lsp_main bt coqcorelib coqlib findlib_config ocamlpath vo_load_path
-    ml_include_path require_libraries delay int_backend =
+let lsp_main bt coqlib findlib_config ocamlpath vo_load_path require_libraries
+    delay int_backend =
   Coq.Limits.select_best int_backend;
   Coq.Limits.start ();
 
@@ -112,12 +112,10 @@ let lsp_main bt coqcorelib coqlib findlib_config ocamlpath vo_load_path
   let debug = bt || Fleche.Debug.backtraces in
   let root_state = coq_init ~debug in
   let cmdline =
-    { Coq.Workspace.CmdLine.coqcorelib
-    ; coqlib
+    { Coq.Workspace.CmdLine.coqlib
     ; findlib_config
     ; ocamlpath
     ; vo_load_path
-    ; ml_include_path
     ; args = []
     ; require_libraries
     }
@@ -201,8 +199,8 @@ let lsp_cmd : unit Cmd.t =
     v
       (Cmd.info "coq-lsp" ~version:Fleche.Version.server ~doc ~man)
       Term.(
-        const lsp_main $ bt $ coqcorelib $ coqlib $ findlib_config $ ocamlpath
-        $ vo_load_path $ ml_include_path $ ri_from $ delay $ int_backend))
+        const lsp_main $ bt $ coqlib $ findlib_config $ ocamlpath $ vo_load_path
+        $ ri_from $ delay $ int_backend))
 
 let main () =
   let ecode = Cmd.eval lsp_cmd in

controller/dune

@@ -1,7 +1,7 @@
 (library
  (name controller)
  (modules :standard \ coq_lsp)
- (libraries coq fleche petanque petanque_json lsp dune-build-info))
+ (libraries coq fleche petanque petanque_json fleche_lsp dune-build-info))
 
 (executable
  (name coq_lsp)

controller/lsp_core.ml

@@ -34,7 +34,7 @@ let string_field name dict = U.to_string (field name dict)
 let ofield name dict = List.(assoc_opt name dict)
 let ostring_field name dict = Option.map U.to_string (ofield name dict)
 
-module LSP = Lsp.Base
+module Lsp = Fleche_lsp
 module L = Fleche.Io.Log
 
 module Helpers = struct
@@ -171,17 +171,21 @@ module Rq : sig
   end
 
   val serve :
-       ofn_rq:(LSP.Response.t -> unit)
+       ofn_rq:(Lsp.Base.Response.t -> unit)
     -> token:Coq.Limits.Token.t
     -> id:int
     -> Action.t
     -> unit
 
   val cancel :
-    ofn_rq:(LSP.Response.t -> unit) -> code:int -> message:string -> int -> unit
+       ofn_rq:(Lsp.Base.Response.t -> unit)
+    -> code:int
+    -> message:string
+    -> int
+    -> unit
 
   val serve_postponed :
-       ofn_rq:(LSP.Response.t -> unit)
+       ofn_rq:(Lsp.Base.Response.t -> unit)
     -> token:Coq.Limits.Token.t
     -> doc:Fleche.Doc.t
     -> Int.Set.t
@@ -190,8 +194,8 @@ end = struct
   (* Answer a request, private *)
   let answer ~ofn_rq ~id result =
     (match result with
-    | Result.Ok result -> LSP.Response.mk_ok ~id ~result
-    | Error (code, message) -> LSP.Response.mk_error ~id ~code ~message)
+    | Result.Ok result -> Lsp.Base.Response.mk_ok ~id ~result
+    | Error (code, message) -> Lsp.Base.Response.mk_error ~id ~code ~message)
     |> ofn_rq
 
   (* private to the Rq module, just used not to retrigger canceled requests *)
@@ -517,7 +521,7 @@ let lsp_init_process ~ofn ~io ~cmdline ~debug msg : Init_effect.t =
   let ofn_rq r = Lsp.Base.Message.response r |> ofn in
   let ofn_nt r = Lsp.Base.Message.notification r |> ofn in
   match msg with
-  | LSP.Message.Request { method_ = "initialize"; id; params } ->
+  | Lsp.Base.Message.Request { method_ = "initialize"; id; params } ->
     (* At this point logging is allowed per LSP spec *)
     Fleche.Io.Report.msg ~io ~lvl:Info "Initializing coq-lsp server %s"
       (version ());
@@ -536,16 +540,17 @@ let lsp_init_process ~ofn ~io ~cmdline ~debug msg : Init_effect.t =
     in
     List.iter (log_workspace ~io) workspaces;
     Success workspaces
-  | LSP.Message.Request { id; _ } ->
+  | Lsp.Base.Message.Request { id; _ } ->
     (* per spec *)
-    LSP.Response.mk_error ~id ~code:(-32002) ~message:"server not initialized"
+    Lsp.Base.Response.mk_error ~id ~code:(-32002)
+      ~message:"server not initialized"
     |> ofn_rq;
     Loop
-  | LSP.Message.Notification { method_ = "exit"; params = _ } -> Exit
-  | LSP.Message.Notification _ ->
+  | Lsp.Base.Message.Notification { method_ = "exit"; params = _ } -> Exit
+  | Lsp.Base.Message.Notification _ ->
     (* We can't log before getting the initialize message *)
     Loop
-  | LSP.Message.Response _ ->
+  | Lsp.Base.Message.Response _ ->
     (* O_O *)
     Loop
 
@@ -616,7 +621,8 @@ let dispatch_request ~token ~method_ ~params : Rq.Action.t =
 let dispatch_request ~ofn_rq ~token ~id ~method_ ~params =
   dispatch_request ~token ~method_ ~params |> Rq.serve ~ofn_rq ~token ~id
 
-let dispatch_message ~io ~ofn ~token ~state (com : LSP.Message.t) : State.t =
+let dispatch_message ~io ~ofn ~token ~state (com : Lsp.Base.Message.t) : State.t
+    =
   let ofn_rq r = Lsp.Base.Message.response r |> ofn in
   match com with
   | Notification { method_; params } ->
@@ -666,8 +672,8 @@ let check_or_yield ~io ~ofn ~token ~state =
     Cont state
 
 module LspQueue : sig
-  val pop_opt : unit -> LSP.Message.t option
-  val push_and_optimize : LSP.Message.t -> unit
+  val pop_opt : unit -> Lsp.Base.Message.t option
+  val push_and_optimize : Lsp.Base.Message.t -> unit
 end = struct
   let request_queue = Queue.create ()
 
@@ -679,7 +685,8 @@ end = struct
       Some v
 
   let analyze = function
-    | LSP.Message.Notification { method_ = "textDocument/didChange"; params } ->
+    | Lsp.Base.Message.Notification
+        { method_ = "textDocument/didChange"; params } ->
       let uri, version = Helpers.get_uri_version params in
       Some (uri, version)
     | _ -> None
@@ -724,14 +731,14 @@ let dispatch_or_resume_check ~io ~ofn ~state =
     let iexn = Exninfo.capture exn in
     L.trace "process_queue" "%s"
       (if Printexc.backtrace_status () then "bt=true" else "bt=false");
-    (* let method_name = LSP.Message.method_ com in *)
+    (* let method_name = Lsp.Base.Message.method_ com in *)
     (* L.trace "process_queue" "exn in method: %s" method_name; *)
     L.trace "print_exn [OCaml]" "%s" (Printexc.to_string exn);
     L.trace "print_exn [Coq  ]" "%a" Pp.pp_with CErrors.(iprint iexn);
     L.trace "print_bt  [OCaml]" "%s" bt;
     Some (Yield state)
 
-let enqueue_message (com : LSP.Message.t) =
+let enqueue_message (com : Lsp.Base.Message.t) =
   if Fleche.Debug.sched_wakeup then
     L.trace "-> enqueue" "%.2f" (Unix.gettimeofday ());
   (* TODO: this is the place to cancel pending requests that are invalid, and in