diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index d7a1e9e4c..996daaeec 100644 --- a/.github/workflows/build.yml +++ b/.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 diff --git a/CHANGES.md b/CHANGES.md index ec0986a1f..72cfd9ec2 100644 --- a/CHANGES.md +++ b/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 ----------------------------- diff --git a/coq-lsp.opam b/coq-lsp.opam index 6e2f3ca1b..09b567941 100644 --- a/coq-lsp.opam +++ b/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 diff --git a/coq/dune b/coq/dune index 70893e102..307f9a785 100644 --- a/coq/dune +++ b/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)) diff --git a/coq/limits.ml b/coq/limits.ml new file mode 100644 index 000000000..7bfbf0be4 --- /dev/null +++ b/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 diff --git a/coq/limits.mli b/coq/limits.mli new file mode 100644 index 000000000..1fea90e10 --- /dev/null +++ b/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 diff --git a/coq/limits_mp_impl.fake.ml b/coq/limits_mp_impl.fake.ml new file mode 100644 index 000000000..2848d73c7 --- /dev/null +++ b/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 diff --git a/coq/limits_mp_impl.real.ml b/coq/limits_mp_impl.real.ml new file mode 100644 index 000000000..d5c4801fc --- /dev/null +++ b/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