From eb78a8a365790f46f779b257723afef97d06ad2b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 12 Nov 2024 15:40:20 +0100 Subject: [PATCH] Support per-file _CoqProject cf https://github.com/coq/coq/pull/19826 --- language-server/dm/vscoqtop_proof_worker.ml | 6 ++- language-server/dm/vscoqtop_tactic_worker.ml | 6 ++- language-server/tests/common.ml | 4 +- language-server/vscoqtop/lspManager.ml | 43 ++++++++++++++++---- language-server/vscoqtop/lspManager.mli | 2 +- language-server/vscoqtop/vscoqtop.ml | 12 +++--- 6 files changed, 54 insertions(+), 19 deletions(-) diff --git a/language-server/dm/vscoqtop_proof_worker.ml b/language-server/dm/vscoqtop_proof_worker.ml index 5183e0c6..04e8b92d 100644 --- a/language-server/dm/vscoqtop_proof_worker.ml +++ b/language-server/dm/vscoqtop_proof_worker.ml @@ -54,8 +54,10 @@ let _ = let () = Coqinit.init_ocaml (); let opts, emoptions = Coqinit.parse_arguments ~parse_extra:Dm.ExecutionManager.ProofWorkerProcess.parse_options (List.tl (Array.to_list Sys.argv)) in - let injections = Coqinit.init_runtime ~usage:vscoqtop_specific_usage opts in - start_library (Coqinit.dirpath_of_top opts.config.logic.toplevel_name) injections; + let () = Coqinit.init_runtime ~usage:vscoqtop_specific_usage opts in + (* not sure if init_document is useful in proof worker *) + let () = Coqinit.init_document opts in + start_library (Coqinit.dirpath_of_top opts.config.logic.toplevel_name) []; log @@ "started"; Sys.(set_signal sigint Signal_ignore); main_worker emoptions diff --git a/language-server/dm/vscoqtop_tactic_worker.ml b/language-server/dm/vscoqtop_tactic_worker.ml index 4886b757..69552393 100644 --- a/language-server/dm/vscoqtop_tactic_worker.ml +++ b/language-server/dm/vscoqtop_tactic_worker.ml @@ -53,8 +53,10 @@ let () = let () = Coqinit.init_ocaml (); let opts, emoptions = Coqinit.parse_arguments ~parse_extra:Dm.ParTactic.TacticWorkerProcess.parse_options (List.tl (Array.to_list Sys.argv)) in - let injections = Coqinit.init_runtime ~usage:vscoqtop_specific_usage opts in - start_library (Coqinit.dirpath_of_top opts.config.logic.toplevel_name) injections; + let () = Coqinit.init_runtime ~usage:vscoqtop_specific_usage opts in + (* not sure if init_document is useful in tactic worker *) + let () = Coqinit.init_document opts in + start_library (Coqinit.dirpath_of_top opts.config.logic.toplevel_name) []; log @@ "started"; Sys.(set_signal sigint Signal_ignore); main_worker ~opts emoptions () diff --git a/language-server/tests/common.ml b/language-server/tests/common.ml index 82ec6f2e..b8d2b100 100644 --- a/language-server/tests/common.ml +++ b/language-server/tests/common.ml @@ -29,7 +29,9 @@ let injections = Coqinit.init_ocaml (); let opts, _ = Coqargs.parse_args ~init:Coqargs.default [] in let usage = Boot.Usage.{executable_name = ""; extra_args = ""; extra_options = ""} in - Coqinit.init_runtime ~usage opts + Coqinit.init_runtime ~usage opts; + Coqinit.init_document opts; + Coqargs.injection_commands opts [%%endif] let init_state = Vernacstate.freeze_full_state () diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index d9e4f4d4..446e4ce6 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -23,7 +23,7 @@ open Protocol.ExtProtocol module CompactedDecl = Context.Compacted.Declaration -let init_state : (Vernacstate.t * Coqargs.injection_command list) option ref = ref None +let init_state : Vernacstate.t option ref = ref None let get_init_state () = match !init_state with | Some st -> st @@ -256,10 +256,39 @@ let reset_observe_ids = in Hashtbl.fold reset_doc_observe_id states +[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"] +(* in these coq versions init_runtime called globally for the process includes init_document + this means in these versions we do not support local _CoqProject except for the effect on injections + (eg -noinit) *) +let init_document _ vst = vst +[%%else] +let init_document local_args vst = + let () = Vernacstate.unfreeze_full_state vst in + let () = Coqinit.init_document local_args in + Vernacstate.freeze_full_state () +[%%endif] + let open_new_document uri text = - let vst, opts = get_init_state () in + let vst = get_init_state () in + + let local_args = + let fname = DocumentUri.to_path uri in + let dir = Filename.dirname fname in + match CoqProject_file.find_project_file ~from:dir ~projfile_name:"_CoqProject" with + | None -> + log (Printf.sprintf "No project file found for %s" fname); + Coqargs.default + | Some f -> + let project = CoqProject_file.read_project_file ~warning_fn:(fun _ -> ()) f in + let args = CoqProject_file.coqtop_args_from_project project in + log (Printf.sprintf "Arguments from project file %s: %s" f (String.concat " " args)); + fst @@ Coqargs.parse_args ~init:Coqargs.default args + in + + let vst = init_document local_args vst in + let observe_id = if !check_mode = Settings.Mode.Continuous then None else Some Dm.DocumentManager.Top in - let st, events = try Dm.DocumentManager.init vst ~opts uri ~text observe_id with + let st, events = try Dm.DocumentManager.init vst ~opts:(Coqargs.injection_commands local_args) uri ~text observe_id with e -> raise e in let (st, events') = @@ -330,7 +359,7 @@ let consider_purge_invisible_tabs () = let usage = current_memory_usage () in if usage > !max_memory_usage (* 4G *) then begin purge_invisible_tabs (); - let vst, _ = get_init_state () in + let vst = get_init_state () in Vernacstate.unfreeze_full_state vst; Vernacstate.Interp.invalidate_cache (); Gc.compact (); @@ -737,6 +766,6 @@ let pr_event = function | SendMoveCursor _ -> Pp.str"move cursor" | SendBlockOnError _ -> Pp.str"block on error" -let init injections = - init_state := Some (Vernacstate.freeze_full_state (), injections); - [lsp] \ No newline at end of file +let init () = + init_state := Some (Vernacstate.freeze_full_state ()); + [lsp] diff --git a/language-server/vscoqtop/lspManager.mli b/language-server/vscoqtop/lspManager.mli index 5aed1f35..8a5c0557 100644 --- a/language-server/vscoqtop/lspManager.mli +++ b/language-server/vscoqtop/lspManager.mli @@ -18,4 +18,4 @@ type events = event Sel.Event.t list val handle_event : event -> events val pr_event : event -> Pp.t -val init : Coqargs.injection_command list -> event Sel.Event.t list \ No newline at end of file +val init : unit -> event Sel.Event.t list diff --git a/language-server/vscoqtop/vscoqtop.ml b/language-server/vscoqtop/vscoqtop.ml index 1a3c762a..80f93f37 100644 --- a/language-server/vscoqtop/vscoqtop.ml +++ b/language-server/vscoqtop/vscoqtop.ml @@ -17,8 +17,8 @@ let Dm.Types.Log log = Dm.Log.mk_log "top" -let loop injections = - let events = LspManager.init injections in +let loop () = + let events = LspManager.init () in let rec loop (todo : LspManager.event Sel.Todo.t) = (*log @@ "looking for next step";*) flush_all (); @@ -75,10 +75,10 @@ let _ = log (Printf.sprintf "Arguments from project file %s: %s" f (String.concat " " args)); fst @@ Coqargs.parse_args ~usage:vscoqtop_specific_usage ~init:Coqargs.default args in let opts, () = Coqinit.parse_arguments ~usage:vscoqtop_specific_usage ~initial_args ~parse_extra () in - let injections = Coqinit.init_runtime opts in + let _injections = Coqinit.init_runtime opts in Safe_typing.allow_delayed_constants := true; (* Needed to delegate or skip proofs *) Sys.(set_signal sigint Signal_ignore); - loop injections + loop () [%%else] let parse_extra _ x = skip_xd [] x @@ -97,8 +97,8 @@ let () = log (Printf.sprintf "Arguments from project file %s: %s" f (String.concat " " args)); fst @@ Coqargs.parse_args ~init:Coqargs.default args in let opts, () = Coqinit.parse_arguments ~initial_args ~parse_extra (List.tl (Array.to_list Sys.argv)) in - let injections = Coqinit.init_runtime ~usage:vscoqtop_specific_usage opts in + let () = Coqinit.init_runtime ~usage:vscoqtop_specific_usage opts in Safe_typing.allow_delayed_constants := true; (* Needed to delegate or skip proofs *) Sys.(set_signal sigint Signal_ignore); - loop injections + loop () [%%endif]