[limits] Some refactoring

compiler/cc.ml

@@ -4,5 +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
+  ; token : Limits.Token.t
   }

compiler/driver.ml

@@ -37,7 +37,7 @@ 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 token = Coq.Limits.Token.create () in
+  let token = Limits.Token.create () in
   let workspaces =
     List.map
       (fun dir -> (dir, Coq.Workspace.guess ~token ~cmdline ~debug ~dir))

controller/coq_lsp.ml

@@ -95,7 +95,7 @@ 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 ();
+  Limits.start ();
 
   (* Try to be sane w.r.t. \r\n in Windows *)
   Stdlib.set_binary_mode_in stdin true;

controller/lsp_core.ml

@@ -164,13 +164,13 @@ module Rq : sig
   end
 
   val serve :
-    ofn:(J.t -> unit) -> token:Coq.Limits.Token.t -> id:int -> Action.t -> unit
+    ofn:(J.t -> unit) -> token:Limits.Token.t -> id:int -> Action.t -> unit
 
   val cancel : ofn:(J.t -> unit) -> code:int -> message:string -> int -> unit
 
   val serve_postponed :
        ofn:(J.t -> unit)
-    -> token:Coq.Limits.Token.t
+    -> token:Limits.Token.t
     -> doc:Fleche.Doc.t
     -> Int.Set.t
     -> unit
@@ -428,7 +428,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.create () in
+    let token = Limits.Token.create () in
     Rq.Action.now (Ok result) |> Rq.serve ~ofn ~token ~id;
     LIO.logMessage ~lvl:3 ~message:"Server initialized";
     (* Workspace initialization *)
@@ -528,7 +528,7 @@ let dispatch_message ~io ~ofn ~token ~state (com : LSP.Message.t) : State.t =
 let current_token = ref None
 
 let token_factory () =
-  let token = Coq.Limits.Token.create () in
+  let token = Limits.Token.create () in
   current_token := Some token;
   token
 
@@ -537,7 +537,7 @@ let set_current_token () =
   | None -> ()
   | Some tok ->
     current_token := None;
-    Coq.Limits.Token.set tok
+    Limits.Token.set tok
 
 type 'a cont =
   | Cont of 'a

controller/request.ml

@@ -40,10 +40,10 @@ module R = struct
     | Completed (Ok r) -> r
 end
 
-type document = token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> R.t
+type document = token:Limits.Token.t -> doc:Fleche.Doc.t -> R.t
 
 type position =
-  token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> point:int * int -> R.t
+  token:Limits.Token.t -> doc:Fleche.Doc.t -> point:int * int -> R.t
 
 (** Requests that require data access *)
 module Data = struct

controller/request.mli

@@ -25,10 +25,10 @@ module R : sig
     name:string -> f:('a -> (t, Loc.t) Coq.Protect.E.t) -> 'a -> t
 end
 
-type document = token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> R.t
+type document = token:Limits.Token.t -> doc:Fleche.Doc.t -> R.t
 
 type position =
-  token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> point:int * int -> R.t
+  token:Limits.Token.t -> doc:Fleche.Doc.t -> point:int * int -> R.t
 
 (** Requests that require data access *)
 module Data : sig
@@ -49,7 +49,7 @@ module Data : sig
   (* Debug printing *)
   val data : Format.formatter -> t -> unit
   val dm_request : t -> Lang.LUri.File.t * bool * Fleche.Theory.Request.request
-  val serve : token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> t -> R.t
+  val serve : token:Limits.Token.t -> doc:Fleche.Doc.t -> t -> R.t
 end
 
 (** Returns an empty list of results for any position / document *)

controller/rq_hover.ml

@@ -164,14 +164,14 @@ open Fleche
 module Handler = struct
   (** Returns [Some markdown] if there is some hover to match *)
   type 'node h_node =
-       token:Coq.Limits.Token.t
+       token:Limits.Token.t
     -> contents:Contents.t
     -> point:int * int
     -> node:'node
     -> string option
 
   type h_doc =
-       token:Coq.Limits.Token.t
+       token:Limits.Token.t
     -> doc:Doc.t
     -> point:int * int
     -> node:Doc.Node.t option

controller/rq_hover.mli

@@ -12,14 +12,14 @@ open Fleche
 module Handler : sig
   (** Returns [Some markdown] if there is some hover to match *)
   type 'node h_node =
-       token:Coq.Limits.Token.t
+       token:Limits.Token.t
     -> contents:Contents.t
     -> point:int * int
     -> node:'node
     -> string option
 
   type h_doc =
-       token:Coq.Limits.Token.t
+       token:Limits.Token.t
     -> doc:Doc.t
     -> point:int * int
     -> node:Doc.Node.t option

coq/dune

@@ -6,4 +6,4 @@
  (inline_tests)
  (preprocess
   (pps ppx_compare ppx_hash ppx_inline_test))
- (libraries memprof-limits lang coq-core.vernac coq-serapi.serlib))
+ (libraries lang limits coq-core.vernac coq-serapi.serlib))

coq/limits/dune

@@ -0,0 +1,4 @@
+(library
+ (name limits)
+ (public_name coq-lsp.limits)
+ (libraries memprof-limits coq-core.lib))

coq/limits.ml → coq/limits/limits.ml

@@ -1,14 +1,29 @@
 (* We'd like to move this code to Lang, but it is still too specific *)
 
-module Token = Memprof_limits.Token
+module type Intf = sig
+  module Token : sig
+    type t
 
-let start () = Memprof_limits.start_memprof_limits ()
+    val create : unit -> t
+    val set : t -> unit
+    val is_set : t -> bool
+  end
 
-let limit ~token ~f x =
-  let f () = f x in
-  Memprof_limits.limit_with_token ~token f
+  val start : unit -> unit
+  val limit : token:Token.t -> f:('a -> 'b) -> 'a -> ('b, exn) Result.t
+end
 
-module Flag = struct
+module Memprof : Intf = struct
+  module Token = Memprof_limits.Token
+
+  let start () = Memprof_limits.start_memprof_limits ()
+
+  let limit ~token ~f x =
+    let f () = f x in
+    Memprof_limits.limit_with_token ~token f
+end
+
+module CoqPolling : Intf = struct
   module Token : sig
     type t
 
@@ -35,3 +50,5 @@ module Flag = struct
       let () = Control.interrupt := false in
       try Ok (f x) with Sys.Break -> Error Sys.Break
 end
+
+include Memprof

fleche/doc.ml

@@ -542,7 +542,7 @@ end
    [Node.t] out (yet) *)
 module Recovery : sig
   val handle :
-       token:Coq.Limits.Token.t
+       token:Limits.Token.t
     -> context:Recovery_context.t
     -> st:Coq.State.t
     -> Coq.State.t

fleche/doc.mli

@@ -99,7 +99,7 @@ val diags : t -> Lang.Diagnostic.t list
     suceeds, but the document could be created in a `Failed` state if problems
     arise. *)
 val create :
-     token:Coq.Limits.Token.t
+     token:Limits.Token.t
   -> env:Env.t
   -> uri:Lang.LUri.File.t
   -> version:int
@@ -109,8 +109,7 @@ val create :
 (** Update the contents of a document, updating the right structures for
     incremental checking. If the operation fails, the document will be left in
     `Failed` state. *)
-val bump_version :
-  token:Coq.Limits.Token.t -> version:int -> raw:string -> t -> t
+val bump_version : token:Limits.Token.t -> version:int -> raw:string -> t -> t
 
 (** Checking targets, this specifies what we expect check to reach *)
 module Target : sig
@@ -128,15 +127,15 @@ end
     in the [io] record, used to send partial updates. *)
 val check :
      io:Io.CallBack.t
-  -> token:Coq.Limits.Token.t
+  -> token:Limits.Token.t
   -> target:Target.t
   -> doc:t
   -> unit
   -> t
 
 (** [save ~doc] will save [doc] .vo file. It will fail if proofs are open, or if
     the document completion status is not [Yes] *)
-val save : token:Coq.Limits.Token.t -> doc:t -> (unit, Loc.t) Coq.Protect.E.t
+val save : token:Limits.Token.t -> doc:t -> (unit, Loc.t) Coq.Protect.E.t
 
 (** This is internal, to workaround the Coq multiple-docs problem *)
 val create_failed_permanent :

fleche/info.mli

@@ -53,7 +53,7 @@ module O : S with module P := Offset
 (** We move towards a more modular design here, for preprocessing *)
 module Goals : sig
   val goals :
-       token:Coq.Limits.Token.t
+       token:Limits.Token.t
     -> st:Coq.State.t
     -> (Pp.t Coq.Goals.reified_pp option, Loc.t) Coq.Protect.E.t
 
@@ -62,7 +62,7 @@ end
 
 module Completion : sig
   val candidates :
-       token:Coq.Limits.Token.t
+       token:Limits.Token.t
     -> st:Coq.State.t
     -> string
     -> (string list option, Loc.t) Coq.Protect.E.t

fleche/memo.ml

@@ -115,7 +115,7 @@ module type EvalType = sig
 
   type output
 
-  val eval : token:Coq.Limits.Token.t -> t -> (output, Loc.t) Coq.Protect.E.t
+  val eval : token:Limits.Token.t -> t -> (output, Loc.t) Coq.Protect.E.t
 end
 
 module SEval (E : EvalType) = struct

fleche/memo.mli

@@ -13,18 +13,15 @@ module Init : sig
   (** [size ()] Return the size in words, expensive *)
   val size : unit -> int
 
-  val eval :
-    token:Coq.Limits.Token.t -> t -> (Coq.State.t, Loc.t) Coq.Protect.E.t
+  val eval : token:Limits.Token.t -> t -> (Coq.State.t, Loc.t) Coq.Protect.E.t
 end
 
 module Interp : sig
   type t = Coq.State.t * Coq.Ast.t
 
   (** Interpret a command, possibly memoizing it *)
   val eval :
-       token:Coq.Limits.Token.t
-    -> t
-    -> (Coq.State.t, Loc.t) Coq.Protect.E.t Stats.t
+    token:Limits.Token.t -> t -> (Coq.State.t, Loc.t) Coq.Protect.E.t Stats.t
 
   (** [size ()] Return the size in words, expensive *)
   val size : unit -> int
@@ -38,9 +35,7 @@ module Require : sig
 
   (** Interpret a require, possibly memoizing it *)
   val eval :
-       token:Coq.Limits.Token.t
-    -> t
-    -> (Coq.State.t, Loc.t) Coq.Protect.E.t Stats.t
+    token:Limits.Token.t -> t -> (Coq.State.t, Loc.t) Coq.Protect.E.t Stats.t
 
   (** [size ()] Return the size in words, expensive *)
   val size : unit -> int
@@ -55,8 +50,7 @@ module Admit : sig
   (** [size ()] Return the size in words, expensive *)
   val size : unit -> int
 
-  val eval :
-    token:Coq.Limits.Token.t -> t -> (Coq.State.t, Loc.t) Coq.Protect.E.t
+  val eval : token:Limits.Token.t -> t -> (Coq.State.t, Loc.t) Coq.Protect.E.t
 end
 
 module CacheStats : sig

fleche/theory.ml

@@ -139,14 +139,14 @@ let diags_of_doc doc = List.concat_map Doc.Node.diags doc.Doc.nodes
    general structure *)
 module Register : sig
   module Completed : sig
-    type t = io:Io.CallBack.t -> token:Coq.Limits.Token.t -> doc:Doc.t -> unit
+    type t = io:Io.CallBack.t -> token:Limits.Token.t -> doc:Doc.t -> unit
   end
 
   val add : Completed.t -> unit
-  val fire : io:Io.CallBack.t -> token:Coq.Limits.Token.t -> doc:Doc.t -> unit
+  val fire : io:Io.CallBack.t -> token:Limits.Token.t -> doc:Doc.t -> unit
 end = struct
   module Completed = struct
-    type t = io:Io.CallBack.t -> token:Coq.Limits.Token.t -> doc:Doc.t -> unit
+    type t = io:Io.CallBack.t -> token:Limits.Token.t -> doc:Doc.t -> unit
   end
 
   let callback : Completed.t list ref = ref []
@@ -175,7 +175,7 @@ module Check : sig
   val deschedule : uri:Lang.LUri.File.t -> unit
 
   val maybe_check :
-    io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option
+    io:Io.CallBack.t -> token:Limits.Token.t -> (Int.Set.t * Doc.t) option
 end = struct
   let pending = ref []
 

fleche/theory.mli

@@ -20,13 +20,13 @@ module Check : sig
       [Some rqs] the list of requests ready to execute after the check. Sends
       progress and diagnostics notifications using output function [ofn]. *)
   val maybe_check :
-    io:Io.CallBack.t -> token:Coq.Limits.Token.t -> (Int.Set.t * Doc.t) option
+    io:Io.CallBack.t -> token:Limits.Token.t -> (Int.Set.t * Doc.t) option
 end
 
 (** Create a document inside a theory *)
 val create :
      io:Io.CallBack.t
-  -> token:Coq.Limits.Token.t
+  -> token:Limits.Token.t
   -> env:Doc.Env.t
   -> uri:Lang.LUri.File.t
   -> raw:string
@@ -36,7 +36,7 @@ val create :
 (** Update a document inside a theory, returns the list of not valid requests *)
 val change :
      io:Io.CallBack.t
-  -> token:Coq.Limits.Token.t
+  -> token:Limits.Token.t
   -> uri:Lang.LUri.File.t
   -> version:int
   -> raw:string
@@ -77,7 +77,7 @@ end
 (* Experimental plugin API, not stable yet *)
 module Register : sig
   module Completed : sig
-    type t = io:Io.CallBack.t -> token:Coq.Limits.Token.t -> doc:Doc.t -> unit
+    type t = io:Io.CallBack.t -> token:Limits.Token.t -> doc:Doc.t -> unit
   end
 
   val add : Completed.t -> unit