Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[coq] Don't expose feedback to clients. #451

Merged
merged 1 commit into from
Mar 6, 2023
Merged

[coq] Don't expose feedback to clients. #451

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 3 additions & 23 deletions controller/coq_lsp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,28 +60,10 @@ let lsp_cb =
Lsp.JFleche.mk_progress ~uri ~version progress |> ofn)
}

let lvl_to_severity (lvl : Feedback.level) =
match lvl with
| Feedback.Debug -> 5
| Feedback.Info -> 4
| Feedback.Notice -> 3
| Feedback.Warning -> 2
| Feedback.Error -> 1

let add_message lvl loc msg q =
let lvl = lvl_to_severity lvl in
q := (loc, lvl, msg) :: !q

let mk_fb_handler q Feedback.{ contents; _ } =
match contents with
| Message (lvl, loc, msg) -> add_message lvl loc msg q
| _ -> ()

let coq_init ~fb_queue ~debug =
let fb_handler = mk_fb_handler fb_queue in
let coq_init ~debug =
let load_module = Dynlink.loadfile in
let load_plugin = Coq.Loader.plugin_handler None in
Coq.Init.(coq_init { fb_handler; debug; load_module; load_plugin })
Coq.Init.(coq_init { debug; load_module; load_plugin })

let exit_notification =
Lsp.Base.Message.(Notification { method_ = "exit"; params = [] })
Expand Down Expand Up @@ -111,10 +93,8 @@ let lsp_main bt coqcorelib coqlib ocamlpath vo_load_path ml_include_path =
initialize is received *)

(* Core Coq initialization *)
let fb_queue = Coq.Protect.fb_queue in

let debug = bt || Fleche.Debug.backtraces in
let root_state = coq_init ~fb_queue ~debug in
let root_state = coq_init ~debug in
let cmdline =
{ Coq.Workspace.CmdLine.coqcorelib
; coqlib
Expand Down
24 changes: 20 additions & 4 deletions coq/init.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,14 +19,29 @@
(**************************************************************************)

type coq_opts =
{ fb_handler : Feedback.feedback -> unit
(** callback to handle async feedback *)
; load_module : string -> unit (** callback to load cma/cmo files *)
{ load_module : string -> unit (** callback to load cma/cmo files *)
; load_plugin : Mltop.PluginSpec.t -> unit
(** callback to load findlib packages *)
; debug : bool (** Enable Coq Debug mode *)
}

let lvl_to_severity (lvl : Feedback.level) =
match lvl with
| Feedback.Debug -> 5
| Feedback.Info -> 4
| Feedback.Notice -> 3
| Feedback.Warning -> 2
| Feedback.Error -> 1

let add_message lvl loc msg q =
let lvl = lvl_to_severity lvl in
q := (loc, lvl, msg) :: !q

let mk_fb_handler q Feedback.{ contents; _ } =
match contents with
| Message (lvl, loc, msg) -> add_message lvl loc msg q
| _ -> ()

let coq_init opts =
(* Core Coq initialization *)
Lib.init ();
Expand All @@ -40,7 +55,8 @@ let coq_init opts =
(**************************************************************************)

(* Initialize logging. *)
ignore (Feedback.add_feeder opts.fb_handler);
let fb_handler = mk_fb_handler Protect.fb_queue in
ignore (Feedback.add_feeder fb_handler);

(* SerAPI plugins *)
let load_plugin = opts.load_plugin in
Expand Down
4 changes: 1 addition & 3 deletions coq/init.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,7 @@
(**************************************************************************)

type coq_opts =
{ fb_handler : Feedback.feedback -> unit
(** callback to handle async feedback *)
; load_module : string -> unit (** callback to load cma/cmo files *)
{ load_module : string -> unit (** callback to load cma/cmo files *)
; load_plugin : Mltop.PluginSpec.t -> unit
(** callback to load findlib packages *)
; debug : bool (** Enable Coq Debug mode *)
Expand Down