[coq] Preliminary support for memprof_limits token-based interruption

compiler/cc.ml

@@ -4,4 +4,5 @@ type t =
   ; workspaces : (string * (Coq.Workspace.t, string) Result.t) list
   ; default : Coq.Workspace.t
   ; io : Fleche.Io.CallBack.t
+  ; token : Coq.Limits.Token.t
   }

compiler/compile.ml

@@ -25,7 +25,7 @@ let save_diags_file ~(doc : Fleche.Doc.t) =
   Util.format_to_file ~file ~f:Output.pp_diags diags
 
 let compile_file ~cc file =
-  let { Cc.io; root_state; workspaces; default } = cc in
+  let { Cc.io; root_state; workspaces; default; token } = cc in
   let lvl = Io.Level.info in
   let message = Format.asprintf "compiling file %s@\n%!" file in
   io.message ~lvl ~message;
@@ -35,7 +35,6 @@ let compile_file ~cc file =
     let workspace = workspace_of_uri ~io ~workspaces ~uri ~default in
     let env = Doc.Env.make ~init:root_state ~workspace in
     let raw = Util.input_all file in
-    let token = Coq.Limits.Token.create () in
     let () = Theory.create ~io ~token ~env ~uri ~raw ~version:1 in
     match Theory.Check.maybe_check ~io ~token with
     | None -> ()

compiler/driver.ml

@@ -37,14 +37,15 @@ 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.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 cc = Cc.{ root_state; workspaces; default; io } in
+  let cc = Cc.{ root_state; workspaces; default; io; token } in
   (* Initialize plugins *)
   plugin_init plugins;
   Compile.compile ~cc files

controller/coq_lsp.ml

@@ -95,6 +95,8 @@ let rec lsp_init_loop ~ifn ~ofn ~cmdline ~debug =
 
 let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path
     require_libraries delay =
+  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;

coq/limits.ml

@@ -46,5 +46,4 @@ module Coq : Intf = struct
 end
 
 module Mp = Limits_mp_impl
-
-include Coq
+include Mp

coq/limits.mli

@@ -16,5 +16,4 @@ end
 
 module Coq : Intf
 module Mp : Intf
-
 include Intf