aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/dumpglob.ml32
-rw-r--r--interp/dumpglob.mli14
-rw-r--r--lib/aux_file.mli2
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli4
-rw-r--r--stm/vio_checking.ml3
-rw-r--r--tactics/declare.ml2
-rw-r--r--toplevel/ccompile.ml11
-rw-r--r--toplevel/coqargs.ml10
-rw-r--r--toplevel/coqargs.mli1
-rw-r--r--toplevel/coqc.ml3
-rw-r--r--toplevel/coqcargs.ml13
-rw-r--r--toplevel/coqcargs.mli1
-rw-r--r--toplevel/coqloop.ml6
-rw-r--r--vernac/proof_using.ml2
15 files changed, 39 insertions, 67 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 8d6a266c30..41d1da9694 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -20,31 +20,21 @@ let open_glob_file f =
let close_glob_file () =
close_out !glob_file
-type glob_output_t =
- | NoGlob
- | StdOut
- | MultFiles
- | Feedback
- | File of string
+type glob_output =
+ | NoGlob
+ | Feedback
+ | MultFiles
+ | File of string
let glob_output = ref NoGlob
-let dump () = !glob_output != NoGlob
+let dump () = !glob_output <> NoGlob
-let noglob () = glob_output := NoGlob
-
-let dump_to_dotglob () = glob_output := MultFiles
-
-let dump_into_file f =
- if String.equal f "stdout" then
- (glob_output := StdOut; glob_file := stdout)
- else
- (glob_output := File f; open_glob_file f)
-
-let feedback_glob () = glob_output := Feedback
+let set_glob_output mode =
+ glob_output := mode
let dump_string s =
- if dump () && !glob_output != Feedback then
+ if dump () && !glob_output != Feedback then
output_string !glob_file s
let start_dump_glob ~vfile ~vofile =
@@ -57,13 +47,13 @@ let start_dump_glob ~vfile ~vofile =
| File f ->
open_glob_file f;
output_string !glob_file "DIGEST NO\n"
- | NoGlob | Feedback | StdOut ->
+ | NoGlob | Feedback ->
()
let end_dump_glob () =
match !glob_output with
| MultFiles | File _ -> close_glob_file ()
- | NoGlob | Feedback | StdOut -> ()
+ | NoGlob | Feedback -> ()
let previous_state = ref MultFiles
let pause () = previous_state := !glob_output; glob_output := NoGlob
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 60d62a1cb2..2b6a116a01 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -8,19 +8,19 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-val open_glob_file : string -> unit
-val close_glob_file : unit -> unit
-
val start_dump_glob : vfile:string -> vofile:string -> unit
val end_dump_glob : unit -> unit
val dump : unit -> bool
-val noglob : unit -> unit
-val dump_into_file : string -> unit (** special handling of "stdout" *)
+type glob_output =
+ | NoGlob
+ | Feedback
+ | MultFiles (* one glob file per .v file *)
+ | File of string (* Single file for all coqc arguments *)
-val dump_to_dotglob : unit -> unit
-val feedback_glob : unit -> unit
+(* Default "NoGlob" *)
+val set_glob_output : glob_output -> unit
val pause : unit -> unit
val continue : unit -> unit
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index 60c8fb4449..b241fdc6cc 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -21,7 +21,7 @@ val contents : aux_file -> string M.t H.t
val aux_file_name_for : string -> string
val start_aux_file : aux_file:string -> v_file:string -> unit
-val stop_aux_file : unit -> unit
+val stop_aux_file : unit -> unit
val recording : unit -> bool
val record_in_aux_at : ?loc:Loc.t -> string -> string -> unit
diff --git a/lib/flags.ml b/lib/flags.ml
index 190de5853d..f09dc48f5d 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 record_aux_file = ref false
-
let async_proofs_worker_id = ref "master"
let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
diff --git a/lib/flags.mli b/lib/flags.mli
index 1c96796220..185a5f8425 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -31,10 +31,6 @@
(** Command-line flags *)
-(** 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
-
(** Async-related flags *)
val async_proofs_worker_id : string ref
val async_proofs_is_worker : unit -> bool
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index fab6767beb..baa7b3570c 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -11,7 +11,6 @@
open Util
let check_vio (ts,f_in) =
- Dumpglob.noglob ();
let _, _, _, tasks, _ = Library.load_library_todo f_in in
Stm.set_compilation_hints f_in;
List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts
@@ -142,5 +141,3 @@ let schedule_vio_compilation j fs =
List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs;
end;
exit !rc
-
-
diff --git a/tactics/declare.ml b/tactics/declare.ml
index c280760e84..c23ee4a76e 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -224,7 +224,7 @@ let cast_opaque_proof_entry e =
let vars = global_vars_set env pf in
ids_typ, vars
in
- let () = if !Flags.record_aux_file then record_aux env hyp_typ hyp_def in
+ let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in
keep_hyps env (Id.Set.union hyp_typ hyp_def)
| Some hyps -> hyps
in
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index d8a3dbb4bb..fe5361c156 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -108,8 +108,6 @@ let compile opts copts ~echo ~f_in ~f_out =
in
match copts.compilation_mode with
| BuildVo ->
- Flags.record_aux_file := true;
-
let long_f_dot_v, long_f_dot_vo =
ensure_exists_with_prefix f_in f_out ".v" ".vo" in
@@ -124,8 +122,11 @@ let compile opts copts ~echo ~f_in ~f_out =
Aux_file.(start_aux_file
~aux_file:(aux_file_name_for long_f_dot_vo)
~v_file:long_f_dot_v);
+
+ Dumpglob.set_glob_output copts.glob_out;
Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
+
let wall_clock1 = Unix.gettimeofday () in
let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in
let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_v in
@@ -139,9 +140,6 @@ let compile opts copts ~echo ~f_in ~f_out =
Dumpglob.end_dump_glob ()
| BuildVio ->
- Flags.record_aux_file := false;
- Dumpglob.noglob ();
-
let long_f_dot_v, long_f_dot_vio =
ensure_exists_with_prefix f_in f_out ".v" ".vio" in
@@ -174,9 +172,6 @@ let compile opts copts ~echo ~f_in ~f_out =
Stm.reset_task_queue ()
| Vio2Vo ->
-
- Flags.record_aux_file := false;
- Dumpglob.noglob ();
let long_f_dot_vio, long_f_dot_vo =
ensure_exists_with_prefix f_in f_out ".vio" ".vo" in
let sum, lib, univs, tasks, proofs =
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 67d70416c8..64c1da20b6 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -59,7 +59,6 @@ type coqargs_config = {
debug : bool;
diffs_set : bool;
time : bool;
- glob_opt : bool;
print_emacs : bool;
set_options : (Goptions.option_name * option_command) list;
}
@@ -125,7 +124,6 @@ let default_config = {
debug = false;
diffs_set = false;
time = false;
- glob_opt = false;
print_emacs = false;
set_options = [];
@@ -380,13 +378,6 @@ let parse_args ~help ~init arglist : t * string list =
Flags.compat_version := v;
add_compat_require oval v
- |"-dump-glob" ->
- Dumpglob.dump_into_file (next ());
- { oval with config = { oval.config with glob_opt = true }}
-
- |"-feedback-glob" ->
- Dumpglob.feedback_glob (); oval
-
|"-exclude-dir" ->
System.exclude_directory (next ()); oval
@@ -524,7 +515,6 @@ 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 }}
- |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with config = { oval.config with glob_opt = 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; }}
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index e414888861..26f22386a0 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -35,7 +35,6 @@ type coqargs_config = {
debug : bool;
diffs_set : bool;
time : bool;
- glob_opt : bool;
print_emacs : bool;
set_options : (Goptions.option_name * option_command) list;
}
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index 5678acb2b1..019577ac85 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -16,8 +16,7 @@ let outputstate opts =
let coqc_init _copts ~opts =
Flags.quiet := true;
System.trust_file_cache := true;
- Coqtop.init_color opts.Coqargs.config;
- if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob ()
+ Coqtop.init_color opts.Coqargs.config
let coqc_specific_usage = Usage.{
executable_name = "coqc";
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index 5cced2baac..0b5481fe72 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -23,7 +23,8 @@ type t =
; echo : bool
- ; outputstate : string option;
+ ; outputstate : string option
+ ; glob_out : Dumpglob.glob_output
}
let default =
@@ -40,6 +41,7 @@ let default =
; echo = false
; outputstate = None
+ ; glob_out = Dumpglob.MultFiles
}
let depr opt =
@@ -187,6 +189,15 @@ let parse arglist : t =
| "-outputstate" ->
set_outputstate oval (next ())
+ (* Glob options *)
+ |"-no-glob" | "-noglob" ->
+ { oval with glob_out = Dumpglob.NoGlob }
+
+ |"-dump-glob" ->
+ let file = next () in
+ { oval with glob_out = Dumpglob.File file }
+
+ (* Rest *)
| s ->
extras := s :: !extras;
oval
diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli
index b02eeeb9ee..13bea3bf3e 100644
--- a/toplevel/coqcargs.mli
+++ b/toplevel/coqcargs.mli
@@ -24,6 +24,7 @@ type t =
; echo : bool
; outputstate : string option
+ ; glob_out : Dumpglob.glob_output
}
val default : t
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 78640334e2..07466d641e 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -438,19 +438,15 @@ let rec loop ~state =
loop ~state
(* Default toplevel loop *)
-let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s))
let drop_args = ref None
+
let loop ~opts ~state =
drop_args := Some opts;
let open Coqargs in
print_emacs := opts.config.print_emacs;
(* We initialize the console only if we run the toploop_run *)
let tl_feed = Feedback.add_feeder coqloop_feed in
- if Dumpglob.dump () then begin
- Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
- Dumpglob.noglob ()
- end;
let _ = loop ~state in
(* Initialise and launch the Ocaml toplevel *)
Coqinit.init_ocaml_path();
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 094e2c1184..cfb3248c7b 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -130,7 +130,7 @@ let suggest_common env ppid used ids_typ skip =
str "should start with one of the following commands:"++spc()++
v 0 (
prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs));
- if !Flags.record_aux_file
+ if Aux_file.recording ()
then
let s = string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs) in
record_proof_using s
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:16:54 +0000