aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checker.ml8
-rw-r--r--lib/envars.ml4
-rw-r--r--lib/envars.mli2
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli2
-rw-r--r--stm/stm.ml15
-rw-r--r--stm/stm.mli4
-rw-r--r--tools/coq_makefile.ml2
-rw-r--r--tools/coqdep.ml3
-rw-r--r--toplevel/ccompile.ml2
-rw-r--r--toplevel/coqargs.ml12
-rw-r--r--toplevel/coqargs.mli2
-rw-r--r--toplevel/coqtop.ml3
-rw-r--r--toplevel/usage.ml2
14 files changed, 40 insertions, 23 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index d97ab5409e..af8d1e5617 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -319,6 +319,8 @@ let explain_exn = function
let deprecated flag =
Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag))
+let boot_opt = ref false
+
let parse_args argv =
let rec parse = function
| [] -> ()
@@ -348,14 +350,14 @@ let parse_args argv =
| "-debug" :: rem -> set_debug (); parse rem
| "-where" :: _ ->
- Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
+ Envars.set_coqlib ~boot:!boot_opt ~fail:(fun x -> CErrors.user_err Pp.(str x));
print_endline (Envars.coqlib ());
exit 0
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
| ("-v"|"--version") :: _ -> version ()
- | "-boot" :: rem -> Flags.boot := true; parse rem
+ | "-boot" :: rem -> boot_opt := true; parse rem
| ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
| ("-o" | "--output-context") :: rem ->
Check_stat.output_context := true; parse rem
@@ -384,7 +386,7 @@ let init_with_argv argv =
try
parse_args argv;
if !Flags.debug then Printexc.record_backtrace true;
- Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
+ Envars.set_coqlib ~boot:!boot_opt ~fail:(fun x -> CErrors.user_err Pp.(str x));
Flags.if_verbose print_header ();
init_load_path ();
make_senv ()
diff --git a/lib/envars.ml b/lib/envars.ml
index b5036e7340..8a75d9a552 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -110,11 +110,11 @@ let set_user_coqlib path = coqlib := Some path
(** coqlib is now computed once during coqtop initialization *)
-let set_coqlib ~fail =
+let set_coqlib ~boot ~fail =
match !coqlib with
| Some _ -> ()
| None ->
- let lib = if !Flags.boot then coqroot else guess_coqlib fail in
+ let lib = if boot then coqroot else guess_coqlib fail in
coqlib := Some lib
let coqlib () = Option.default "" !coqlib
diff --git a/lib/envars.mli b/lib/envars.mli
index ebf86d0650..21365c48f6 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -39,7 +39,7 @@ val datadir : unit -> string
val configdir : unit -> string
(** [set_coqlib] must be runned once before any access to [coqlib] *)
-val set_coqlib : fail:(string -> string) -> unit
+val set_coqlib : boot:bool -> fail:(string -> string) -> unit
(** [set_user_coqlib path] sets the coqlib directory explicitedly. *)
val set_user_coqlib : string -> unit
diff --git a/lib/flags.ml b/lib/flags.ml
index 55bfa3cbde..20cf991a25 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -41,8 +41,6 @@ let with_options ol f x =
let () = List.iter2 (:=) ol vl in
Exninfo.iraise reraise
-let boot = ref false
-
let record_aux_file = ref false
let test_mode = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 7336b9beaf..607f0e2e49 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -31,8 +31,6 @@
(** Command-line flags *)
-val boot : bool ref
-
(** Set by coqtop to tell the kernel to output to the aux file; will
be eventually removed by cleanups such as PR#1103 *)
val record_aux_file : bool ref
diff --git a/stm/stm.ml b/stm/stm.ml
index 0165b3c029..8db1bd4508 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2647,6 +2647,10 @@ type stm_init_options = {
some point. *)
doc_type : stm_doc_type;
+ (* Allow compiling modules in the Coq prefix. Irrelevant in
+ interactive mode. *)
+ allow_coq_overwrite : bool;
+
(* Initial load path in scope for the document. Usually extracted
from -R options / _CoqProject *)
iload_path : Mltop.coq_path list;
@@ -2674,11 +2678,12 @@ let init_core () =
if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true;
State.register_root_state ()
-let check_coq_overwriting p =
+let check_coq_overwriting ~allow_coq_overwrite p =
+ if not allow_coq_overwrite then
let l = DirPath.repr p in
let id, l = match l with id::l -> id,l | [] -> assert false in
let is_empty = match l with [] -> true | _ -> false in
- if not !Flags.boot && not is_empty && Id.equal (CList.last l) Libnames.coq_root then
+ if not is_empty && Id.equal (CList.last l) Libnames.coq_root then
user_err
(str "Cannot build module " ++ DirPath.print p ++ str "." ++ spc () ++
str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
@@ -2695,7 +2700,7 @@ let dirpath_of_file f =
let ldir = Libnames.add_dirpath_suffix ldir0 id in
ldir
-let new_doc { doc_type ; iload_path; require_libs; stm_options } =
+let new_doc { doc_type ; allow_coq_overwrite; iload_path; require_libs; stm_options } =
let load_objs libs =
let rq_file (dir, from, exp) =
@@ -2730,14 +2735,14 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
| VoDoc f ->
let ldir = dirpath_of_file f in
- check_coq_overwriting ldir;
+ check_coq_overwriting ~allow_coq_overwrite ldir;
let () = Flags.verbosely Declaremods.start_library ldir in
VCS.set_ldir ldir;
set_compilation_hints f
| VioDoc f ->
let ldir = dirpath_of_file f in
- check_coq_overwriting ldir;
+ check_coq_overwriting ~allow_coq_overwrite ldir;
let () = Flags.verbosely Declaremods.start_library ldir in
VCS.set_ldir ldir;
set_compilation_hints f
diff --git a/stm/stm.mli b/stm/stm.mli
index 821ab59a43..313ac58111 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -67,6 +67,10 @@ type stm_init_options = {
some point. *)
doc_type : stm_doc_type;
+ (* Allow compiling modules in the Coq prefix. Irrelevant in
+ interactive mode. *)
+ allow_coq_overwrite : bool;
+
(* Initial load path in scope for the document. Usually extracted
from -R options / _CoqProject *)
iload_path : Mltop.coq_path list;
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 5fd894e908..5526970d3f 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -431,7 +431,7 @@ let _ =
check_overlapping_include project;
- Envars.set_coqlib ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1);
+ Envars.set_coqlib ~boot:false ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1);
let ocm = Option.cata open_out stdout project.makefile in
generate_makefile ocm conf_file local_file (prog :: args) project;
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 4e80caa4cc..5f8cc99ed1 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -530,7 +530,8 @@ let coqdep () =
add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"];
add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"];
end else begin
- Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg));
+ (* option_boot is actually always false in this branch *)
+ Envars.set_coqlib ~boot:!option_boot ~fail:(fun msg -> raise (CoqlibError msg));
let coqlib = Envars.coqlib () in
add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"];
add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"];
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index df2b983029..ecb0407f75 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -109,6 +109,7 @@ let compile opts copts ~echo ~f_in ~f_out =
let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
Stm.new_doc
Stm.{ doc_type = VoDoc long_f_dot_vo;
+ allow_coq_overwrite = opts.boot;
iload_path; require_libs; stm_options;
} in
let state = { doc; sid; proof = None; time = opts.time } in
@@ -159,6 +160,7 @@ let compile opts copts ~echo ~f_in ~f_out =
let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
Stm.new_doc
Stm.{ doc_type = VioDoc long_f_dot_vio;
+ allow_coq_overwrite = opts.boot;
iload_path; require_libs; stm_options;
} in
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 74c016101a..ae3c5b32dc 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -35,6 +35,8 @@ type color = [`ON | `AUTO | `OFF]
type t = {
+ boot : bool;
+
load_init : bool;
load_rcfile : bool;
rcfile : string option;
@@ -81,6 +83,8 @@ let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
let default = {
+ boot = false;
+
load_init = true;
load_rcfile = true;
rcfile = None;
@@ -232,9 +236,9 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy
exception NoCoqLib
-let usage help =
+let usage ~boot help =
begin
- try Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib)
+ try Envars.set_coqlib ~boot ~fail:(fun x -> raise NoCoqLib)
with NoCoqLib -> usage_no_coqlib ()
end;
let lp = Coqinit.toplevel_init_load_path () in
@@ -436,7 +440,7 @@ let parse_args ~help ~init arglist : t * string list =
{ oval with batch = true }
|"-test-mode" -> Flags.test_mode := true; oval
|"-beautify" -> Flags.beautify := true; oval
- |"-boot" -> Flags.boot := true; { oval with load_rcfile = false; }
+ |"-boot" -> { oval with boot = true; load_rcfile = false; }
|"-bt" -> Backtrace.record_backtrace true; oval
|"-color" -> set_color oval (next ())
|"-config"|"--config" -> { oval with print_config = true }
@@ -468,7 +472,7 @@ let parse_args ~help ~init arglist : t * string list =
|"-type-in-type" -> set_type_in_type (); oval
|"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
|"-where" -> { oval with print_where = true }
- |"-h"|"-H"|"-?"|"-help"|"--help" -> usage help; oval
+ |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ~boot:oval.boot help; oval
|"-v"|"--version" -> Usage.version (exitcode oval)
|"-print-version"|"--print-version" ->
Usage.machine_readable_version (exitcode oval)
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index c9a7a0fd56..52ab2b60d7 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -14,6 +14,8 @@ val default_toplevel : Names.DirPath.t
type t = {
+ boot : bool;
+
load_init : bool;
load_rcfile : bool;
rcfile : string option;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6ef0aa390d..faf26a9665 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -162,7 +162,7 @@ let init_toplevel ~help ~init custom_init arglist =
(* If we have been spawned by the Spawn module, this has to be done
* early since the master waits us to connect back *)
Spawned.init_channels ();
- Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
+ Envars.set_coqlib ~boot:opts.boot ~fail:(fun msg -> CErrors.user_err Pp.(str msg));
if opts.print_where then begin
print_endline (Envars.coqlib ());
exit (exitcode opts)
@@ -221,6 +221,7 @@ let init_toploop opts =
let doc, sid =
Stm.(new_doc
{ doc_type = Interactive opts.toplevel_name;
+ allow_coq_overwrite = true; (* irrelevant *)
iload_path; require_libs; stm_options;
}) in
let state = { doc; sid; proof = None; time = opts.time } in
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 277f8b7367..0d17218a56 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -62,7 +62,7 @@ let print_usage_common co command =
\n\
\n -q skip loading of rcfile\
\n -init-file f set the rcfile to f\
-\n -boot boot mode (allows to overload the `Coq` library prefix)\
+\n -boot boot mode (allows to overload the `Coq` library prefix, implies -q)\
\n -bt print backtraces (requires configure debug flag)\
\n -debug debug mode (implies -bt)\
\n -diffs (on|off|removed) highlight differences between proof steps\
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:39:22 +0000