Skip to content

Commit

Permalink
[limits] Display chosen backend on server init message.
Browse files Browse the repository at this point in the history
  • Loading branch information
ejgallego committed May 10, 2024
1 parent 00aaae8 commit 1b884fc
Show file tree
Hide file tree
Showing 5 changed files with 9 additions and 8 deletions.
3 changes: 2 additions & 1 deletion controller/lsp_core.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
8 changes: 4 additions & 4 deletions coq/limits.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand All @@ -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 ())

Expand Down Expand Up @@ -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
2 changes: 1 addition & 1 deletion coq/limits.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion coq/limits_mp_impl.fake.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion coq/limits_mp_impl.real.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 1b884fc

Please sign in to comment.