aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqargs.ml12
-rw-r--r--toplevel/coqargs.mli1
-rw-r--r--toplevel/coqloop.ml32
-rw-r--r--toplevel/coqtop.ml41
-rw-r--r--toplevel/dune13
-rw-r--r--toplevel/usage.ml3
6 files changed, 66 insertions, 36 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 89602c9b56..98a28bb2b6 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -68,6 +68,7 @@ type coq_cmdopts = {
impredicative_set : Declarations.set_predicativity;
stm_flags : Stm.AsyncOpts.stm_opt;
debug : bool;
+ diffs_set : bool;
time : bool;
filter_opts : bool;
@@ -117,6 +118,7 @@ let init_args = {
impredicative_set = Declarations.PredicativeSet;
stm_flags = Stm.AsyncOpts.default_opts;
debug = false;
+ diffs_set = false;
time = false;
filter_opts = false;
@@ -152,7 +154,7 @@ let add_compat_require opts v =
match v with
| Flags.V8_6 -> add_vo_require opts "Coq.Compat.Coq86" None (Some false)
| Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false)
- | Flags.Current -> opts
+ | Flags.Current -> add_vo_require opts "Coq.Compat.Coq88" None (Some false)
let set_batch_mode opts =
Flags.quiet := true;
@@ -423,7 +425,7 @@ let parse_args arglist : coq_cmdopts * string list =
|"-worker-id" -> set_worker_id opt (next ()); oval
|"-compat" ->
- let v = G_vernac.parse_compat_version ~allow_old:false (next ()) in
+ let v = G_vernac.parse_compat_version (next ()) in
Flags.compat_version := v;
add_compat_require oval v
@@ -526,6 +528,12 @@ let parse_args arglist : coq_cmdopts * string list =
|"-color" -> set_color oval (next ())
|"-config"|"--config" -> { oval with print_config = true }
|"-debug" -> Coqinit.set_debug (); oval
+ |"-diffs" -> let opt = next () in
+ 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);
+ { oval with diffs_set = true }
|"-stm-debug" -> Stm.stm_debug := true; oval
|"-emacs" -> set_emacs oval
|"-filteropts" -> { oval with filter_opts = true }
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 9fb6219a61..7b0cdcf127 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -43,6 +43,7 @@ type coq_cmdopts = {
impredicative_set : Declarations.set_predicativity;
stm_flags : Stm.AsyncOpts.stm_opt;
debug : bool;
+ diffs_set : bool;
time : bool;
filter_opts : bool;
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 7ae15ac100..59a464a22e 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -318,12 +318,6 @@ let loop_flush_all () =
Format.pp_print_flush !Topfmt.std_ft ();
Format.pp_print_flush !Topfmt.err_ft ()
-let pr_open_cur_subgoals () =
- try
- let proof = Proof_global.give_me_the_proof () in
- Printer.pr_open_subgoals ~proof
- with Proof_global.NoCurrentProof -> Pp.str ""
-
(* Goal equality heuristic. *)
let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2
let evleq e1 e2 = CList.equal Evar.equal e1 e2
@@ -336,17 +330,33 @@ let cproof p1 p2 =
let drop_last_doc = ref None
+(* todo: could add other Set/Unset commands, such as "Printing Universes" *)
+let print_anyway_opts = [
+ [ "Diffs" ];
+ ]
+
+let print_anyway c =
+ let open Vernacexpr in
+ match c with
+ | VernacExpr (_, VernacSetOption (_, opt, _))
+ | VernacExpr (_, VernacUnsetOption (_, opt)) ->
+ List.mem opt print_anyway_opts
+ | _ -> false
+
(* We try to behave better when goal printing raises an exception
[usually Ctrl-C]
This is mostly a hack as we should protect printing in a more
generic way, but that'll do for now *)
-let top_goal_print oldp newp =
+let top_goal_print ~doc c oldp newp =
try
let proof_changed = not (Option.equal cproof oldp newp) in
- let print_goals = not !Flags.quiet &&
- proof_changed && Proof_global.there_are_pending_proofs () in
- if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ())
+ let print_goals = proof_changed && Proof_global.there_are_pending_proofs () ||
+ print_anyway c in
+ if not !Flags.quiet && print_goals then begin
+ let dproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
+ Printer.print_and_diff dproof newp
+ end
with
| exn ->
let (e, info) = CErrors.push exn in
@@ -382,7 +392,7 @@ let rec vernac_loop ~state =
else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state)
| {v=VernacControl c; loc} ->
let nstate = Vernac.process_expr ~state (make ?loc c) in
- top_goal_print state.proof nstate.proof;
+ top_goal_print ~doc:state.doc c state.proof nstate.proof;
vernac_loop ~state:nstate
with
| Stm.End_of_input ->
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e979d0e544..8cd262c6d6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -339,8 +339,8 @@ let do_vio opts =
(******************************************************************************)
(* Color Options *)
(******************************************************************************)
-let init_color color_mode =
- let has_color = match color_mode with
+let init_color opts =
+ let has_color = match opts.color with
| `OFF -> false
| `ON -> true
| `AUTO ->
@@ -350,26 +350,23 @@ let init_color color_mode =
its TERM variable is set to "dumb". *)
try Sys.getenv "TERM" <> "dumb" with Not_found -> false
in
- if has_color then begin
- let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
- match colors with
- | None ->
- (** Default colors *)
- Topfmt.default_styles ();
- Topfmt.init_terminal_output ~color:true
- | Some "" ->
- (** No color output *)
- Topfmt.init_terminal_output ~color:false
- | Some s ->
- (** Overwrite all colors *)
- Topfmt.parse_color_config s;
- Topfmt.init_terminal_output ~color:true
- end
- else
- Topfmt.init_terminal_output ~color:false
+ let term_color =
+ if has_color then begin
+ let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
+ match colors with
+ | None -> Topfmt.default_styles (); true (** Default colors *)
+ | Some "" -> false (** No color output *)
+ | Some s -> Topfmt.parse_color_config s; true (** Overwrite all colors *)
+ end
+ else
+ false
+ in
+ if Proof_diffs.show_diffs () && not term_color && not opts.batch_mode then
+ (prerr_endline "Error: -diffs requires enabling -color"; exit 1);
+ Topfmt.init_terminal_output ~color:term_color
let print_style_tags opts =
- let () = init_color opts.color in
+ let () = init_color opts in
let tags = Topfmt.dump_tags () in
let iter (t, st) =
let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in
@@ -387,7 +384,7 @@ let print_style_tags opts =
(** GC tweaking *)
(** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
- minor heap is heavily sollicited. Unfortunately, the default size is far too
+ minor heap is heavily solicited. Unfortunately, the default size is far too
small, so we enlarge it a lot (128 times larger).
To better handle huge memory consumers, we also augment the default major
@@ -520,7 +517,7 @@ type custom_toplevel = {
}
let coqtop_init ~opts extra =
- init_color opts.color;
+ init_color opts;
CoqworkmgrApi.(init !async_proofs_worker_priority);
opts, extra
diff --git a/toplevel/dune b/toplevel/dune
new file mode 100644
index 0000000000..f51e50aaa3
--- /dev/null
+++ b/toplevel/dune
@@ -0,0 +1,13 @@
+(library
+ (name toplevel)
+ (public_name coq.toplevel)
+ (synopsis "Coq's Interactive Shell [terminal-based]")
+ (wrapped false)
+ (libraries num coq.stm))
+; Coqlevel provides the `Num` library to plugins, we could also use
+; -linkall in the plugins file, to be discussed.
+
+(rule
+ (targets g_toplevel.ml)
+ (deps (:mlg-file g_toplevel.mlg))
+ (action (run coqpp %{mlg-file})))
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 504ffa521b..d85fed5f43 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -72,7 +72,8 @@ let print_usage_channel co command =
\n -boot boot mode (implies -q and -batch)\
\n -bt print backtraces (requires configure debug flag)\
\n -debug debug mode (implies -bt)\
-\n -stm-debug STM debug mode (will trace every transaction) \
+\n -diffs (on|off|removed) highlight differences between proof steps\
+\n -stm-debug STM debug mode (will trace every transaction)\
\n -emacs tells Coq it is executed under Emacs\
\n -noglob do not dump globalizations\
\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 00:51:47 +0000