Merge pull request #945 from SkySkimmer/vscoq-multiple-coqproject

Support per-file _CoqProject

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

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 ()

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 ()

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]
+let init () =
+  init_state := Some (Vernacstate.freeze_full_state ());
+  [lsp]

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
+val init : unit -> event Sel.Event.t list

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]