Merge pull request #685 from ejgallego/limits_select

[limits] Allow to select interruption backend at startup.

CHANGES.md

@@ -91,8 +91,10 @@
    `--max_errors=0` to imitate `coqc` behavior (@ejgallego, #680)
  - Fix `fcc` exit status when checking terminates with fatal errors
    (@ejgallego, @Alizter, #680)
- - Fix (@ejgallego, #683, fixes #682, cc #479 #488, thanks to
-   @Hazardouspeach for the report)
+ - 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
 -----------------------------

compiler/driver.ml

@@ -35,7 +35,7 @@ let apply_config ~max_errors =
     (fun max_errors -> Fleche.Config.v := { !Fleche.Config.v with max_errors })
     max_errors
 
-let go args =
+let go ~int_backend args =
   let { Args.cmdline; roots; display; debug; files; plugins; max_errors } =
     args
   in
@@ -47,6 +47,8 @@ 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

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 max_errors =
+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
@@ -21,10 +21,9 @@ let fcc_main roots display debug plugins files coqlib coqcorelib ocamlpath
   let args =
     Args.{ cmdline; roots; display; files; debug; plugins; max_errors }
   in
-  Driver.go args
+  Driver.go ~int_backend args
 
 (****************************************************************************)
-
 (* Specific to fcc *)
 let roots : string list Term.t =
   let doc = "Workspace(s) root(s)" in
@@ -94,9 +93,9 @@ let fcc_cmd : int 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
-      $ max_errors)
+      const fcc_main $ int_backend $ roots $ display $ debug $ plugins $ file
+      $ coqlib $ coqcorelib $ ocamlpath $ rload_paths $ qload_paths $ ri_from
+      $ no_vo $ max_errors)
   in
   let exits = Exit_codes.[ fatal; stopped; scheduled; uri_failed ] in
   Cmd.(v (Cmd.info "fcc" ~exits ~version ~doc ~man) fcc_term)

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/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

etc/doc/USER_MANUAL.md

@@ -0,0 +1,49 @@
+# `coq-lsp` user manual
+
+Welcome to `coq-lsp` in-progress user-manual.
+
+Please see also `coq-lsp` FAQ.
+
+## First steps with `coq-lsp`
+
+`coq-lsp` is designed to work on a project-basis, that is to say, the
+user should point to the _root_ of their project (for example using
+"Open Folder" in VSCode).
+
+Given a project root `dir`, `coq-lsp` will try to read
+`$dir/_CoqProject` and will apply the settings for your project from
+there.
+
+Other tools included in the `coq-lsp` suite usually take a
+`--root=dir` command line parameter to set this information.
+
+`coq-lsp` will display information about the project root and setting
+auto-detection using the standard language server protocol messaging
+facilities. In VSCode, these settings can be usually displayed in the
+"Output > Coq-lsp server" window.
+
+## Selecting the interruption backend
+
+When a Coq document is being checked, it is often necessary to
+_interrupt_ the checking process, for example, to check a new version,
+or to retrieve some user-facing information.
+
+`coq-lsp` supports two interruption methods, selectable at start time
+via the `--int_backend` command-line parameter:
+
+- Coq-side polling (`--int_backend=Coq`, default): in this mode, Coq
+  polls for a flag every once in a while, and will raise an
+  interruption when the flag is set. This method has the downside that
+  some paths in Coq don't check the flag often enough, for example,
+  `Qed.`, so users may face unresponsiveness, as our server can only
+  run one thread at a time.
+
+- `memprof-limits` token-based interruption (`--int_backend=Mp`,
+  experimental): in this mode, Coq will use the `memprof-limits`
+  library to interrupt Coq.
+
+Coq has some bugs w.r.t. handling of asynchronous interruptions coming
+from `memprof-limits`. The situation is better in Coq 8.20, but users
+on Coq <= 8.19 do need to install a version of Coq with the backported
+fixes. See the information about Coq upstream bugs in the README for
+more information about available branches.