diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 8679846e..4ebc86f2 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -451,7 +451,8 @@ let lsp_init_process ~ofn ~cmdline ~debug msg : Init_effect.t = (* We don't need to interrupt this *) let token = Coq.Limits.Token.create () in Rq.Action.now (Ok result) |> Rq.serve ~ofn ~token ~id; - LIO.logMessage ~lvl:Info ~message:"Server initialized"; + let message = Format.asprintf "Server initializing (int_backend: %s)" (Coq.Limits.name ()) in + LIO.logMessage ~lvl:Info ~message; (* Workspace initialization *) let debug = debug || !Fleche.Config.v.debug in let workspaces = diff --git a/coq/limits.ml b/coq/limits.ml index a6855c6d..cd0c863a 100644 --- a/coq/limits.ml +++ b/coq/limits.ml @@ -10,7 +10,7 @@ module type Intf = sig val start : unit -> unit val limit : token:Token.t -> f:('a -> 'b) -> 'a -> ('b, exn) Result.t - val name : string + val name : unit -> string val available : bool end @@ -41,7 +41,7 @@ module Coq : Intf = struct let () = Control.interrupt := false in try Ok (f x) with Sys.Break -> Error Sys.Break - let name = "Control.interrupt" + let name () = "Control.interrupt" let available = true end @@ -65,7 +65,7 @@ module Token = struct let create () = let module M = (val !backend) in - match M.name with + match M.name () with | "memprof-limits" -> M (Mp.Token.create ()) | "Control.interrupt" | _ -> C (Coq.Token.create ()) @@ -95,5 +95,5 @@ let limit ~token ~f x = let () = Control.interrupt := false in Ok (f x) -let name = "select backend" +let name () = let module M = (val !backend) in M.name () let available = true diff --git a/coq/limits.mli b/coq/limits.mli index 631b4c3a..3f5e3b25 100644 --- a/coq/limits.mli +++ b/coq/limits.mli @@ -10,7 +10,7 @@ module type Intf = sig val start : unit -> unit val limit : token:Token.t -> f:('a -> 'b) -> 'a -> ('b, exn) Result.t - val name : string + val name : unit -> string val available : bool end diff --git a/coq/limits_mp_impl.fake.ml b/coq/limits_mp_impl.fake.ml index 7baeca46..386991fb 100644 --- a/coq/limits_mp_impl.fake.ml +++ b/coq/limits_mp_impl.fake.ml @@ -9,5 +9,5 @@ end let start () = () let limit ~token:_ ~f x = Result.Ok (f x) -let name = "memprof-limits" +let name () = "memprof-limits (fake)" let available = false diff --git a/coq/limits_mp_impl.real.ml b/coq/limits_mp_impl.real.ml index d5c4801f..a3a162ea 100644 --- a/coq/limits_mp_impl.real.ml +++ b/coq/limits_mp_impl.real.ml @@ -7,5 +7,5 @@ let limit ~token ~f x = let f () = f x in Memprof_limits.limit_with_token ~token f -let name = "memprof-limits" +let name () = "memprof-limits" let available = true