aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/ccompile.ml7
-rw-r--r--toplevel/coqargs.ml69
-rw-r--r--toplevel/coqargs.mli5
-rw-r--r--toplevel/coqinit.ml2
-rw-r--r--toplevel/coqloop.ml6
-rw-r--r--toplevel/coqtop.ml2
-rw-r--r--toplevel/g_toplevel.mlg2
-rw-r--r--toplevel/usage.ml1
-rw-r--r--toplevel/vernac.ml20
9 files changed, 74 insertions, 40 deletions
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index df2b983029..3fe6ad0718 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -96,6 +96,9 @@ let compile opts copts ~echo ~f_in ~f_out =
let iload_path = build_load_path opts in
let require_libs = require_libs opts in
let stm_options = opts.stm_flags in
+ let output_native_objects = match opts.native_compiler with
+ | NativeOff -> false | NativeOn {ondemand} -> not ondemand
+ in
match copts.compilation_mode with
| BuildVo ->
Flags.record_aux_file := true;
@@ -125,7 +128,7 @@ let compile opts copts ~echo ~f_in ~f_out =
let _doc = Stm.join ~doc:state.doc in
let wall_clock2 = Unix.gettimeofday () in
check_pending_proofs ();
- Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
+ Library.save_library_to ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ());
Aux_file.record_in_aux_at "vo_compile_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
Aux_file.stop_aux_file ();
@@ -168,7 +171,7 @@ let compile opts copts ~echo ~f_in ~f_out =
let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in
let doc = Stm.finish ~doc:state.doc in
check_pending_proofs ();
- let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
+ let () = ignore (Stm.snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vio) in
Stm.reset_task_queue ()
| Vio2Vo ->
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 74c016101a..abfda07426 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -13,6 +13,9 @@ let fatal_error exn =
let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
exit exit_code
+let error_wrong_arg msg =
+ prerr_endline msg; exit 1
+
let error_missing_arg s =
prerr_endline ("Error: extra argument expected after option "^s);
prerr_endline "See -help for the syntax of supported options";
@@ -33,6 +36,8 @@ let set_type_in_type () =
type color = [`ON | `AUTO | `OFF]
+type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+
type t = {
load_init : bool;
@@ -54,7 +59,7 @@ type t = {
impredicative_set : Declarations.set_predicativity;
indices_matter : bool;
enable_VM : bool;
- enable_native_compiler : bool;
+ native_compiler : native_compiler;
stm_flags : Stm.AsyncOpts.stm_opt;
debug : bool;
@@ -79,6 +84,11 @@ type t = {
let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
+let default_native =
+ if Coq_config.native_compiler
+ then NativeOn {ondemand=true}
+ else NativeOff
+
let default = {
load_init = true;
@@ -99,7 +109,8 @@ let default = {
impredicative_set = Declarations.PredicativeSet;
indices_matter = false;
enable_VM = true;
- enable_native_compiler = Coq_config.native_compiler;
+ native_compiler = default_native;
+
stm_flags = Stm.AsyncOpts.default_opts;
debug = false;
diffs_set = false;
@@ -157,12 +168,17 @@ let set_color opts = function
| "yes" | "on" -> { opts with color = `ON }
| "no" | "off" -> { opts with color = `OFF }
| "auto" -> { opts with color = `AUTO }
-| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1
+| _ ->
+ error_wrong_arg ("Error: on/off/auto expected after option color")
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 }
@@ -175,26 +191,26 @@ let exitcode opts = if opts.filter_opts then 2 else 0
let get_bool opt = function
| "yes" | "on" -> true
| "no" | "off" -> false
- | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1
+ | _ ->
+ error_wrong_arg ("Error: yes/no expected after option "^opt)
let get_int opt n =
try int_of_string n
with Failure _ ->
- prerr_endline ("Error: integer expected after option "^opt); exit 1
+ error_wrong_arg ("Error: integer expected after option "^opt)
let get_float opt n =
try float_of_string n
with Failure _ ->
- prerr_endline ("Error: float expected after option "^opt); exit 1
+ error_wrong_arg ("Error: float expected after option "^opt)
let get_host_port opt s =
match String.split_on_char ':' s with
| [host; portr; portw] ->
- Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
+ Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
| ["stdfds"] -> Some Spawned.AnonPipe
| _ ->
- prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt);
- exit 1
+ error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt)
let get_error_resilience opt = function
| "on" | "all" | "yes" -> `All
@@ -204,17 +220,20 @@ let get_error_resilience opt = function
let get_priority opt s =
try CoqworkmgrApi.priority_of_string s
with Invalid_argument _ ->
- prerr_endline ("Error: low/high expected after "^opt); exit 1
+ error_wrong_arg ("Error: low/high expected after "^opt)
let get_async_proofs_mode opt = let open Stm.AsyncOpts in function
| "no" | "off" -> APoff
| "yes" | "on" -> APon
| "lazy" -> APonLazy
- | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1
+ | _ ->
+ error_wrong_arg ("Error: on/off/lazy expected after "^opt)
let get_cache opt = function
| "force" -> Some Stm.AsyncOpts.Force
- | _ -> prerr_endline ("Error: force expected after "^opt); exit 1
+ | _ ->
+ error_wrong_arg ("Error: force expected after "^opt)
+
let get_native_name s =
(* We ignore even critical errors because this mode has to be super silent *)
@@ -299,8 +318,12 @@ let parse_args ~help ~init arglist : t * string list =
}}
|"-async-proofs-tac-j" ->
+ let j = get_int opt (next ()) in
+ if j <= 0 then begin
+ error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1")
+ end;
{ oval with stm_flags = { oval.stm_flags with
- Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ()))
+ Stm.AsyncOpts.async_proofs_n_tacworkers = j
}}
|"-async-proofs-worker-priority" ->
@@ -414,15 +437,15 @@ let parse_args ~help ~init arglist : t * string list =
produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by
a separate flag, and the "ondemand" value removed. Once this is done, use
[get_bool] here. *)
- let (enable,precompile) =
+ let native_compiler =
match (next ()) with
- | ("yes" | "on") -> true, true
- | "ondemand" -> true, false
- | ("no" | "off") -> false, false
- | _ -> prerr_endline ("Error: (yes|no|ondemand) expected after option -native-compiler"); exit 1
+ | ("yes" | "on") -> NativeOn {ondemand=false}
+ | "ondemand" -> NativeOn {ondemand=true}
+ | ("no" | "off") -> NativeOff
+ | _ ->
+ error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler")
in
- Flags.output_native_objects := precompile;
- { oval with enable_native_compiler = enable }
+ { oval with native_compiler }
(* Options with zero arg *)
|"-async-queries-always-delegate"
@@ -436,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" -> Flags.boot := true; { oval with 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 }
@@ -445,7 +470,7 @@ let parse_args ~help ~init arglist : t * string list =
if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then
Proof_diffs.write_diffs_option opt
else
- (prerr_endline ("Error: on|off|removed expected after -diffs"); exit 1);
+ error_wrong_arg "Error: on|off|removed expected after -diffs";
{ oval with diffs_set = true }
|"-stm-debug" -> Stm.stm_debug := true; oval
|"-emacs" -> set_emacs oval
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index c9a7a0fd56..b89a88d1f6 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -12,6 +12,8 @@ type color = [`ON | `AUTO | `OFF]
val default_toplevel : Names.DirPath.t
+type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+
type t = {
load_init : bool;
@@ -32,7 +34,8 @@ type t = {
impredicative_set : Declarations.set_predicativity;
indices_matter : bool;
enable_VM : bool;
- enable_native_compiler : bool;
+ native_compiler : native_compiler;
+
stm_flags : Stm.AsyncOpts.stm_opt;
debug : bool;
diffs_set : bool;
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index e1d35e537b..74a089510e 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -11,7 +11,7 @@
open Util
open Pp
-let ( / ) s1 s2 = s1 ^ "/" ^ s2
+let ( / ) s1 s2 = Filename.concat s1 s2
let set_debug () =
let () = Backtrace.record_backtrace true in
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index e933f08735..1094fc86b4 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -366,6 +366,11 @@ let top_goal_print ~doc c oldp newp =
let msg = CErrors.iprint (e, info) in
TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer
+let exit_on_error =
+ let open Goptions in
+ declare_bool_option_and_ref ~depr:false ~name:"coqtop-exit-on-error" ~key:["Coqtop";"Exit";"On";"Error"]
+ ~value:false
+
let rec vernac_loop ~state =
let open CAst in
let open Vernac.State in
@@ -410,6 +415,7 @@ let rec vernac_loop ~state =
let loc = Loc.get_loc info in
let msg = CErrors.iprint (e, info) in
TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
+ if exit_on_error () then exit 1;
vernac_loop ~state
let rec loop ~state =
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6ef0aa390d..92ac200bc0 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -188,7 +188,7 @@ let init_toplevel ~help ~init custom_init arglist =
Global.set_engagement opts.impredicative_set;
Global.set_indices_matter opts.indices_matter;
Global.set_VM opts.enable_VM;
- Global.set_native_compiler opts.enable_native_compiler;
+ Global.set_native_compiler (match opts.native_compiler with NativeOff -> false | NativeOn _ -> true);
(* Allow the user to load an arbitrary state here *)
inputstate opts;
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 7f1cca277e..f2025858d7 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -41,7 +41,7 @@ GRAMMAR EXTEND Gram
| cmd = Pvernac.Vernac_.main_entry ->
{ match cmd with
| None -> None
- | Some (loc,c) -> Some (CAst.make ~loc (VernacControl c)) }
+ | Some {CAst.loc; v} -> Some (CAst.make ?loc (VernacControl v)) }
]
]
;
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 277f8b7367..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)\
\n -bt print backtraces (requires configure debug flag)\
\n -debug debug mode (implies -bt)\
\n -diffs (on|off|removed) highlight differences between proof steps\
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 45ca658857..ef1dc6993b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -101,20 +101,18 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
~doc:state.doc ~entry:Pvernac.main_entry state.sid in_pa
with
| None ->
- input_cleanup ();
- state, ids, Pcoq.Parsable.comment_state in_pa
- | Some (loc, ast) ->
- let ast = CAst.make ~loc ast in
+ input_cleanup ();
+ state, ids, Pcoq.Parsable.comment_state in_pa
+ | Some ast ->
+ (* Printing of AST for -compile-verbose *)
+ Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo;
- (* Printing of AST for -compile-verbose *)
- Option.iter (vernac_echo ~loc) in_echo;
+ checknav_simple ast;
- checknav_simple ast;
+ let state =
+ Flags.silently (interp_vernac ~check ~interactive ~state) ast in
- let state =
- Flags.silently (interp_vernac ~check ~interactive ~state) ast in
-
- loop state (state.sid :: ids)
+ loop state (state.sid :: ids)
in
try loop state []
with any -> (* whatever the exception *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 00:45:52 +0000