diff options
| -rw-r--r-- | doc/changelog/07-commands-and-options/11617-toplevel+boot.rst | 5 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 5 | ||||
| -rw-r--r-- | toplevel/coqargs.mli | 1 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 2 | ||||
| -rw-r--r-- | toplevel/usage.ml | 3 |
6 files changed, 17 insertions, 7 deletions
diff --git a/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst new file mode 100644 index 0000000000..49dd0ee2d8 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst @@ -0,0 +1,5 @@ +- **Added:** + New ``coqc`` / ``coqtop`` option ``-boot`` that will not bind the + `Coq` library prefix by default + (`#11617 <https://github.com/coq/coq/pull/11617>`_, + by Emilio Jesus Gallego Arias). diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 506a8dc5b0..2b79bff1b2 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -64,6 +64,7 @@ type coqargs_config = { } type coqargs_pre = { + boot : bool; load_init : bool; load_rcfile : bool; @@ -131,6 +132,7 @@ let default_config = { } let default_pre = { + boot = false; load_init = true; load_rcfile = true; ml_includes = []; @@ -512,6 +514,7 @@ let parse_args ~help ~init arglist : t * string list = |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} + |"-boot" -> { oval with pre = { oval.pre with boot = true }} |"-output-context" -> { oval with post = { oval.post with output_context = true }} |"-profile-ltac" -> Flags.profile_ltac := true; oval |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} @@ -569,5 +572,5 @@ let cmdline_load_path opts = opts.pre.ml_includes @ opts.pre.vo_includes let build_load_path opts = - Coqinit.libs_init_load_path ~load_init:opts.pre.load_init @ + (if opts.pre.boot then [] else Coqinit.libs_init_load_path ()) @ cmdline_load_path opts diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 26f22386a0..f38381a086 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -40,6 +40,7 @@ type coqargs_config = { } type coqargs_pre = { + boot : bool; load_init : bool; load_rcfile : bool; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 3aa9acfc52..7f3d4b570f 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -52,10 +52,10 @@ let load_rcfile ~rcfile ~state = iraise reraise (* Recursively puts `.v` files in the LoadPath if -nois was not passed *) -let build_stdlib_vo_path ~load_init ~unix_path ~coq_path = +let build_stdlib_vo_path ~unix_path ~coq_path = let open Loadpath in { recursive = true; - path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = load_init } + path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = true } } let build_stdlib_ml_path ~dir = @@ -88,7 +88,7 @@ let toplevel_init_load_path () = ml_path_if Coq_config.local [coqlib/"dev"] (* LoadPath for Coq user libraries *) -let libs_init_load_path ~load_init = +let libs_init_load_path () = let open Loadpath in let coqlib = Envars.coqlib () in @@ -107,7 +107,7 @@ let libs_init_load_path ~load_init = (* then standard library *) [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @ - [build_stdlib_vo_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path] @ + [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @ (* then user-contrib *) (if Sys.file_exists user_contrib then diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index fc53c8b47c..f3a007d987 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -20,4 +20,4 @@ val init_ocaml_path : unit -> unit val toplevel_init_load_path : unit -> Loadpath.coq_path list (* LoadPath for Coq user libraries *) -val libs_init_load_path : load_init:bool -> Loadpath.coq_path list +val libs_init_load_path : unit -> Loadpath.coq_path list diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 6848862603..ba3deeb2f6 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -32,7 +32,8 @@ let print_usage_common co command = \n -coqlib dir set the coq standard library directory\ \n -exclude-dir f exclude subdirectories named f for option -R\ \n\ -\n -noinit start without loading the Init library\ +\n -boot don't bind the `Coq.` prefix to the default -coqlib dir\ +\n -noinit don't load Coq.Init.Prelude on start \ \n -nois (idem)\ \n -compat X.Y provides compatibility support for Coq version X.Y\ \n\ |