Merge branch 'main' into v8.19

CHANGES.md

@@ -87,6 +87,14 @@
  - 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)
 
 # 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,11 +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
+  let args =
+    Args.{ cmdline; roots; display; files; debug; plugins; max_errors }
+  in
+  Driver.go ~int_backend args
 
 (****************************************************************************)
-
 (* Specific to fcc *)
 let roots : string list Term.t =
   let doc = "Workspace(s) root(s)" in
@@ -50,7 +51,36 @@ 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"
@@ -63,13 +93,15 @@ let fcc_cmd : unit Cmd.t =
   let fcc_term =
     let open Coq.Args in
     Term.(
-      const fcc_main $ roots $ display $ debug $ plugins $ file $ coqlib
-      $ coqcorelib $ ocamlpath $ rload_paths $ qload_paths $ ri_from $ 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 ()

controller/coq_lsp.ml

@@ -98,7 +98,10 @@ let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug =
     | Init_effect.Success w -> w)
 
 let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
-    require_libraries delay =
+    require_libraries delay int_backend =
+  Coq.Limits.select int_backend;
+  Coq.Limits.start ();
+
   (* Try to be sane w.r.t. \r\n in Windows *)
   Stdlib.set_binary_mode_in stdin true;
   Stdlib.set_binary_mode_out stdout true;
@@ -207,7 +210,7 @@ let lsp_cmd : unit Cmd.t =
       (Cmd.info "coq-lsp" ~version:Fleche.Version.server ~doc ~man)
       Term.(
         const lsp_main $ bt $ coqcorelib $ coqlib $ ocamlpath $ vo_load_path
-        $ ml_include_path $ ri_from $ delay))
+        $ ml_include_path $ ri_from $ delay $ int_backend))
 
 let main () =
   let ecode = Cmd.eval lsp_cmd in

coq-lsp.opam

@@ -40,5 +40,8 @@ depends: [
   "coq-serapi"   { >= "8.19" < "8.20"  }
 ]
 
-build: [ [ "dune" "build" "-p" name "-j" jobs ] ]
+build: [
+  [ "rm" "-rf" "vendor" ]
+  [ "dune" "build" "-p" name "-j" jobs ]
+]
 run-test: [ [ "dune" "runtest" "-p" name "-j" jobs ] ]

coq/args.ml

@@ -82,3 +82,10 @@ let ri_from : (string option * string) list Term.t =
         value
         & opt_all (pair string string) []
         & info [ "rifrom"; "require-import-from" ] ~docv:"FROM,LIBRARY" ~doc))
+
+let int_backend =
+  let doc = "Select Interruption Backend" in
+  Arg.(
+    value
+    & opt (enum [ ("Coq", Limits.Coq); ("Mp", Limits.Mp) ]) Limits.Coq
+    & info [ "int_backend" ] ~docv:"INT_BACKEND" ~doc)

coq/args.mli

@@ -16,3 +16,4 @@ val debug : Bool.t Term.t
 val bt : Bool.t Term.t
 val ml_include_path : string list Term.t
 val ri_from : (string option * string) list Term.t
+val int_backend : Limits.backend Term.t

coq/init.ml

@@ -97,5 +97,7 @@ let doc_init ~root_state ~workspace ~uri () =
   (* We return the state at this point! *)
   Vernacstate.freeze_full_state () |> State.of_coq
 
-let doc_init ~token ~root_state ~workspace ~uri =
+let doc_init ~token:_ ~root_state ~workspace ~uri =
+  (* Don't interrupt document creation. *)
+  let token = Limits.create_atomic () in
   Protect.eval ~token ~f:(doc_init ~root_state ~workspace ~uri) ()

coq/limits.ml

@@ -46,4 +46,54 @@ module Coq : Intf = struct
 end
 
 module Mp = Limits_mp_impl
-include Coq
+
+type backend =
+  | Coq
+  | Mp
+
+let backend : (module Intf) ref = ref (module Coq : Intf)
+
+let select = function
+  | Coq -> backend := (module Coq)
+  | Mp -> backend := (module Mp)
+
+module Token = struct
+  type t =
+    | C of Coq.Token.t
+    | M of Mp.Token.t
+    | A (* Atomic operation *)
+
+  let create () =
+    let module M = (val !backend) in
+    match M.name with
+    | "memprof-limits" -> M (Mp.Token.create ())
+    | "Control.interrupt" | _ -> C (Coq.Token.create ())
+
+  let set = function
+    | C token -> Coq.Token.set token
+    | M token -> Mp.Token.set token
+    | A -> ()
+
+  let is_set = function
+    | C token -> Coq.Token.is_set token
+    | M token -> Mp.Token.is_set token
+    | A -> false
+end
+
+let create_atomic () = Token.A
+
+let start () =
+  let module M = (val !backend) in
+  M.start ()
+
+let limit ~token ~f x =
+  let module M = (val !backend) in
+  match token with
+  | Token.C token -> Coq.limit ~token ~f x
+  | Token.M token -> Mp.limit ~token ~f x
+  | Token.A ->
+    let () = Control.interrupt := false in
+    Ok (f x)
+
+let name = "select backend"
+let available = true

coq/limits.mli

@@ -17,3 +17,12 @@ end
 module Coq : Intf
 module Mp : Intf
 include Intf
+
+type backend =
+  | Coq
+  | Mp
+
+(** *Must* be called *only* once *)
+val select : backend -> unit
+
+val create_atomic : unit -> Token.t

coq/loader.ml

@@ -80,8 +80,11 @@ let safe_loader loader fl_pkg =
           ++ str "failed" ++ fnl () ++ exn_msg);
     Exninfo.iraise iexn
 
+let default_loader pkgs : unit =
+  Fl_dynload.load_packages ~debug:false pkgs
+
 let plugin_handler user_loader =
-  let loader = Option.default (Fl_dynload.load_packages ~debug:false) user_loader in
+  let loader = Option.default default_loader user_loader in
   let safe_loader = safe_loader loader in
   fun fl_pkg ->
     let _, fl_pkg = Mltop.PluginSpec.repr fl_pkg in