[coq] Add Coq.Limits interface to incorporate an interruption token.

- We now conditionally depend on `memprof-limits` on OCaml 4.x
- Each call that can be interrupted now additionally can take a `Token.t`

There is still more work to be done so this can be properly used.

cc: #509

.github/workflows/build.yml

@@ -36,8 +36,6 @@ jobs:
             ocaml: 4.13.x
           - os: ubuntu-latest
             ocaml: 4.12.x
-          - os: ubuntu-latest
-            ocaml: 4.11.x
           - os: ubuntu-latest
             ocaml: 5.0.x
           - os: ubuntu-latest

CHANGES.md

@@ -51,6 +51,9 @@
  - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
    step. `.vo` saving is now an `fcc` plugins, but for now, it is
    enabled by default (@ejgallego, #650)
+ - depend on `memprof-limits` on OCaml 4.x (@ejgallego, #660)
+ - bump minimal OCaml version to 4.12 due to `memprof-limits`
+   (@ejgallego, #660)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

coq-lsp.opam

@@ -18,7 +18,9 @@ license: "LGPL-2.1-or-later"
 doc: "https://ejgallego.github.io/coq-lsp/"
 
 depends: [
-  "ocaml"        { >= "4.11.0" }
+
+  ("ocaml" {>= "5.0"} | ("ocaml" {<= "5.0"} & "memprof-limits" { >= "0.2.1" } ))
+
   "dune"         { >= "3.13.0" } # Version interval [3.8-3.12] was
                                  # broken for composed builds with Coq
 

coq/dune

@@ -6,4 +6,12 @@
  (inline_tests)
  (preprocess
   (pps ppx_compare ppx_hash ppx_inline_test))
- (libraries lang coq-core.vernac coq-serapi.serlib))
+ (libraries
+  (select
+   limits_mp_impl.ml
+   from
+   (memprof-limits -> limits_mp_impl.real.ml)
+   (!memprof-limits -> limits_mp_impl.fake.ml))
+  lang
+  coq-core.vernac
+  coq-serapi.serlib))

coq/limits.ml

@@ -0,0 +1,48 @@
+(* This is a wrapper for memprof-limits libs *)
+module type Intf = sig
+  module Token : sig
+    type t
+
+    val create : unit -> t
+    val set : t -> unit
+    val is_set : t -> bool
+  end
+
+  val start : unit -> unit
+  val limit : token:Token.t -> f:('a -> 'b) -> 'a -> ('b, exn) Result.t
+  val name : string
+  val available : bool
+end
+
+module Coq : Intf = struct
+  module Token : sig
+    type t
+
+    val create : unit -> t
+    val set : t -> unit
+    val is_set : t -> bool
+  end = struct
+    type t = bool ref
+
+    let create () = ref false
+
+    let set t =
+      t := true;
+      Control.interrupt := true
+
+    let is_set t = !t
+  end
+
+  let start () = ()
+
+  let limit ~token ~f x =
+    if Token.is_set token then Error Sys.Break
+    else
+      let () = Control.interrupt := false in
+      try Ok (f x) with Sys.Break -> Error Sys.Break
+
+  let name = "Control.interrupt"
+  let available = true
+end
+
+module Mp = Limits_mp_impl

coq/limits.mli

@@ -0,0 +1,18 @@
+(* This is a wrapper for memprof-limits libs *)
+module type Intf = sig
+  module Token : sig
+    type t
+
+    val create : unit -> t
+    val set : t -> unit
+    val is_set : t -> bool
+  end
+
+  val start : unit -> unit
+  val limit : token:Token.t -> f:('a -> 'b) -> 'a -> ('b, exn) Result.t
+  val name : string
+  val available : bool
+end
+
+module Coq : Intf
+module Mp : Intf

coq/limits_mp_impl.fake.ml

@@ -0,0 +1,13 @@
+(* We'd like to move this code to Lang, but it is still too specific *)
+module Token = struct
+  type t = unit
+
+  let create () = ()
+  let set () = ()
+  let is_set _ = false
+end
+
+let start () = ()
+let limit ~token ~f x = Result.Ok (f x)
+let name = "memprof-limits"
+let available = false

coq/limits_mp_impl.real.ml

@@ -0,0 +1,11 @@
+(* We'd like to move this code to Lang, but it is still too specific *)
+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
+
+let name = "memprof-limits"
+let available = true