From 840ae4553da99e0882174fb7f1de6e22b3e738ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 12 Nov 2024 15:38:58 +0100 Subject: [PATCH] Coqinit split init_runtime to better support having multiple docs cf vscoqtop PR https://github.com/coq/vscoq/pull/945 --- ...26-SkySkimmer-vscoq-multiple-coqproject.sh | 1 + sysinit/coqinit.ml | 25 +++++++++++++------ sysinit/coqinit.mli | 8 +++--- toplevel/coqtop.ml | 5 ++-- 4 files changed, 24 insertions(+), 15 deletions(-) create mode 100644 dev/ci/user-overlays/19826-SkySkimmer-vscoq-multiple-coqproject.sh diff --git a/dev/ci/user-overlays/19826-SkySkimmer-vscoq-multiple-coqproject.sh b/dev/ci/user-overlays/19826-SkySkimmer-vscoq-multiple-coqproject.sh new file mode 100644 index 000000000000..ef9d44a61c8d --- /dev/null +++ b/dev/ci/user-overlays/19826-SkySkimmer-vscoq-multiple-coqproject.sh @@ -0,0 +1 @@ +overlay vscoq https://github.com/SkySkimmer/vscoq vscoq-multiple-coqproject 19826 diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml index 9ad972b07cd1..256a916702c8 100644 --- a/sysinit/coqinit.ml +++ b/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" diff --git a/sysinit/coqinit.mli b/sysinit/coqinit.mli index 009004273a22..f180ec7a3d4f 100644 --- a/sysinit/coqinit.mli +++ b/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) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a21f09bfd881..1f797469f0ef 100644 --- a/toplevel/coqtop.ml +++ b/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 =