Merge branch 'v8.18' into v8.17

CHANGES.md

@@ -75,6 +75,29 @@
    server-side option is enabled (@ejgallego, #670)
  - include range of full sentence in error diagnostic extra data
    (@ejgallego, #670 , thanks to @driverag22 for the idea, cc: #663).
+ - The `coq-lsp.pp_type` VSCode client option now takes effect
+   immediately, no more need to restart the server to get different
+   goal display formats (@ejgallego, #675)
+ - new public VSCode extension API so other extensions can perform
+   actions when the user request the goals (@ejgallego, @bhaktishh,
+   #672, fixes #538)
+ - Support Visual Studio Live Share URIs better (`vsls://`), in
+   particular don't try to display goals if the URI is VSLS one
+   (@ejgallego, #676)
+ - New `InjectRequire` plugin API for plugins to be able to instrument
+   the default import list of files (@ejgallego @corwin-of-amber,
+   #679)
+ - Add `--max_errors=n` option to `fcc`, this way users can set
+   `--max_errors=0` to imitate `coqc` behavior (@ejgallego, #680)
+ - Fix `fcc` exit status when checking terminates with fatal errors
+   (@ejgallego, @Alizter, #680)
+ - Fix install to OPAM switches from `main` branch (@ejgallego, #683,
+   fixes #682, cc #479 #488, thanks to @Hazardouspeach for the report)
+ - New `--int_backend={Coq,Mp}` command line parameter to select the
+   interruption method for Coq (@ejgallego, #684)
+ - Update `package-lock.json` for latest bugfixes (@ejgallego, #687)
+ - Update Nix flake enviroment (@Alizter, #684 #688)
+ - Update `prettier` (@Alizter @ejgallego, #684 #688)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

CONTRIBUTING.md

@@ -58,12 +58,27 @@ generate it from the relevant entries in `CHANGES.md` at release time.
 
 ### Compilation
 
-#### Opam/Dune
 The server project uses a standard OCaml development setup based on
 Opam and Dune. This also works on Windows using the [Coq Platform
 Source
 Install](https://github.com/coq/platform/blob/main/doc/README_Windows.md#installation-by-compiling-from-sources-using-opam-on-cygwin)
 
+The default development environment for `coq-lsp` is a "composed"
+build that includes git submodules for `coq` and `coq-serapi` in the
+`vendor/` directory. This allows us to easily work with PRs using
+experimental Coq branches, and some other advantages like a better CI
+build cache and easier bisects.
+
+This will however install a local Coq version which may not be
+convenient for all use cases; we thus detail below an alternative
+install method for those that would like to install a `coq-lsp`
+development branch into an OPAM switch.
+
+#### Default development setup, local Coq / `coq-lsp`
+
+This setup will build Coq and `coq-lsp` locally; it is the recommended
+way to develop `coq-lsp` itself.
+
 1. Install the dependencies (the complete updated list of dependencies can be found in `coq-lsp.opam`).
 
     ```sh
@@ -85,6 +100,31 @@ Install](https://github.com/coq/platform/blob/main/doc/README_Windows.md#install
 
 Alternatively, you can also use the regular `dune build @check` etc... targets.
 
+Now, binaries for Coq and `coq-lsp` can be found under
+`_build/install/default` and used via `dune exec -- fcc` or `dune exec
+-- $your_editor`.
+
+#### Global OPAM install
+
+This setup will build Coq and `coq-lsp` and install them to the
+current OPAM switch. This is a good setup for people looking to try
+out `coq-lsp` development versions with other OPAM packages.
+
+1. Install vendored Coq and SerAPI:
+
+    ```sh
+    opam install vendor/coq/coq{-core,-stdlib,}.opam
+    opam install vendor/coq-serapi
+    ```
+
+2. Install `coq-lsp`:
+    ```sh
+    opam install .
+    ```
+
+Then, you should get a working OPAM switch with Coq and `coq-lsp` from
+your chosen `coq-lsp` branch.
+
 #### Nix
 
 We have a Nix flake that you can use.

compiler/args.ml

@@ -12,6 +12,8 @@ type t =
   ; debug : bool  (** run in debug mode *)
   ; display : Display.t  (** display level *)
   ; plugins : string list  (** Flèche plugins to load *)
+  ; max_errors : int option
+        (** Maximum erros before aborting the compilation *)
   }
 
 let compute_default_plugins ~no_vo ~plugins =

compiler/compile.ml

@@ -24,24 +24,40 @@ let save_diags_file ~(doc : Fleche.Doc.t) =
   let diags = Fleche.Doc.diags doc in
   Util.format_to_file ~file ~f:Output.pp_diags diags
 
-let compile_file ~cc file =
+(** Return: exit status for file:
+
+    - 1: fatal error in checking (usually due to [max_errors=n]
+    - 2: checking stopped
+    - 102: file not scheduled
+    - 222: Incorrect URI *)
+let status_of_doc (doc : Doc.t) =
+  match doc.completed with
+  | Yes _ -> 0
+  | Stopped _ -> 2
+  | Failed _ | FailedPermanent _ -> 1
+
+let compile_file ~cc file : int =
   let { Cc.io; root_state; workspaces; default; token } = cc in
   let lvl = Io.Level.info in
   let message = Format.asprintf "compiling file %s" file in
   Io.Report.message ~io ~lvl ~message;
   match Lang.LUri.(File.of_uri (of_string file)) with
-  | Error _ -> ()
+  | Error _ -> 222
   | Ok uri -> (
     let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in
     let files = Coq.Files.make () in
     let env = Doc.Env.make ~init:root_state ~workspace ~files in
     let raw = Util.input_all file in
     let () = Theory.create ~io ~token ~env ~uri ~raw ~version:1 in
     match Theory.Check.maybe_check ~io ~token with
-    | None -> ()
+    | None -> 102
     | Some (_, doc) ->
       save_diags_file ~doc;
       (* Vo file saving is now done by a plugin *)
-      Theory.close ~uri)
+      Theory.close ~uri;
+      status_of_doc doc)
 
-let compile ~cc = List.iter (compile_file ~cc)
+let compile ~cc =
+  List.fold_left
+    (fun status file -> if status = 0 then compile_file ~cc file else status)
+    0

compiler/driver.ml

@@ -30,8 +30,15 @@ let log_workspace ~io (dir, w) =
 let load_plugin plugin_name = Fl_dynload.load_packages [ plugin_name ]
 let plugin_init = List.iter load_plugin
 
-let go args =
-  let { Args.cmdline; roots; display; debug; files; plugins } = args in
+let apply_config ~max_errors =
+  Option.iter
+    (fun max_errors -> Fleche.Config.v := { !Fleche.Config.v with max_errors })
+    max_errors
+
+let go ~int_backend args =
+  let { Args.cmdline; roots; display; debug; files; plugins; max_errors } =
+    args
+  in
   (* Initialize event callbacks, in testing don't do perfData *)
   let perfData = Option.is_empty fcc_test in
   let io = Output.init display ~perfData in
@@ -40,13 +47,16 @@ let go args =
   let root_state = coq_init ~debug in
   let roots = if List.length roots < 1 then [ Sys.getcwd () ] else roots in
   let default = Coq.Workspace.default ~debug ~cmdline in
+  let () = Coq.Limits.select int_backend in
+  let () = Coq.Limits.start () in
   let token = Coq.Limits.Token.create () in
   let workspaces =
     List.map
       (fun dir -> (dir, Coq.Workspace.guess ~token ~cmdline ~debug ~dir))
       roots
   in
   List.iter (log_workspace ~io) workspaces;
+  let () = apply_config ~max_errors in
   let cc = Cc.{ root_state; workspaces; default; io; token } in
   (* Initialize plugins *)
   plugin_init plugins;

compiler/fcc.ml

@@ -2,8 +2,8 @@
 open Cmdliner
 open Fcc_lib
 
-let fcc_main roots display debug plugins files coqlib coqcorelib ocamlpath
-    rload_path load_path require_libraries no_vo =
+let fcc_main int_backend roots display debug plugins files coqlib coqcorelib
+    ocamlpath rload_path load_path require_libraries no_vo max_errors =
   let vo_load_path = rload_path @ load_path in
   let ml_include_path = [] in
   let args = [] in
@@ -18,61 +18,12 @@ let fcc_main roots display debug plugins files coqlib coqcorelib ocamlpath
     }
   in
   let plugins = Args.compute_default_plugins ~no_vo ~plugins in
-  let args = Args.{ cmdline; roots; display; files; debug; plugins } in
-  Driver.go args
-
-(****************************************************************************)
-(* XXX: Common with coq-lsp.exe *)
-let coqlib =
-  let doc =
-    "Load Coq.Init.Prelude from $(docv); theories and user-contrib should live \
-     there."
-  in
-  Arg.(
-    value & opt string Coq_config.coqlib & info [ "coqlib" ] ~docv:"COQLIB" ~doc)
-
-let coqcorelib =
-  let doc = "Path to Coq plugin directories." in
-  Arg.(
-    value
-    & opt string (Filename.concat Coq_config.coqlib "../coq-core/")
-    & info [ "coqcorelib" ] ~docv:"COQCORELIB" ~doc)
-
-let ocamlpath =
-  let doc = "Path to OCaml's lib" in
-  Arg.(
-    value & opt (some string) None & info [ "ocamlpath" ] ~docv:"OCAMLPATH" ~doc)
-
-let coq_lp_conv ~implicit (unix_path, lp) =
-  { Loadpath.coq_path = Libnames.dirpath_of_string lp
-  ; unix_path
-  ; has_ml = true
-  ; implicit
-  ; recursive = true
-  }
-
-let rload_path : Loadpath.vo_path list Term.t =
-  let doc =
-    "Bind a logical loadpath LP to a directory DIR and implicitly open its \
-     namespace."
+  let args =
+    Args.{ cmdline; roots; display; files; debug; plugins; max_errors }
   in
-  Term.(
-    const List.(map (coq_lp_conv ~implicit:true))
-    $ Arg.(
-        value
-        & opt_all (pair dir string) []
-        & info [ "R"; "rec-load-path" ] ~docv:"DIR,LP" ~doc))
+  Driver.go ~int_backend args
 
-let load_path : Loadpath.vo_path list Term.t =
-  let doc = "Bind a logical loadpath LP to a directory DIR" in
-  Term.(
-    const List.(map (coq_lp_conv ~implicit:false))
-    $ Arg.(
-        value
-        & opt_all (pair dir string) []
-        & info [ "Q"; "load-path" ] ~docv:"DIR,LP" ~doc))
 (****************************************************************************)
-
 (* Specific to fcc *)
 let roots : string list Term.t =
   let doc = "Workspace(s) root(s)" in
@@ -88,10 +39,6 @@ let display : Args.Display.t Term.t =
     & opt (enum dparse) Args.Display.Normal
     & info [ "display" ] ~docv:"DISPLAY" ~doc)
 
-let debug : bool Term.t =
-  let doc = "Enable debug mode" in
-  Arg.(value & flag & info [ "debug" ] ~doc)
-
 let file : string list Term.t =
   let doc = "File(s) to compile" in
   Arg.(value & pos_all string [] & info [] ~docv:"FILES" ~doc)
@@ -100,23 +47,40 @@ let plugins : string list Term.t =
   let doc = "Compiler plugins to load" in
   Arg.(value & opt_all string [] & info [ "plugin" ] ~docv:"PLUGINS" ~doc)
 
-let rifrom : (string option * string) list Term.t =
-  let doc =
-    "FROM Require Import LIBRARY before creating the document, à la From Coq \
-     Require Import Prelude"
-  in
-  Term.(
-    const (List.map (fun (x, y) -> (Some x, y)))
-    $ Arg.(
-        value
-        & opt_all (pair string string) []
-        & info [ "rifrom"; "require-import-from" ] ~docv:"FROM,LIBRARY" ~doc))
-
 let no_vo : bool Term.t =
   let doc = "Don't generate .vo files at the end of compilation" in
   Arg.(value & flag & info [ "no_vo" ] ~doc)
 
-let fcc_cmd : unit Cmd.t =
+let max_errors : int option Term.t =
+  let doc = "Maximum errors in files before aborting" in
+  Arg.(
+    value & opt (some int) None & info [ "max_errors" ] ~docv:"MAX_ERRORS" ~doc)
+
+module Exit_codes = struct
+  let fatal : Cmd.Exit.info =
+    let doc =
+      "A fatal error was found. This is typically due to `--max_errors` being \
+       triggered, but also failures in library / Coq setup will trigger this."
+    in
+    Cmd.Exit.info ~doc 1
+
+  let stopped : Cmd.Exit.info =
+    let doc =
+      "The document was not fully checked: this is often due to a timeout, \
+       interrupt, or resource limit."
+    in
+    Cmd.Exit.info ~doc 2
+
+  let scheduled : Cmd.Exit.info =
+    let doc = "[INTERNAL] File not scheduled" in
+    Cmd.Exit.info ~doc 102
+
+  let uri_failed : Cmd.Exit.info =
+    let doc = "[INTERNAL] URI failed" in
+    Cmd.Exit.info ~doc 222
+end
+
+let fcc_cmd : int Cmd.t =
   let doc = "Flèche Coq Compiler" in
   let man =
     [ `S "DESCRIPTION"
@@ -127,14 +91,17 @@ let fcc_cmd : unit Cmd.t =
   in
   let version = Fleche.Version.server in
   let fcc_term =
+    let open Coq.Args in
     Term.(
-      const fcc_main $ roots $ display $ debug $ plugins $ file $ coqlib
-      $ coqcorelib $ ocamlpath $ rload_path $ load_path $ rifrom $ no_vo)
+      const fcc_main $ int_backend $ roots $ display $ debug $ plugins $ file
+      $ coqlib $ coqcorelib $ ocamlpath $ rload_paths $ qload_paths $ ri_from
+      $ no_vo $ max_errors)
   in
-  Cmd.(v (Cmd.info "fcc" ~version ~doc ~man) fcc_term)
+  let exits = Exit_codes.[ fatal; stopped; scheduled; uri_failed ] in
+  Cmd.(v (Cmd.info "fcc" ~exits ~version ~doc ~man) fcc_term)
 
 let main () =
-  let ecode = Cmd.eval fcc_cmd in
+  let ecode = Cmd.eval' fcc_cmd in
   exit ecode
 
 let () = main ()