[coq] Adapt Coq.Protect interface to incorporate an interruption to…

…ken.

- We now conditionally depend on `memprof-limits` on OCaml 4.x
- Each call that can be interrupted now additionally takes 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,8 @@
  (inline_tests)
  (preprocess
   (pps ppx_compare ppx_hash ppx_inline_test))
- (libraries lang coq-core.vernac coq-serapi.serlib))
+ (libraries
+  (select limits.ml from
+   (memprof-limits -> limits.mp.ml)
+   (!memprof-limits -> limits.dummy.ml))
+   lang coq-core.vernac coq-serapi.serlib))

coq/limits.dummy.ml

@@ -0,0 +1,10 @@
+module Token = struct
+  type t = bool ref
+  let create () = ref false
+  let set r = r := true
+  let is_set r = !r
+end
+
+let start () = ()
+
+let limit_with_token ~token:_ f = Result.Ok (f ())

coq/limits.mli

@@ -0,0 +1,12 @@
+(* This is a wrapper for the memprof-limits lib, as it is not
+   available in most setups *)
+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_with_token : token:Token.t -> (unit -> 'a) -> ('a, exn) Result.t

coq/limits.mp.ml

@@ -0,0 +1,5 @@
+module Token = Memprof_limits.Token
+
+let start = Memprof_limits.start_memprof_limits
+
+let limit_with_token = Memprof_limits.limit_with_token