Coqinit split init_runtime to better support having multiple docs

cf vscoqtop PR coq/vscoq#945

dev/ci/user-overlays/19826-SkySkimmer-vscoq-multiple-coqproject.sh

@@ -0,0 +1 @@
+overlay vscoq https://github.com/SkySkimmer/vscoq vscoq-multiple-coqproject 19826

sysinit/coqinit.ml

@@ -155,7 +155,6 @@ let init_load_paths opts =
   let ml_path = opts.pre.ml_includes @ boot_ml_path in
   List.iter Mltop.add_ml_dir (List.rev ml_path);
   List.iter Loadpath.add_vo_path boot_vo_path;
-  List.iter (fun x -> Loadpath.add_vo_path @@ to_vo_path x) opts.pre.vo_includes;
   let env_ocamlpath =
     try [Sys.getenv "OCAMLPATH"]
     with Not_found -> []
@@ -184,6 +183,21 @@ let init_runtime ~usage opts =
   (* excluded directories *)
   List.iter System.exclude_directory opts.config.exclude_dirs;
 
+  (* Paths for loading stuff *)
+  init_load_paths opts;
+
+  match opts.Coqargs.main with
+  | Coqargs.Queries q -> List.iter (print_query ~usage) q; exit 0
+  | Coqargs.Run -> ()
+
+let init_document opts =
+  let open Coqargs in
+
+  (* this isn't in init_load_paths because processes (typically
+     vscoqtop) are allowed to have states with differing vo paths (but
+     not with differing -boot or ml paths) *)
+  List.iter (fun x -> Loadpath.add_vo_path @@ to_vo_path x) opts.pre.vo_includes;
+
   (* Kernel configuration *)
   Global.set_impredicative_set opts.config.logic.impredicative_set;
   Global.set_indices_matter opts.config.logic.indices_matter;
@@ -192,6 +206,7 @@ let init_runtime ~usage opts =
   Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
   Global.set_rewrite_rules_allowed opts.config.logic.rewrite_rules;
 
+  (* XXX these flags should probably be in the summary *)
   (* Native output dir *)
   Nativelib.output_dir := opts.config.native_output_dir;
   Nativelib.include_dirs := opts.config.native_include_dirs;
@@ -213,13 +228,7 @@ let init_runtime ~usage opts =
     Flags.make_warn false;
   end;
 
-  (* Paths for loading stuff *)
-  init_load_paths opts;
-
-  match opts.Coqargs.main with
-  | Coqargs.Queries q -> List.iter (print_query ~usage) q; exit 0
-  | Coqargs.Run ->
-      injection_commands opts
+  ()
 
 let warn_require_not_found =
   CWarnings.create ~name:"compatibility-module-not-found"

sysinit/coqinit.mli

@@ -46,12 +46,10 @@ val parse_arguments :
     compilation. If Coq is used to process multiple libraries, what is set up
     here is really global and common to all of them.
 
-    The returned injections are options (as in "Set This Thing" or "Require
-    that") as specified on the command line.
-    The prelude is one of these (unless "-nois" is passed).
-
     This API must be called, typically jsut after parsing arguments. *)
-val init_runtime : usage:Boot.Usage.specific_usage -> Coqargs.t -> Coqargs.injection_command list
+val init_runtime : usage:Boot.Usage.specific_usage -> Coqargs.t -> unit
+
+val init_document : Coqargs.t -> unit
 
 (** 4 Start a library (sets options and loads objects like the prelude)
 

toplevel/coqtop.ml

@@ -60,10 +60,11 @@ let init_toplevel { parse_extra; init_extra; usage; initial_args } args =
   Coqinit.init_ocaml ();
   let opts, customopts = Coqinit.parse_arguments ~parse_extra ~initial_args args in
   Stm.init_process (snd customopts);
-  let injections = Coqinit.init_runtime ~usage opts in
+  let () = Coqinit.init_runtime ~usage opts in
+  let () = Coqinit.init_document opts in
   (* This state will be shared by all the documents *)
   Stm.init_core ();
-  let customstate = init_extra ~opts customopts injections in
+  let customstate = init_extra ~opts customopts (Coqargs.injection_commands opts) in
   opts, customopts, customstate
 
 let start_coq custom args =