aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.build4
-rw-r--r--Makefile.common4
-rw-r--r--lib/flags.ml4
-rw-r--r--lib/flags.mli2
-rw-r--r--scripts/coqc.ml7
-rw-r--r--tools/coq_makefile.ml48
-rw-r--r--tools/coqdep.ml6
-rw-r--r--toplevel/coqtop.ml8
-rw-r--r--toplevel/usage.ml2
-rw-r--r--toplevel/vernac.ml20
10 files changed, 41 insertions, 24 deletions
diff --git a/Makefile.build b/Makefile.build
index a87d0032b..e91ffb86a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -563,7 +563,7 @@ states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/M
theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY)
$(SHOW)'COQC -nois $<'
$(HIDE)rm -f theories/Init/$*.glob
- $(HIDE)$(BOOTCOQTOP) -dump-glob theories/Init/$*.glob -nois -compile theories/Init/$*
+ $(HIDE)$(BOOTCOQTOP) -nois -compile theories/Init/$*
theories/Numbers/Natural/BigN/NMake.v: theories/Numbers/Natural/BigN/NMake_gen.ml
$(OCAML) $< > $@
@@ -875,7 +875,7 @@ endif
%.vo %.glob: %.v states/initial.coq $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY)
$(SHOW)'COQC $<'
$(HIDE)rm -f $*.glob
- $(HIDE)$(BOOTCOQTOP) -dump-glob $*.glob -compile $*
+ $(HIDE)$(BOOTCOQTOP) -compile $*
ifdef VALIDATE
$(SHOW)'COQCHK $(shell basename $*)'
$(HIDE)$(BESTCHICKEN) -silent -norec $(shell basename $*) \
diff --git a/Makefile.common b/Makefile.common
index 3ba85f9a4..158617045 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -357,8 +357,8 @@ COQIDECMX:=$(COQIDECMO:.cmo=.cmx)
COQMKTOPCMO:=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo
COQMKTOPCMX:=config/coq_config.cmx scripts/tolink.cmx scripts/coqmktop.cmx
-COQCCMO:=$(CONFIG) toplevel/usage.cmo scripts/coqc.cmo
-COQCCMX:=config/coq_config.cmx toplevel/usage.cmx scripts/coqc.cmx
+COQCCMO:=$(CONFIG) toplevel/usage.cmo lib/pp_control.cmo lib/pp.cmo scripts/coqc.cmo
+COQCCMX:=config/coq_config.cmx toplevel/usage.cmx lib/pp_control.cmx lib/pp.cmx scripts/coqc.cmx
INTERFACE:=\
contrib/interface/vtp.cmo contrib/interface/xlate.cmo \
diff --git a/lib/flags.ml b/lib/flags.ml
index dbb8c38ab..68e287f69 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -84,6 +84,7 @@ let is_unsafe s = Stringset.mem s !unsafe_set
(* Dump of globalization (to be used by coqdoc) *)
+let noglob = ref false
let dump = ref false
let dump_file = ref ""
let dump_into_file f = dump := true; dump_file := f
@@ -94,9 +95,10 @@ let dump_string = Buffer.add_string dump_buffer
let dump_it () =
if !dump then begin
- let mode = [Open_wronly; Open_append; Open_creat] in
+ let mode = [Open_wronly; Open_creat] in
let c = open_out_gen mode 0o666 !dump_file in
output_string c (Buffer.contents dump_buffer);
+ Buffer.clear dump_buffer;
close_out c
end
diff --git a/lib/flags.mli b/lib/flags.mli
index 2301d8a0d..08f9a279d 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -59,9 +59,11 @@ val is_unsafe : string -> bool
(* Dump of globalization (to be used by coqdoc) *)
+val noglob : bool ref
val dump : bool ref
val dump_into_file : string -> unit
val dump_string : string -> unit
+val dump_it : unit -> unit
(* Options for the virtual machine *)
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 673567a85..84f12049a 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -141,7 +141,7 @@ let parse_args () =
| ("-I"|"-include"|"-outputstate"
|"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object"
|"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
- |"-init-file"|"-dump-glob" as o) :: rem ->
+ |"-init-file" as o) :: rem ->
begin
match rem with
| s :: rem' -> parse (cfiles,s::o::args) rem'
@@ -151,13 +151,16 @@ let parse_args () =
| ("-notactics"|"-debug"|"-nolib"
| "-debugVM"|"-alltransp"|"-VMno"
- |"-batch"|"-nois"
+ |"-batch"|"-nois" | "-noglob" | "-no-glob"
|"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
|"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-translate" |"-strict-implicit"
|"-dont-load-proofs"|"-impredicative-set"|"-vm"
| "-unboxed-values" | "-unboxed-definitions" | "-draw-vm-instr"
as o) :: rem ->
parse (cfiles,o::args) rem
+
+ | "-dump-glob" :: _ :: rem -> Pp.msg_warning (Pp.str "option -dumpglob is obsolete"); parse (cfiles,args) rem
+
| "-where" :: _ ->
let coqlib =
try Sys.getenv "COQLIB" with Not_found -> Coq_config.coqlib
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 3138ce4ef..2dfac4e18 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -136,15 +136,15 @@ let implicit () =
print "%.ml.d: %.ml\n";
print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) \"$<\" > \"$@\"\n\n"
and v_rule () =
- print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n";
+ print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
print "%.g: %.v\n\t$(GALLINA) $<\n\n";
print "%.tex: %.v\n\t$(COQDOC) -latex $< -o $@\n\n";
- print "%.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html $< -o $@\n\n";
+ print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n";
print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n";
- print "%.g.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html -g $< -o $@\n\n";
+ print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n";
print "%.v.d: %.v\n";
- print "\t$(COQDEP) -glob -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
+ print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
in
if !some_mlfile then ml_rules ();
if !some_vfile then v_rule ()
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 84f9eb3ff..5a31a64d8 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -22,7 +22,7 @@ let option_D = ref false
let option_w = ref false
let option_i = ref false
let option_sort = ref false
-let option_glob = ref false
+let option_noglob = ref false
let option_slash = ref false
let option_boot = ref false
@@ -375,7 +375,7 @@ let mL_dependencies () =
let coq_dependencies () =
List.iter
(fun (name,_) ->
- let glob = if !option_glob then " "^name^".glob" else "" in
+ let glob = if !option_noglob then "" else " "^name^".glob" in
printf "%s%s%s: %s.v" name !suffixe glob name;
traite_fichier_Coq true (name ^ ".v");
printf "\n";
@@ -503,7 +503,7 @@ let rec parse = function
| "-i" :: ll -> option_i := true; parse ll
| "-boot" :: ll -> option_boot := true; parse ll
| "-sort" :: ll -> option_sort := true; parse ll
- | "-glob" :: ll -> option_glob := true; parse ll
+ | "-noglob" :: ll | "-no-glob" :: ll -> option_noglob := true; parse ll
| "-I" :: r :: ll -> add_dir add_known r []; parse ll
| "-I" :: [] -> usage ()
| "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0c9b12bb4..02044b2cf 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -113,6 +113,10 @@ let compile_files () =
(fun (v,f) ->
States.unfreeze init_state;
Constrintern.coqdoc_unfreeze coqdoc_init_state;
+ if !Flags.noglob then
+ Flags.dump := false
+ else
+ Flags.dump_into_file (f^".glob");
if Flags.do_translate () then
with_option translate_file (Vernac.compile v) f
else
@@ -231,8 +235,8 @@ let parse_args is_ide =
| "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
| "-load-vernac-object" :: [] -> usage ()
- | "-dump-glob" :: f :: rem -> dump_into_file f; parse rem
- | "-dump-glob" :: [] -> usage ()
+ | "-dump-glob" :: _ :: rem -> warning "option -dumpglob is obsolete"; parse rem
+ | ("-no-glob" | "-noglob") :: rem -> Flags.noglob := true; parse rem
| "-require" :: f :: rem -> add_require f; parse rem
| "-require" :: [] -> usage ()
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 4944bfede..e00f7808b 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -53,7 +53,7 @@ let print_usage_channel co command =
-batch batch mode (exits just after arguments parsing)
-boot boot mode (implies -q and -batch)
-emacs tells Coq it is executed under Emacs
- -dump-glob f dump globalizations in file f (to be used by coqdoc)
+ -no-glob f do not dump globalizations
-with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)
-impredicative-set set sort Set impredicative
-dont-load-proofs don't load opaque proofs in memory
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ac834b2a5..c0ec55228 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -226,11 +226,17 @@ let load_vernac verb file =
(* Compile a vernac file (f is assumed without .v suffix) *)
let compile verbosely f =
let ldir,long_f_dot_v = Library.start_library f in
- if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
- if !Flags.xml_export then !xml_start_library ();
- let _ = load_vernac verbosely long_f_dot_v in
- if Pfedit.get_all_proof_names () <> [] then
- (message "Error: There are pending proofs"; exit 1);
- if !Flags.xml_export then !xml_end_library ();
- Library.save_library_to ldir (long_f_dot_v ^ "o")
+ let dumpstate = !Flags.dump in
+ if not !Flags.noglob then
+ (Flags.dump_into_file (f ^ ".glob");
+ Flags.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"));
+ if !Flags.xml_export then !xml_start_library ();
+ let _ = load_vernac verbosely long_f_dot_v in
+ if Pfedit.get_all_proof_names () <> [] then
+ (message "Error: There are pending proofs"; exit 1);
+ if !Flags.xml_export then !xml_end_library ();
+ if !Flags.dump then Flags.dump_it ();
+ Flags.dump := dumpstate;
+ Library.save_library_to ldir (long_f_dot_v ^ "o")
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 10:26:23 +0000