From e8419bac30ab98527ec6b15d5a0f5c1035539ca5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 12 Feb 2019 02:41:00 +0100 Subject: [library] Remove `-boot` option. The `-boot` option was used to: - suppress loading of the rc_file - allow to save modules with prefix `Coq` There is no good reason disable saving of modules with `Coq` prefix by default, thus we remove this option. Fixes: #9575 --- Makefile.build | 2 +- checker/checker.ml | 4 ---- man/coqide.1 | 9 --------- man/coqtop.1 | 6 ------ stm/stm.ml | 18 +----------------- stm/stm.mli | 4 ---- test-suite/bugs/closed/bug_5198.v | 2 +- tools/coq_dune.ml | 2 +- tools/coq_tex.ml | 3 --- toplevel/ccompile.ml | 2 -- toplevel/coqargs.ml | 12 +++++++----- toplevel/coqargs.mli | 2 -- toplevel/coqtop.ml | 1 - toplevel/usage.ml | 1 - 14 files changed, 11 insertions(+), 57 deletions(-) diff --git a/Makefile.build b/Makefile.build index 2b401cd9e6..ea356d5f8e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -201,7 +201,7 @@ COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS) # Beware this depends on the makefile being in a particular dir, we # should pass an absolute path here but windows is tricky # c.f. https://github.com/coq/coq/pull/9560 -BOOTCOQC=$(TIMER) $(COQC) -coqlib . -boot $(COQOPTS) +BOOTCOQC=$(TIMER) $(COQC) -coqlib . -q $(COQOPTS) LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) MLINCLUDES=$(LOCALINCLUDES) diff --git a/checker/checker.ml b/checker/checker.ml index 4dac02210b..3c93ef7d36 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -192,7 +192,6 @@ let print_usage_channel co command = \n -coqlib dir set coqchk's standard library location\ \n -where print coqchk's standard library location and exit\ \n -v print coqchk version and exit\ -\n -boot boot mode\ \n -o, --output-context print the list of assumptions\ \n -m, --memory print the maximum heap size\ \n -silent disable trace of constants being checked\ @@ -320,8 +319,6 @@ 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 | [] -> () @@ -358,7 +355,6 @@ let parse_args argv = | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-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 diff --git a/man/coqide.1 b/man/coqide.1 index 3592f6e4e3..62a102af03 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -100,15 +100,6 @@ Skip loading of rcfile. Set the rcfile to .IR f . .TP -.B \-batch -Batch mode (exits just after arguments parsing). -.TP -.B \-boot -Boot mode (implies -.B \-q -and -.BR \-batch ). -.TP .B \-emacs Tells Coq it is executed under Emacs. .TP diff --git a/man/coqtop.1 b/man/coqtop.1 index addfb54672..25d0ef7718 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -105,12 +105,6 @@ set the rcfile to .B \-batch batch mode (exits just after arguments parsing) -.TP -.B \-boot -boot mode (implies -.B \-q -) - .TP .B \-emacs tells Coq it is executed under Emacs diff --git a/stm/stm.ml b/stm/stm.ml index b4f26570c6..8af1a2ebd2 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2647,10 +2647,6 @@ 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; @@ -2678,16 +2674,6 @@ let init_core () = if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; State.register_root_state () -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 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.") - let dirpath_of_file f = let ldir0 = try @@ -2700,7 +2686,7 @@ let dirpath_of_file f = let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir -let new_doc { doc_type ; allow_coq_overwrite; iload_path; require_libs; stm_options } = +let new_doc { doc_type ; iload_path; require_libs; stm_options } = let load_objs libs = let rq_file (dir, from, exp) = @@ -2735,14 +2721,12 @@ let new_doc { doc_type ; allow_coq_overwrite; iload_path; require_libs; stm_opti | VoDoc f -> let ldir = dirpath_of_file f in - 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 ~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 102e832d3e..91651e3534 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -67,10 +67,6 @@ 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/test-suite/bugs/closed/bug_5198.v b/test-suite/bugs/closed/bug_5198.v index 5d4409f89b..4f24189d3f 100644 --- a/test-suite/bugs/closed/bug_5198.v +++ b/test-suite/bugs/closed/bug_5198.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-boot" "-nois") -*- *) +(* -*- mode: coq; coq-prog-args: ("-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 286 lines to 27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 68371edcb1..62a871aa0e 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -186,7 +186,7 @@ let pp_vo_dep dir fmt vo = (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) let libflag = "-coqlib %{project_root}" in (* The final build rule *) - let action = sprintf "(chdir %%{project_root} (run coqc -boot %s %s %s %s))" libflag eflag cflag source in + let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in let all_targets = gen_coqc_targets vo in pp_rule fmt all_targets deps action diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 0ffa5bd7e4..c6d3551561 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -259,8 +259,6 @@ let parse_cl () = " Coq parts are written between 2 horizontal lines"; "-small", Arg.Set small, " Coq parts are written in small font"; - "-boot", Arg.Set boot, - " Launch coqtop with the -boot option" ] (fun s -> files := s :: !files) "coq-tex [options] file ..." @@ -279,7 +277,6 @@ let find_coqtop () = let _ = parse_cl (); if !image = "" then image := Filename.quote (find_coqtop ()); - if !boot then image := !image ^ " -boot"; if Sys.command (!image ^ " -batch -silent") <> 0 then begin Printf.printf "Error: "; let _ = Sys.command (!image ^ " -batch") in diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 8064ee8880..3fe6ad0718 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -112,7 +112,6 @@ 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 @@ -163,7 +162,6 @@ 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 0c9201c3a5..abfda07426 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -40,8 +40,6 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool } type t = { - boot : bool; - load_init : bool; load_rcfile : bool; rcfile : string option; @@ -93,8 +91,6 @@ let default_native = let default = { - boot = false; - load_init = true; load_rcfile = true; rcfile = None; @@ -179,6 +175,10 @@ let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") +let warn_deprecated_boot = + CWarnings.create ~name:"deprecated-boot" ~category:"noop" + (fun () -> Pp.strbrk "The -boot option is deprecated, please use -q and/or -coqlib options instead.") + let set_inputstate opts s = warn_deprecated_inputstate (); { opts with inputstate = Some s } @@ -459,7 +459,9 @@ 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" -> { oval with boot = true; load_rcfile = false; } + |"-boot" -> + warn_deprecated_boot (); + { oval with load_rcfile = false; } |"-bt" -> Backtrace.record_backtrace true; oval |"-color" -> set_color oval (next ()) |"-config"|"--config" -> { oval with print_config = true } diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index 9cc846edea..b89a88d1f6 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -16,8 +16,6 @@ type native_compiler = NativeOff | NativeOn of { ondemand : bool } type t = { - boot : bool; - load_init : bool; load_rcfile : bool; rcfile : string option; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 9115fbb726..92ac200bc0 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -221,7 +221,6 @@ 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 0d17218a56..94ec6bb70d 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -62,7 +62,6 @@ 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, 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\ -- cgit v1.2.3