[coq] Preliminary support for memprof_limits token-based interruption

controller/coq_lsp.ml

@@ -88,6 +88,8 @@ 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 delay =
+  Memprof_limits.start_memprof_limits ();
+
   (* 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;

controller/lsp_core.ml

@@ -367,7 +367,7 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t =
     LIO.logMessage ~lvl:3 ~message;
     let result, dirs = Rq_init.do_initialize ~params in
     (* We don't need to interrupt this *)
-    let token = Coq.Limits.Token.make () in
+    let token = Coq.Limits.Token.create () in
     Rq.Action.now (Ok result) |> Rq.serve ~ofn ~token ~id;
     LIO.logMessage ~lvl:3 ~message:"Server initialized";
     (* Workspace initialization *)
@@ -463,7 +463,7 @@ let dispatch_message ~ofn ~token ~state (com : LSP.Message.t) : State.t =
 let current_token = ref None
 
 let token_factory () =
-  let token = Coq.Limits.Token.make () in
+  let token = Coq.Limits.Token.create () in
   current_token := Some token;
   token
 

coq/dune

@@ -3,4 +3,4 @@
  (public_name coq-lsp.coq)
  ; Unfortunate we have to link the STM due to the LTAC plugin
  ; depending on it, we should fix this upstream
- (libraries lang coq-core.vernac coq-core.stm coq-serapi.serlib))
+ (libraries memprof-limits lang coq-core.vernac coq-core.stm coq-serapi.serlib))

coq/limits.ml

@@ -1,15 +1,22 @@
 (* We'd like to move this code to Lang, but it is still too specific *)
 
+module Token = Memprof_limits.Token
+
+let limit ~token ~f x =
+  let f () = f x in
+  Memprof_limits.limit_with_token ~token f
+
+module Flag = struct
 module Token : sig
   type t
 
-  val make : unit -> t
+  val create : unit -> t
   val set : t -> unit
   val is_set : t -> bool
 end = struct
   type t = bool ref
 
-  let make () = ref false
+  let create () = ref false
   let set t =
     t := true;
     Control.interrupt := true
@@ -25,3 +32,4 @@ let limit ~token ~f x =
       Ok (f x)
     with Sys.Break ->
       Error Sys.Break
+end