aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore2
-rw-r--r--CHANGES2
-rw-r--r--checker/check.ml6
-rw-r--r--checker/cic.mli2
-rw-r--r--checker/values.ml2
-rw-r--r--doc/refman/AsyncProofs.tex28
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli2
-rw-r--r--stm/stm.ml14
-rw-r--r--stm/stm.mli8
-rw-r--r--stm/stm.mllib2
-rw-r--r--stm/vio_checking.ml (renamed from stm/vi_checking.ml)18
-rw-r--r--stm/vio_checking.mli (renamed from stm/vi_checking.mli)8
-rw-r--r--test-suite/Makefile18
-rw-r--r--test-suite/vio/simple.v (renamed from test-suite/vi/simple.v)0
-rw-r--r--test-suite/vio/univ_constraints_statements.v (renamed from test-suite/vi/univ_constraints_statements.v)0
-rw-r--r--tools/coq_makefile.ml10
-rw-r--r--tools/coqc.ml4
-rw-r--r--tools/coqdep_common.ml4
-rw-r--r--toplevel/coqtop.ml78
-rw-r--r--toplevel/vernac.ml8
21 files changed, 110 insertions, 108 deletions
diff --git a/.gitignore b/.gitignore
index cb728ea75..54b9d10b5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,7 +1,7 @@
*.glob
*.d
*.d.raw
-*.vi
+*.vio
*.vo
*.cm*
*.annot
diff --git a/CHANGES b/CHANGES
index 075d1bcf8..c9e0ebfd2 100644
--- a/CHANGES
+++ b/CHANGES
@@ -282,7 +282,7 @@ Tools
added to the load path. (Same behavior as with coq/user-contrib.)
- coqdep accepts a -dumpgraph option generating a dot file.
- Makefiles generated through coq_makefile have three new targets "quick"
- "checkproof" and "vi2vo", allowing respectively to asynchronously compile
+ "checkproof" and "vio2vo", allowing respectively to asynchronously compile
the files without playing the proof scripts, asynchronously checking
that the quickly generated proofs are correct and generating the object
files from the quickly generated proofs.
diff --git a/checker/check.ml b/checker/check.ml
index 1f84b56b5..bda0224ee 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -332,10 +332,10 @@ let intern_from_file (dir, f) =
errorlabstrm "intern_from_file"
(str "The file "++str f++str " contains unfinished tasks");
if opaque_csts <> None then begin
- pp (str " (was a vi file) ");
+ pp (str " (was a vio file) ");
Option.iter (fun (_,_,b) -> if not b then
errorlabstrm "intern_from_file"
- (str "The file "++str f++str " is still a .vi"))
+ (str "The file "++str f++str " is still a .vio"))
opaque_csts;
Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
end;
@@ -344,7 +344,7 @@ let intern_from_file (dir, f) =
Validate.validate !Flags.debug Values.v_opaques table;
Flags.if_verbose ppnl (str" done]"); pp_flush ();
let digest =
- if opaque_csts <> None then Cic.Dvivo (digest,udg)
+ if opaque_csts <> None then Cic.Dviovo (digest,udg)
else (Cic.Dvo digest) in
md,table,opaque_csts,digest
with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
diff --git a/checker/cic.mli b/checker/cic.mli
index 12146715a..c8b7c9e66 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -404,7 +404,7 @@ type compilation_unit_name = DirPath.t
type vodigest =
| Dvo of Digest.t (* The digest of the seg_lib part *)
- | Dvivo of Digest.t * Digest.t (* The digest of the seg_lib + seg_univ part *)
+ | Dviovo of Digest.t * Digest.t (* The digest of the seg_lib+seg_univ part *)
type library_info = compilation_unit_name * vodigest
diff --git a/checker/values.ml b/checker/values.ml
index ea3df47f5..0ac8bf78c 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 ed14962eac3aa2feba45a572f72b9531 checker/cic.mli
+MD5 27f35ee65fef280d5a7a80bb11b31837 checker/cic.mli
*)
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 65ac2c8a2..bef746729 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -98,14 +98,14 @@ Coq need to process all the proofs of the $.v$ file.
The asynchronous processing of proofs can decouple the generation of a
compiled file (like the $.vo$ one) that can be $Required$ from the generation
and checking of the proof objects. The $-quick$ flag can be passed to
-$coqc$ or $coqtop$ to produce, quickly, $.vi$ files. Alternatively, if
+$coqc$ or $coqtop$ to produce, quickly, $.vio$ files. Alternatively, if
the $Makefile$ one uses was produced by $coq\_makefile$ the $quick$
target can be used to compile all files using the $-quick$ flag.
-A $.vi$ file can be $Required$ exactly as a $.vo$ file but: 1) proofs are
+A $.vio$ file can be $Required$ exactly as a $.vo$ file but: 1) proofs are
not available (the $Print$ command produces an error); 2) some universe
constraints are missing, hence universes inconsistencies may not be
-discovered. A $.vi$ file does not contain proof objects, but proof tasks,
+discovered. A $.vio$ file does not contain proof objects, but proof tasks,
i.e. what a worker process can transform into a proof object.
Compiling a set of files with the $-quick$ flag allows one to work,
@@ -114,30 +114,30 @@ interactively, on any file without waiting for all proofs to be checked.
While one works interactively, he can fully check all $.v$ files by
running $coqc$ as usual.
-Alternatively one can turn each $.vi$ into the corresponding $.vo$.
-All $.vi$ files can be processed in parallel, hence this alternative
-may be faster. The command $coqtop -schedule-vi2vo 2 a b c$
+Alternatively one can turn each $.vio$ into the corresponding $.vo$.
+All $.vio$ files can be processed in parallel, hence this alternative
+may be faster. The command $coqtop -schedule-vio2vo 2 a b c$
can be used to obtain a good scheduling for 2 workers to produce
$a.vo$, $b.vo$ and $c.vo$. If the $Makefile$ one uses was produced
-by $coq\_makefile$ the $vi2vo$ target can be used for that.
+by $coq\_makefile$ the $vio2vo$ target can be used for that.
The variable $J$ should be set to the number of workers, like
-in $make vi2vo J=2$. The only caveat is that, while the $.vo$ file
-obtained from $.vi$ files are complete (they contain all proof terms
+in $make vio2vo J=2$. The only caveat is that, while the $.vo$ file
+obtained from $.vio$ files are complete (they contain all proof terms
and universe constraints) the satisfiability of all universe constraints
has not been checked globally (they are checked to be consistent for
every single proof). Constraints will be checked when these $.vo$ files
are (recursively) loaded with $Require$.
There is an extra, possibly even faster, alternative: just check
-the proof tasks store in $.vi$ files without producing the $.vo$ files.
+the proof tasks store in $.vio$ files without producing the $.vo$ files.
This is possibly faster because all proof tasks are independent, hence
one can further partition the job to be done between workers.
-The $coqtop -schedule-vi-checking 6 a b c$ command can be used to obtain
-a good scheduling for 6 workers to check all proof tasks of $a.vi$, $b.vi$ and
-$c.vi$. Auxiliary files are used to predict how long a proof task will take,
+The $coqtop -schedule-vio-checking 6 a b c$ command can be used to obtain
+a good scheduling for 6 workers to check all proof tasks of $a.vio$, $b.vio$ and
+$c.vio$. Auxiliary files are used to predict how long a proof task will take,
assuming it will take the same amount of time it took last time.
If the $Makefile$ one uses was produced by $coq\_makefile$ the $checkproofs$
-target can be used to check all $.vi$ files. The variable $J$ should be
+target can be used to check all $.vio$ files. The variable $J$ should be
set to the number of workers, like in $make checkproofs J=6$.
Checking all proof tasks does not guarantee the same degree of safety
that producing a $.vo$ file gives. In particular universe constraints
diff --git a/lib/flags.ml b/lib/flags.ml
index 9c718743d..ad69c5a2b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -45,7 +45,7 @@ let boot = ref false
let load_init = ref true
let batch_mode = ref false
-type compilation_mode = BuildVo | BuildVi | Vi2Vo
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
let compilation_mode = ref BuildVo
type async_proofs = APoff | APonLazy | APon
diff --git a/lib/flags.mli b/lib/flags.mli
index fbb2f817a..c35943e53 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -12,7 +12,7 @@ val boot : bool ref
val load_init : bool ref
val batch_mode : bool ref
-type compilation_mode = BuildVo | BuildVi | Vi2Vo
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
val compilation_mode : compilation_mode ref
type async_proofs = APoff | APonLazy | APon
diff --git a/stm/stm.ml b/stm/stm.ml
index 1dff4ae94..4afdb06a1 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1145,7 +1145,7 @@ end = struct (* {{{ *)
VCS.restore document;
try
Reach.known_state ~cache:`No stop;
- (* The original terminator, a hook, has not been saved in the .vi*)
+ (* The original terminator, a hook, has not been saved in the .vio*)
Proof_global.set_terminator
(Lemmas.standard_proof_terminator []
(Lemmas.mk_hook (fun _ _ -> ())));
@@ -1245,7 +1245,7 @@ end = struct (* {{{ *)
let id, valid as t_exn_info = exn_info in
let cancel_switch = ref false in
if TaskQueue.n_workers (Option.get !queue) = 0 then
- if !Flags.compilation_mode = Flags.BuildVi then begin
+ if !Flags.compilation_mode = Flags.BuildVio then begin
let f,assign =
Future.create_delegate ~blocking:true (State.exn_on id ~valid) in
let t_uuid = Future.uuid f in
@@ -1536,11 +1536,11 @@ let async_policy () =
if interactive () = `Yes then
(async_proofs_is_master () || !async_proofs_mode = Flags.APonLazy)
else
- (!compilation_mode = Flags.BuildVi || !async_proofs_mode <> Flags.APoff)
+ (!compilation_mode = Flags.BuildVio || !async_proofs_mode <> Flags.APoff)
let delegate name =
let time = get_hint_bp_time name in
- time >= 1.0 || !Flags.compilation_mode = Flags.BuildVi
+ time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
let collect_proof keep cur hd brkind id =
prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
@@ -1579,7 +1579,7 @@ let collect_proof keep cur hd brkind id =
`ASync (parent last,proof_using_ast last,accn,name,delegate name)
| `Fork((_, hd', GuaranteesOpacity, ids), _) when
has_proof_no_using last && not (State.is_cached (parent last)) &&
- !Flags.compilation_mode = Flags.BuildVi ->
+ !Flags.compilation_mode = Flags.BuildVio ->
assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
(try
let name, hint = name ids, get_hint_ctx loc in
@@ -1903,10 +1903,10 @@ let handle_failure (e, info) vcs tty =
VCS.print ();
iraise (e, info)
-let snapshot_vi ldir long_f_dot_v =
+let snapshot_vio ldir long_f_dot_v =
finish ();
if List.length (VCS.branches ()) > 1 then
- Errors.errorlabstrm "stm" (str"Cannot dump a vi with open proofs");
+ Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v
(Global.opaque_tables ())
diff --git a/stm/stm.mli b/stm/stm.mli
index 715997aee..2cbd54dd5 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -49,18 +49,18 @@ val stop_worker : string -> unit
(* Joins the entire document. Implies finish, but also checks proofs *)
val join : unit -> unit
-(* Saves on the dist a .vi corresponding to the current status:
+(* Saves on the dist a .vio corresponding to the current status:
- if the worker prool is empty, all tasks are saved
- if the worker proof is not empty, then it waits until all workers
are done with their current jobs and then dumps (or fails if one
of the completed tasks is a failuere) *)
-val snapshot_vi : DirPath.t -> string -> unit
+val snapshot_vio : DirPath.t -> string -> unit
(* Empties the task queue, can be used only if the worker pool is empty (E.g.
- * after having built a .vi in batch mode *)
+ * after having built a .vio in batch mode *)
val reset_task_queue : unit -> unit
-(* A .vi contains tasks to be completed *)
+(* A .vio contains tasks to be completed *)
type tasks
val check_task : string -> tasks -> int -> bool
val info_tasks : tasks -> (string * float * int) list
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 2b5ff8c04..92b3a869a 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -9,4 +9,4 @@ CoqworkmgrApi
AsyncTaskQueue
Texmacspp
Stm
-Vi_checking
+Vio_checking
diff --git a/stm/vi_checking.ml b/stm/vio_checking.ml
index 925a2a89e..3922af6e1 100644
--- a/stm/vi_checking.ml
+++ b/stm/vio_checking.ml
@@ -8,7 +8,7 @@
open Util
-let check_vi (ts,f) =
+let check_vio (ts,f) =
Dumpglob.noglob ();
let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints long_f_dot_v;
@@ -23,12 +23,12 @@ end
module Pool = Map.Make(IntOT)
-let schedule_vi_checking j fs =
+let schedule_vio_checking j fs =
if j < 1 then Errors.error "The number of workers must be bigger than 0";
let jobs = ref [] in
List.iter (fun f ->
let f =
- if Filename.check_suffix f ".vi" then Filename.chop_extension f
+ if Filename.check_suffix f ".vio" then Filename.chop_extension f
else f in
let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints long_f_dot_v;
@@ -42,7 +42,7 @@ let schedule_vi_checking j fs =
let pool : Worker.process Pool.t ref = ref Pool.empty in
let rec filter_argv b = function
| [] -> []
- | "-schedule-vi-checking" :: rest -> filter_argv true rest
+ | "-schedule-vio-checking" :: rest -> filter_argv true rest
| s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
| _ :: rest when b -> filter_argv b rest
| s :: rest -> s :: filter_argv b rest in
@@ -81,7 +81,7 @@ let schedule_vi_checking j fs =
let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in
List.flatten
(List.map (fun (f, tl) ->
- "-check-vi-tasks" ::
+ "-check-vio-tasks" ::
String.concat "," (List.map string_of_int tl) :: [f])
(pack (List.sort cmp_job !what))) in
let rc = ref 0 in
@@ -97,12 +97,12 @@ let schedule_vi_checking j fs =
done;
exit !rc
-let schedule_vi_compilation j fs =
+let schedule_vio_compilation j fs =
if j < 1 then Errors.error "The number of workers must be bigger than 0";
let jobs = ref [] in
List.iter (fun f ->
let f =
- if Filename.check_suffix f ".vi" then Filename.chop_extension f
+ if Filename.check_suffix f ".vio" then Filename.chop_extension f
else f in
let paths = Loadpath.get_paths () in
let _, long_f_dot_v =
@@ -118,7 +118,7 @@ let schedule_vi_compilation j fs =
let pool : Worker.process Pool.t ref = ref Pool.empty in
let rec filter_argv b = function
| [] -> []
- | "-schedule-vi2vo" :: rest -> filter_argv true rest
+ | "-schedule-vio2vo" :: rest -> filter_argv true rest
| s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
| _ :: rest when b -> filter_argv b rest
| s :: rest -> s :: filter_argv b rest in
@@ -127,7 +127,7 @@ let schedule_vi_compilation j fs =
let make_job () =
let f, t = List.hd !jobs in
jobs := List.tl !jobs;
- [ "-vi2vo"; f ] in
+ [ "-vio2vo"; f ] in
let rc = ref 0 in
while !jobs <> [] || Pool.cardinal !pool > 0 do
while Pool.cardinal !pool < j && !jobs <> [] do
diff --git a/stm/vi_checking.mli b/stm/vio_checking.mli
index 65414eda4..fb1a0beca 100644
--- a/stm/vi_checking.mli
+++ b/stm/vio_checking.mli
@@ -6,8 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* [check_vi tasks file] checks the [tasks] stored in [file] *)
-val check_vi : int list * string -> bool
-val schedule_vi_checking : int -> string list -> unit
+(* [check_vio tasks file] checks the [tasks] stored in [file] *)
+val check_vio : int list * string -> bool
+val schedule_vio_checking : int -> string list -> unit
-val schedule_vi_compilation : int -> string list -> unit
+val schedule_vio_compilation : int -> string list -> unit
diff --git a/test-suite/Makefile b/test-suite/Makefile
index d5adc4e5f..b2f8ad79d 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -82,7 +82,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
interactive micromega $(COMPLEXITY) modules stm
# All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vi coqchk
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
#######################################################################
# Phony targets
@@ -99,9 +99,9 @@ bugs: $(BUGS)
clean:
rm -f trace lia.cache
- $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.vi> <**/*.log>"
+ $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>"
$(HIDE)find . \( \
- -name '*.stamp' -o -name '*.vo' -o -name '*.vi' -o -name '*.log' \
+ -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \
\) -print0 | xargs -0 rm -f
distclean: clean
@@ -140,7 +140,7 @@ summary:
$(call summary_dir, "Module tests", modules); \
$(call summary_dir, "STM tests", stm); \
$(call summary_dir, "IDE tests", ide); \
- $(call summary_dir, "VI tests", vi); \
+ $(call summary_dir, "VI tests", vio); \
$(call summary_dir, "Coqchk tests", coqchk); \
nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
@@ -428,14 +428,14 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
fi; \
} > "$@"
-vi: $(patsubst %.v,%.vi.log,$(wildcard vi/*.v))
+vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
-%.vi.log:%.v
+%.vio.log:%.v
@echo "TEST $<"
$(HIDE){ \
- $(bincoqc) -quick -R vi vi $* 2>&1 && \
- $(coqtop) -R vi vi -vi2vo $*.vi 2>&1 && \
- $(bincoqchk) -R vi vi $(subst /,.,$*) 2>&1; \
+ $(bincoqc) -quick -R vio vio $* 2>&1 && \
+ $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \
+ $(bincoqchk) -R vio vio $(subst /,.,$*) 2>&1; \
if [ $$? = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
diff --git a/test-suite/vi/simple.v b/test-suite/vio/simple.v
index 407074c1e..407074c1e 100644
--- a/test-suite/vi/simple.v
+++ b/test-suite/vio/simple.v
diff --git a/test-suite/vi/univ_constraints_statements.v b/test-suite/vio/univ_constraints_statements.v
index bb6b95957..bb6b95957 100644
--- a/test-suite/vi/univ_constraints_statements.v
+++ b/test-suite/vio/univ_constraints_statements.v
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index c8087f7f1..159d48599 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -329,7 +329,7 @@ let clean sds sps =
print "\trm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))\n";
end;
if !some_vfile then
- print "\trm -f $(VOFILES) $(VOFILES:.vo=.vi) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n";
+ print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n";
print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n";
print "\t- rm -rf html mlihtml uninstall_me.sh\n";
List.iter
@@ -389,7 +389,7 @@ in
let v_rules () =
print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
- print "$(VFILES:.v=.vi): %.vi: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n";
+ print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n";
print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n";
print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n";
print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n";
@@ -660,9 +660,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
end;
if !some_vfile then
begin
- print "quick:\n\t$(MAKE) -f $(firstword $(MAKEFILE_LIST)) all VO=vi\n";
- print "vi2vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vi2vo $(J) $(VOFILES:%.vo=%.vi)\n";
- print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vi-checking $(J) $(VOFILES:%.vo=%.vi)\n";
+ print "quick: $(VOFILES:.vo=.vio)\n\n";
+ print "vio2vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)\n";
+ print "checkproofs:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)\n";
print "gallina: $(GFILES)\n\n";
print "html: $(GLOBFILES) $(VFILES)\n";
print "\t- mkdir -p html\n";
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 12de061e0..bb15a2941 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -144,8 +144,8 @@ let parse_args () =
| "-R" :: s :: "-as" :: [] -> usage ()
| "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
| "-Q" :: s :: t :: rem -> parse (cfiles,t::s::"-Q"::args) rem
- | ("-schedule-vi-checking"
- |"-check-vi-tasks" | "-schedule-vi2vo" as o) :: s :: rem ->
+ | ("-schedule-vio-checking"
+ |"-check-vio-tasks" | "-schedule-vio2vo" as o) :: s :: rem ->
let nodash, rem =
CList.split_when (fun x -> String.length x > 1 && x.[0] = '-') rem in
extra_arg_needed := false;
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 3dd6cb444..10150497d 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -427,8 +427,8 @@ let coq_dependencies () =
printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename;
traite_fichier_Coq !suffixe true (name ^ ".v");
printf "\n";
- printf "%s.vi: %s.v" ename ename;
- traite_fichier_Coq ".vi" true (name ^ ".v");
+ printf "%s.vio: %s.v" ename ename;
+ traite_fichier_Coq ".vio" true (name ^ ".v");
printf "\n";
flush stdout)
(List.rev !vAccu)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5e5d39ce6..2dcdc7bb7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -159,9 +159,10 @@ let load_vernac_obj () =
let require_prelude () =
let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in
- let vi = Envars.coqlib () / "theories/Init/Prelude.vi" in
+ let vio = Envars.coqlib () / "theories/Init/Prelude.vio" in
let m =
- if Sys.file_exists vo then vo else if Sys.file_exists vi then vi else vo in
+ if Sys.file_exists vo then vo else
+ if Sys.file_exists vio then vio else vo in
Library.require_library_from_dirpath [Coqlib.prelude_module,m] (Some true)
let require_list = ref ([] : string list)
@@ -333,45 +334,46 @@ let get_host_port opt s =
let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
-let vi_tasks = ref []
+let vio_tasks = ref []
-let add_vi_task f =
+let add_vio_task f =
set_batch_mode ();
Flags.make_silent true;
- vi_tasks := f :: !vi_tasks
+ vio_tasks := f :: !vio_tasks
-let check_vi_tasks () =
+let check_vio_tasks () =
let rc =
- List.fold_left (fun acc t -> Vi_checking.check_vi t && acc)
- true (List.rev !vi_tasks) in
+ List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
+ true (List.rev !vio_tasks) in
if not rc then exit 1
-let vi_files = ref []
-let vi_files_j = ref 0
-let vi_checking = ref false
-let add_vi_file f =
+let vio_files = ref []
+let vio_files_j = ref 0
+let vio_checking = ref false
+let add_vio_file f =
set_batch_mode ();
Flags.make_silent true;
- vi_files := f :: !vi_files
-let set_vi_checking_j opt j =
- try vi_files_j := int_of_string j
+ vio_files := f :: !vio_files
+
+let set_vio_checking_j opt j =
+ try vio_files_j := int_of_string j
with Failure _ ->
prerr_endline ("The first argument of " ^ opt ^ " must the number");
prerr_endline "of concurrent workers to be used (a positive integer).";
prerr_endline "Makefiles generated by coq_makefile should be called";
- prerr_endline "setting the J variable like in 'make vi2vo J=3'";
+ prerr_endline "setting the J variable like in 'make vio2vo J=3'";
exit 1
let is_not_dash_option = function
| Some f when String.length f > 0 && f.[0] <> '-' -> true
| _ -> false
-let schedule_vi_checking () =
- if !vi_files <> [] && !vi_checking then
- Vi_checking.schedule_vi_checking !vi_files_j !vi_files
-let schedule_vi_compilation () =
- if !vi_files <> [] && not !vi_checking then
- Vi_checking.schedule_vi_compilation !vi_files_j !vi_files
+let schedule_vio_checking () =
+ if !vio_files <> [] && !vio_checking then
+ Vio_checking.schedule_vio_checking !vio_files_j !vio_files
+let schedule_vio_compilation () =
+ if !vio_files <> [] && not !vio_checking then
+ Vio_checking.schedule_vio_compilation !vio_files_j !vio_files
let parse_args arglist =
let args = ref arglist in
@@ -412,19 +414,19 @@ let parse_args arglist =
end
(* Options with two arg *)
- |"-check-vi-tasks" ->
+ |"-check-vio-tasks" ->
let tno = get_task_list (next ()) in
let tfile = next () in
- add_vi_task (tno,tfile)
- |"-schedule-vi-checking" ->
- vi_checking := true;
- set_vi_checking_j opt (next ());
- add_vi_file (next ());
- while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done
- |"-schedule-vi2vo" ->
- set_vi_checking_j opt (next ());
- add_vi_file (next ());
- while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done
+ add_vio_task (tno,tfile)
+ |"-schedule-vio-checking" ->
+ vio_checking := true;
+ set_vio_checking_j opt (next ());
+ add_vio_file (next ());
+ while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done
+ |"-schedule-vio2vo" ->
+ set_vio_checking_j opt (next ());
+ add_vio_file (next ());
+ while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done
(* Options with one arg *)
|"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
@@ -461,7 +463,7 @@ let parse_args arglist =
|"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
|"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
|"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
- |"-vi2vo" -> add_compile false (next ()); Flags.compilation_mode := Vi2Vo
+ |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
|"-toploop" -> toploop := Some (next ())
(* Options with zero arg *)
@@ -494,7 +496,7 @@ let parse_args arglist =
|"-output-context" -> output_context := true
|"-q" -> no_load_rc ()
|"-quiet"|"-silent" -> Flags.make_silent true
- |"-quick" -> Flags.compilation_mode := BuildVi
+ |"-quick" -> Flags.compilation_mode := BuildVio
|"-list-tags" -> print_tags := true
|"-time" -> Flags.time := true
|"-type-in-type" -> set_type_in_type ()
@@ -577,9 +579,9 @@ let init arglist =
load_rcfile();
load_vernacular ();
compile_files ();
- schedule_vi_checking ();
- schedule_vi_compilation ();
- check_vi_tasks ();
+ schedule_vio_checking ();
+ schedule_vio_compilation ();
+ check_vio_tasks ();
outputstate ()
with any ->
let any = Errors.push any in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index e5c9849a9..682a06f78 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -326,20 +326,20 @@ let compile verbosely f =
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
Aux_file.stop_aux_file ();
Dumpglob.end_dump_glob ()
- | BuildVi ->
+ | BuildVio ->
let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
Dumpglob.noglob ();
Stm.set_compilation_hints long_f_dot_v;
let _ = load_vernac verbosely long_f_dot_v in
Stm.finish ();
check_pending_proofs ();
- Stm.snapshot_vi ldir long_f_dot_v;
+ Stm.snapshot_vio ldir long_f_dot_v;
Stm.reset_task_queue ()
- | Vi2Vo ->
+ | Vio2Vo ->
let open Filename in
let open Library in
Dumpglob.noglob ();
- let f = if check_suffix f ".vi" then chop_extension f else f in
+ let f = if check_suffix f ".vio" then chop_extension f else f in
let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
Stm.set_compilation_hints lfdv;
let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 01:47:58 +0000