diff options
35 files changed, 559 insertions, 170 deletions
diff --git a/.gitignore b/.gitignore index ad5204847c..7b3eadf33b 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,8 @@ *.d *.d.raw *.vio +*.vos +*.vok *.vo *.cm* *.annot diff --git a/Makefile.vofiles b/Makefile.vofiles index 5296ed43ff..97263ed9ea 100644 --- a/Makefile.vofiles +++ b/Makefile.vofiles @@ -49,7 +49,7 @@ endif else NATIVEFILES := endif -LIBFILES:=$(ALLVO:.$(VO)=.vo) $(NATIVEFILES) $(VFILES) $(GLOBFILES) +LIBFILES:=$(ALLVO:.$(VO)=.vo) $(ALLVO:.$(VO)=.vos) $(NATIVEFILES) $(VFILES) $(GLOBFILES) # For emacs: # Local Variables: diff --git a/doc/changelog/08-tools/08642-vos-files.rst b/doc/changelog/08-tools/08642-vos-files.rst new file mode 100644 index 0000000000..f612096880 --- /dev/null +++ b/doc/changelog/08-tools/08642-vos-files.rst @@ -0,0 +1,7 @@ +- `coqc` now provides the ability to generate compiled interfaces. + Use `coqc -vos foo.v` to skip all opaque proofs during the + compilation of `foo.v`, and output a file called `foo.vos`. + This feature is experimental. It enables working on a Coq file without the need to + first compile the proofs contained in its dependencies + (`#8642 <https://github.com/coq/coq/pull/8642>`_ by Arthur Charguéraud, review by + Maxime Dénès and Emilio Gallego). diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 48d5f4075e..70259ff565 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -184,6 +184,13 @@ and ``coqtop``, unless stated otherwise: :-verbose: Output the content of the input file as it is compiled. This option is available for ``coqc`` only; it is the counterpart of -compile-verbose. +:-vos: Indicate |Coq| to skip the processing of opaque proofs + (i.e., proofs ending with ``Qed`` or ``Admitted``), output a ``.vos`` files + instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files + when interpreting ``Require`` commands. +:-vok: Indicate |Coq| to check a file completely, to load ``.vos`` files instead + of ``.vo`` files when interpreting ``Require`` commands, and to output an empty + ``.vok`` files upon success instead of writing a ``.vo`` file. :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or categories (see Section :ref:`controlling-display`). @@ -245,6 +252,119 @@ and ``coqtop``, unless stated otherwise: currently associated color and exit. :-h, --help: Print a short usage and exit. + + +Compiled interfaces (produced using ``-vos``) +---------------------------------------------- + +Compiled interfaces help saving time while developing Coq formalizations, +by compiling the formal statements exported by a library independently of +the proofs that it contains. + + .. warning:: + + Compiled interfaces should only be used for development purposes. + At the end of the day, one still needs to proof check all files + by producing standard ``.vo`` files. (Technically, when using ``-vos``, + fewer universe constraints are collected.) + Moreover, this feature is still experimental, it may be subject to + change without prior notice. + +**Principle.** + +The compilation using ``coqc -vos foo.v`` produces a file called ``foo.vos``, +which is similar to ``foo.vo`` except that all opaque proofs are skipped in +the compilation process. + +The compilation using ``coqc -vok foo.v`` checks that the file ``foo.v`` +correctly compiles, including all its opaque proofs. If the compilation +succeeds, then the output is a file called ``foo.vok``, with empty contents. +This file is only a placeholder indicating that ``foo.v`` has been successfully +compiled. (This placeholder is useful for build systems such as ``make``.) + +When compiling a file ``bar.v`` that depends on ``foo.v`` (for example via +a ``Require Foo.`` command), if the compilation command is ``coqc -vos bar.v`` +or ``coqc -vok bar.v``, then the file ``foo.vos`` gets loaded (instead of +``foo.vo``). A special case is if file ``foo.vos`` exists and has empty +contents, and ``foo.vo`` exists, then ``foo.vo`` is loaded. + +Appart from the aforementioned case where ``foo.vo`` can be loaded in place +of ``foo.vos``, in general the ``.vos`` and ``.vok`` files live totally +independently from the ``.vo`` files. + +**Dependencies generated by ``coq_makefile``.** + +The files ``foo.vos`` and ``foo.vok`` both depend on ``foo.v``. + +Furthermore, if a file ``foo.v`` requires ``bar.v``, then ``foo.vos`` +and ``foo.vok`` also depend on ``bar.vos``. + +Note, however, that ``foo.vok`` does not depend on ``bar.vok``. +Hence, as detailed further, parallel compilation of proofs is possible. + +In addition, ``coq_makefile`` generates for a file ``foo.v`` a target +``foo.required_vos`` which depends on the list of ``.vos`` files that +``foo.vos`` depends upon (excluding ``foo.vos`` itself). As explained +next, the purpose of this target is to be able to request the minimal +working state for editing interactively the file ``foo.v``. + +**Typical compilation of a set of file using a build system.** + +Assume a file ``foo.v`` that depends on two files ``f1.v`` and ``f2.v``. The +command ``make foo.required_vos`` will compile ``f1.v`` and ``f2.v`` using +the option ``-vos`` to skip the proofs, producing ``f1.vos`` and ``f2.vos``. +At this point, one is ready to work interactively on the file ``foo.v``, even +though it was never needed to compile the proofs involved in the files ``f1.v`` +and ``f2.v``. + +Assume a set of files ``f1.v ... fn.v`` with linear dependencies. The command +``make vos`` enables compiling the statements (i.e. excluding the proofs) in all +the files. Next, ``make -j vok`` enables compiling all the proofs in parallel. +Thus, calling ``make -j vok`` directly enables taking advantage of a maximal +amount of parallelism during the compilation of the set of files. + +Note that this comes at the cost of parsing and typechecking all definitions +twice, once for the ``.vos`` file and once for the ``.vok`` file. However, if +files contain nontrivial proofs, or if the files have many linear chains of +dependencies, or if one has many cores available, compilation should be faster +overall. + +**Need for ``Proof using``** + +When a theorem is part of a section, typechecking the statement of this theorem +might be insufficient for deducing the type of this statement as of at the end +of the section. Indeed, the proof of the theorem could make use of section +variables or section hypotheses that are not mentioned in the statement of the +theorem. + +For this reason, proofs inside section should begin with :cmd:`Proof using` +instead of :cmd:`Proof`, where after the ``using`` clause one should provide +the list of the names of the section variables that are required for the proof +but are not involved in the typechecking of the statement. Note that it is safe +to write ``Proof using.`` instead of ``Proof.`` also for proofs that are not +within a section. + +.. warn:: You should use the “Proof using [...].” syntax instead of “Proof.” to enable skipping this proof which is located inside a section. Give as argument to “Proof using” the list of section variables that are not needed to typecheck the statement but that are required by the proof. + + If |Coq| is invoked using the ``-vos`` option, whenever it finds the + command ``Proof.`` inside a section, it will compile the proof, that is, + refuse to skip it, and it will raise a warning. To disable the warning, one + may pass the flag ``-w -proof-without-using-in-section``. + +**Interaction with standard compilation** + +When compiling a file ``foo.v`` using ``coqc`` in the standard way (i.e., without +``-vos`` nor ``-vok``), an empty file ``foo.vos`` is created in addition to the +regular output file ``foo.vo``. If ``coqc`` is subsequently invoked on some other +file ``bar.v`` using option ``-vos`` or ``-vok``, and that ``bar.v`` requires +``foo.v``, if |Coq| finds an empty file ``foo.vos``, then it will load +``foo.vo`` instead of ``foo.vos``. + +The purpose of this feature is to allow users to benefit from the ``-vos`` +option even if they depend on libraries that were compiled in the traditional +manner (i.e., never compiled using the ``-vos`` option). + + Compiled libraries checker (coqchk) ---------------------------------------- diff --git a/lib/flags.ml b/lib/flags.ml index 7676665fe9..90b5f877d5 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -44,6 +44,8 @@ let with_options ol f x = let async_proofs_worker_id = ref "master" let async_proofs_is_worker () = !async_proofs_worker_id <> "master" +let load_vos_libraries = ref false + let debug = ref false let in_debugger = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 3f72cc4b91..76a78e61fc 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -35,6 +35,10 @@ val async_proofs_worker_id : string ref val async_proofs_is_worker : unit -> bool +(** Flag to indicate that .vos files should be loaded for dependencies + instead of .vo files. Used by -vos and -vok options. *) +val load_vos_libraries : bool ref + (** Debug flags *) val debug : bool ref val in_debugger : bool ref diff --git a/stm/stm.ml b/stm/stm.ml index 5c6df26cbb..c399b69a77 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2801,13 +2801,21 @@ let handle_failure (e, info) vcs = VCS.print (); Exninfo.iraise (e, info) -let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo = +let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo = let doc = finish ~doc in if List.length (VCS.branches ()) > 1 then CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); - Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects - ldir long_f_dot_vo - (Global.opaque_tables ()); + (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers, + below, [snapshot] gets computed even if [create_vos] is true. *) + let (tasks,counters) = dump_snapshot() in + let except = List.fold_left (fun e (r,_) -> + Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty tasks in + let todo_proofs = + if create_vos + then Library.ProofsTodoSomeEmpty except + else Library.ProofsTodoSome (except,tasks,counters) + in + Library.save_library_to todo_proofs ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ()); doc let reset_task_queue = Slaves.reset_task_queue diff --git a/stm/stm.mli b/stm/stm.mli index 29e4b02e3f..841adcf05b 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -159,8 +159,10 @@ val join : doc:doc -> doc - if the worker pool 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 failure) *) -val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc + of the completed tasks is a failure). + Note: the create_vos argument is used in the "-vos" mode, where the + proof tasks are not dumped into the output file. *) +val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc (* Empties the task queue, can be used only if the worker pool is empty (E.g. * after having built a .vio in batch mode *) diff --git a/test-suite/Makefile b/test-suite/Makefile index c60f39231e..d9c89d7a8a 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -131,9 +131,10 @@ bugs: $(BUGS) clean: rm -f trace .nia.cache .lia.cache output/MExtraction.out + rm -f vos/Makefile vos/Makefile.conf $(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>' $(HIDE)find . \( \ - -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \ + -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.log' -o -name '*.glob' \ \) -exec rm -f {} + $(SHOW) 'RM <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>' $(HIDE)find unit-tests \( \ @@ -748,3 +749,23 @@ tools/%.log : tools/%/run.sh $(FAIL); \ fi; \ ) > "$@" + +# vos/ + +vos: vos/run.log + +vos/run.log: $(wildcard vos/*.sh) $(wildcard vos/*.v) + @echo "TEST vos" + $(HIDE)(\ + export COQBIN=$(BIN);\ + cd vos && \ + bash run.sh 2>&1; \ + if [ $$? = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error!"; \ + $(FAIL); \ + fi; \ + ) > "$@" diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index 88237815b1..0d9b9ea867 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -28,10 +28,12 @@ sort -u > desired <<EOT ./test/test.glob ./test/test.v ./test/test.vo +./test/test.vos ./test/sub ./test/sub/testsub.glob ./test/sub/testsub.v ./test/sub/testsub.vo +./test/sub/testsub.vos ./test/mlihtml ./test/mlihtml/index_exceptions.html ./test/mlihtml/index.html diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index 5811dd17e4..852ac372f4 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -26,10 +26,12 @@ sort -u > desired <<EOT ./test/test.glob ./test/test.v ./test/test.vo +./test/test.vos ./test/sub ./test/sub/testsub.glob ./test/sub/testsub.v ./test/sub/testsub.vo +./test/sub/testsub.vos ./test/mlihtml ./test/mlihtml/index_exceptions.html ./test/mlihtml/index.html diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index bbd2fc460c..1303aa90b6 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -19,5 +19,6 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos EOT exec diff -u desired actual diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index bbd2fc460c..1303aa90b6 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -19,5 +19,6 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos EOT exec diff -u desired actual diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index 45bf1481df..3a5425c8bf 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -29,10 +29,12 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos ./test2 ./test2/test.glob ./test2/test.v ./test2/test.vo +./test2/test.vos ./orphan_test_test2_test ./orphan_test_test2_test/html ./orphan_test_test2_test/html/coqdoc.css diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 8f9ab9a711..588de82613 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -22,6 +22,7 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos ./test/.coq-native ./test/.coq-native/Ntest_test.cmi ./test/.coq-native/Ntest_test.cmx diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index 1e2bd979b3..cd47187582 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -22,5 +22,6 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos EOT exec diff -u desired actual diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index 1e2bd979b3..cd47187582 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -22,5 +22,6 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos EOT exec diff -u desired actual diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index 1e2bd979b3..cd47187582 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -22,5 +22,6 @@ sort > desired <<EOT ./test/test_plugin.cmxs ./test/test.v ./test/test.vo +./test/test.vos EOT exec diff -u desired actual diff --git a/test-suite/misc/deps/deps.out b/test-suite/misc/deps/deps.out index 5b79349fc2..d0263b8935 100644 --- a/test-suite/misc/deps/deps.out +++ b/test-suite/misc/deps/deps.out @@ -1 +1 @@ -misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo +misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified misc/deps/client/bar.required_vo: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo diff --git a/test-suite/vos/A.v b/test-suite/vos/A.v new file mode 100644 index 0000000000..11245ba015 --- /dev/null +++ b/test-suite/vos/A.v @@ -0,0 +1,4 @@ +Definition x := 3. + +Lemma xeq : x = x. +Proof. auto. Qed. diff --git a/test-suite/vos/B.v b/test-suite/vos/B.v new file mode 100644 index 0000000000..735fefd745 --- /dev/null +++ b/test-suite/vos/B.v @@ -0,0 +1,34 @@ +Require Import A. + +Definition y := x. + +Lemma yeq : y = y. +Proof. pose xeq. auto. Qed. + + +Section Foo. + +Variable (HFalse : False). + +Lemma yeq' : y = y. +Proof using HFalse. elimtype False. apply HFalse. Qed. + +End Foo. + +Module Type E. End E. + +Module M. + Lemma x : True. + Proof. trivial. Qed. +End M. + + +Module Type T. + Lemma x : True. + Proof. trivial. Qed. +End T. + +Module F(X:E). + Lemma x : True. + Proof. trivial. Qed. +End F. diff --git a/test-suite/vos/C.v b/test-suite/vos/C.v new file mode 100644 index 0000000000..5260b7cdaf --- /dev/null +++ b/test-suite/vos/C.v @@ -0,0 +1,13 @@ +Require Import A B. + +Definition z := x + y. + +Lemma zeq : z = z. +Proof. pose xeq. pose yeq. auto. Qed. + +Lemma yeq'' : y = y. +Proof. apply yeq'. Admitted. + +Module M. Include B.M. End M. +Module T. Include B.T. End T. +Module F. Include B.F. End F. diff --git a/test-suite/vos/run.sh b/test-suite/vos/run.sh new file mode 100755 index 0000000000..2496fc8602 --- /dev/null +++ b/test-suite/vos/run.sh @@ -0,0 +1,23 @@ +#!/bin/bash +set -e +set -o pipefail +export PATH="$COQBIN:$PATH" + +# Clean +rm -f *.vo *.vos *.vok *.glob *.aux Makefile + +# Test building all vos, then all vok +coq_makefile -R . TEST -o Makefile *.v +make vos +make vok + +# Cleanup +make clean + +# Test using compilation in custom order +set -x #echo on +coqc A.v +coqc -vos B.v +coqc -vos C.v +coqc -vok B.v +coqc -vok C.v diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 626ac0fe67..abfbd66e28 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -246,8 +246,10 @@ strip_dotslash = $(patsubst ./%,%,$(1)) with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) VO = vo +VOS = vos VOFILES = $(VFILES:.v=.$(VO)) +VOSFILES = $(VFILES:.v=.$(VOS)) GLOBFILES = $(VFILES:.v=.glob) HTMLFILES = $(VFILES:.v=.html) GHTMLFILES = $(VFILES:.v=.g.html) @@ -298,6 +300,7 @@ ALLNATIVEFILES = \ NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) FILESTOINSTALL = \ $(VOFILES) \ + $(VOSFILES) \ $(VFILES) \ $(GLOBFILES) \ $(NATIVEFILES) \ @@ -408,6 +411,12 @@ checkproofs: -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) .PHONY: checkproofs +vos: $(VOFILES:%.vo=%.vos) +.PHONY: vos + +vok: $(VOFILES:%.vo=%.vok) +.PHONY: vok + validate: $(VOFILES) $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^ .PHONY: validate @@ -558,6 +567,8 @@ clean:: $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) $(HIDE)rm -f $(VOFILES:.vo=.vio) + $(HIDE)rm -f $(VOFILES:.vo=.vos) + $(HIDE)rm -f $(VOFILES:.vo=.vok) $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex $(HIDE)rm -f $(VFILES:.v=.glob) @@ -666,6 +677,14 @@ $(VFILES:.v=.vio): %.vio: %.v $(SHOW)COQC -quick $< $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< +$(VFILES:.v=.vos): %.vos: %.v + $(SHOW)COQC -vos $< + $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vok): %.vok: %.v + $(SHOW)COQC -vok $< + $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing $(SHOW)PYTHON TIMING-DIFF $< $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index ab180769b6..f62947ec67 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -170,6 +170,7 @@ let pp_rule fmt targets deps action = let gen_coqc_targets vo = [ vo.target ; replace_ext ~file:vo.target ~newext:".glob" + ; replace_ext ~file:vo.target ~newext:".vos" ; "." ^ replace_ext ~file:vo.target ~newext:".aux"] (* Generate the dune rule: *) diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 8beb314046..ddedec12f8 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -235,15 +235,15 @@ let file_name s = function let depend_ML str = match search_mli_known str, search_ml_known str with | Some mlidir, Some mldir -> - let mlifile = file_name str mlidir - and mlfile = file_name str mldir in - (" "^mlifile^".cmi"," "^mlfile^".cmx") + let mlifile = file_name str mlidir + and mlfile = file_name str mldir in + (" "^mlifile^".cmi"," "^mlfile^".cmx") | None, Some mldir -> - let mlfile = file_name str mldir in - (" "^mlfile^".cmo"," "^mlfile^".cmx") + let mlfile = file_name str mldir in + (" "^mlfile^".cmo"," "^mlfile^".cmx") | Some mlidir, None -> - let mlifile = file_name str mlidir in - (" "^mlifile^".cmi"," "^mlifile^".cmi") + let mlifile = file_name str mlidir in + (" "^mlifile^".cmi"," "^mlifile^".cmi") | None, None -> "", "" let soustraite_fichier_ML dep md ext = @@ -254,9 +254,9 @@ let soustraite_fichier_ML dep md ext = let a_faire_opt = ref "" in List.iter (fun str -> - let byte,opt = depend_ML str in - a_faire := !a_faire ^ byte; - a_faire_opt := !a_faire_opt ^ opt) + let byte,opt = depend_ML str in + a_faire := !a_faire ^ byte; + a_faire_opt := !a_faire_opt ^ opt) (List.rev list); (!a_faire, !a_faire_opt) with @@ -274,15 +274,15 @@ let autotraite_fichier_ML md ext = let a_faire_opt = ref "" in begin try while true do - let (Use_module str) = caml_action buf in - if StrSet.mem str !deja_vu then - () - else begin - deja_vu := StrSet.add str !deja_vu; - let byte,opt = depend_ML str in - a_faire := !a_faire ^ byte; - a_faire_opt := !a_faire_opt ^ opt - end + let (Use_module str) = caml_action buf in + if StrSet.mem str !deja_vu then + () + else begin + deja_vu := StrSet.add str !deja_vu; + let byte,opt = depend_ML str in + a_faire := !a_faire ^ byte; + a_faire_opt := !a_faire_opt ^ opt + end done with Fin_fichier -> () end; @@ -301,14 +301,14 @@ let traite_fichier_modules md ext = let list = mllib_list (Lexing.from_channel chan) in List.fold_left (fun a_faire str -> match search_mlpack_known str with - | Some mldir -> - let file = file_name str mldir in + | Some mldir -> + let file = file_name str mldir in a_faire @ [file] - | None -> - match search_ml_known str with - | Some mldir -> - let file = file_name str mldir in - a_faire @ [file] + | None -> + match search_ml_known str with + | Some mldir -> + let file = file_name str mldir in + a_faire @ [file] | None -> a_faire) [] list with | Sys_error _ -> [] @@ -329,16 +329,16 @@ let escape = let c = s.[i] in if c = ' ' || c = '#' || c = ':' (* separators and comments *) || c = '%' (* pattern *) - || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *) - || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || - 'A' <= s.[1] && s.[1] <= 'Z' || - 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) + || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *) + || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || + 'A' <= s.[1] && s.[1] <= 'Z' || + 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) then begin - let j = ref (i-1) in - while !j >= 0 && s.[!j] = '\\' do - Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *) - done; - Buffer.add_char s' '\\'; + let j = ref (i-1) in + while !j >= 0 && s.[!j] = '\\' do + Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *) + done; + Buffer.add_char s' '\\'; end; if c = '$' then Buffer.add_char s' '$'; Buffer.add_char s' c @@ -362,75 +362,116 @@ end module VCache = Set.Make(VData) -let rec traite_fichier_Coq suffixe verbose f = +(** To avoid reading .v files several times for computing dependencies, + once for .vo, once for .vio, and once for .vos extensions, the + following code performs a single pass and produces a structured + list of dependencies, separating dependencies on compiled Coq files + (those loaded by [Require]) from other dependencies, e.g. dependencies + on ".v" files (for [Load]) or ".cmx", ".cmo", etc... (for [Declare]). *) + +type dependency = + | DepRequire of string (* one basename, to which we later append .vo or .vio or .vos *) + | DepOther of string (* filenames of dependencies, separated by spaces *) + +let string_of_dependency_list suffix_for_require deps = + let string_of_dep = function + | DepRequire basename -> basename ^ suffix_for_require + | DepOther s -> s + in + String.concat " " (List.map string_of_dep deps) + +let rec find_dependencies basename = + let verbose = true in (* for past/future use? *) try + (* Visited marks *) + let visited_ml = ref StrSet.empty in + let visited_v = ref VCache.empty in + let should_visit_v_and_mark from str = + if not (VCache.mem (from, str) !visited_v) then begin + visited_v := VCache.add (from, str) !visited_v; + true + end else false + in + (* Output: dependencies found *) + let dependencies = ref [] in + let add_dep dep = + dependencies := dep::!dependencies in + let add_dep_other s = + add_dep (DepOther s) in + + (* Reading file contents *) + let f = basename ^ ".v" in let chan = open_in f in let buf = Lexing.from_channel chan in - let deja_vu_v = ref VCache.empty in - let deja_vu_ml = ref StrSet.empty in try while true do - let tok = coq_action buf in - match tok with - | Require (from, strl) -> - List.iter (fun str -> - if not (VCache.mem (from, str) !deja_vu_v) then begin - deja_vu_v := VCache.add (from, str) !deja_vu_v; - try - let file_str = safe_assoc from verbose f str in - printf " %s%s" (canonize file_str) suffixe - with Not_found -> - if verbose && not (is_in_coqlib ?from str) then - let str = - match from with - | None -> str - | Some pth -> pth @ str - in - warning_module_notfound f str - end) strl - | Declare sl -> - let declare suff dir s = - let base = escape (file_name s dir) in - match !option_dynlink with - | No -> () - | Byte -> printf " %s%s" base suff - | Opt -> printf " %s.cmxs" base - | Both -> printf " %s%s %s.cmxs" base suff base - | Variable -> - printf " %s%s" base - (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)") + let tok = coq_action buf in + match tok with + | Require (from, strl) -> + List.iter (fun str -> + if should_visit_v_and_mark from str then begin + try + let file_str = safe_assoc from verbose f str in + add_dep (DepRequire (canonize file_str)) + with Not_found -> + if verbose && not (is_in_coqlib ?from str) then + let str = + match from with + | None -> str + | Some pth -> pth @ str + in + warning_module_notfound f str + end) strl + | Declare sl -> + let declare suff dir s = + let base = escape (file_name s dir) in + match !option_dynlink with + | No -> () + | Byte -> add_dep_other (sprintf "%s%s" base suff) + | Opt -> add_dep_other (sprintf "%s.cmxs" base) + | Both -> add_dep_other (sprintf "%s%s" base suff); + add_dep_other (sprintf "%s.cmxs" base) + | Variable -> add_dep_other (sprintf "%s%s" base + (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)")) in - let decl str = - let s = basename_noext str in - if not (StrSet.mem s !deja_vu_ml) then begin - deja_vu_ml := StrSet.add s !deja_vu_ml; - match search_mllib_known s with - | Some mldir -> declare ".cma" mldir s - | None -> - match search_mlpack_known s with - | Some mldir -> declare ".cmo" mldir s - | None -> - match search_ml_known s with - | Some mldir -> declare ".cmo" mldir s - | None -> warning_declare f str - end - in List.iter decl sl - | Load str -> - let str = Filename.basename str in - if not (VCache.mem (None, [str]) !deja_vu_v) then begin - deja_vu_v := VCache.add (None, [str]) !deja_vu_v; - try - let (file_str, _) = Hashtbl.find vKnown [str] in - let canon = canonize file_str in - printf " %s.v" canon; - traite_fichier_Coq suffixe true (canon ^ ".v") - with Not_found -> () - end - | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) () - done - with Fin_fichier -> close_in chan - | Syntax_error (i,j) -> close_in chan; error_cannot_parse f (i,j) - with Sys_error _ -> () + let decl str = + let s = basename_noext str in + if not (StrSet.mem s !visited_ml) then begin + visited_ml := StrSet.add s !visited_ml; + match search_mllib_known s with + | Some mldir -> declare ".cma" mldir s + | None -> + match search_mlpack_known s with + | Some mldir -> declare ".cmo" mldir s + | None -> + match search_ml_known s with + | Some mldir -> declare ".cmo" mldir s + | None -> warning_declare f str + end + in + List.iter decl sl + | Load str -> + let str = Filename.basename str in + if should_visit_v_and_mark None [str] then begin + try + let (file_str, _) = Hashtbl.find vKnown [str] in + let canon = canonize file_str in + add_dep_other (sprintf "%s.v" canon); + let deps = find_dependencies canon in + List.iter add_dep deps + with Not_found -> () + end + | AddLoadPath _ | AddRecLoadPath _ -> (* TODO: will this be handled? *) () + done; + List.rev !dependencies + with + | Fin_fichier -> + close_in chan; + List.rev !dependencies + | Syntax_error (i,j) -> + close_in chan; + error_cannot_parse f (i,j) + with Sys_error _ -> [] (* TODO: report an error? *) let mL_dependencies () = @@ -439,8 +480,8 @@ let mL_dependencies () = let fullname = file_name name dirname in let (dep,dep_opt) = traite_fichier_ML fullname ext in let intf = match search_mli_known name with - | None -> "" - | Some mldir -> " "^(file_name name mldir)^".cmi" + | None -> "" + | Some mldir -> " "^(file_name name mldir)^".cmi" in let efullname = escape fullname in printf "%s.cmo:%s%s\n" efullname dep intf; @@ -481,12 +522,14 @@ let coq_dependencies () = (fun (name,_) -> let ename = escape name in let glob = if !option_noglob then "" else " "^ename^".glob" in - 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.vio: %s.v" ename ename; - traite_fichier_Coq ".vio" true (name ^ ".v"); - printf "\n%!") + let deps = find_dependencies name in + printf "%s%s%s %s.v.beautified %s.required_vo: %s.v %s\n" ename !suffixe glob ename ename ename + (string_of_dependency_list !suffixe deps); + printf "%s.vio: %s.v %s\n" ename ename + (string_of_dependency_list ".vio" deps); + printf "%s.vos %s.vok %s.required_vos: %s.v %s\n" ename ename ename ename + (string_of_dependency_list ".vos" deps); + printf "%!") (List.rev !vAccu) let rec suffixes = function @@ -505,26 +548,26 @@ let add_caml_known phys_dir _ f = | _ -> () let add_coqlib_known recur phys_dir log_dir f = - match get_extension f [".vo"; ".vio"] with - | (basename, (".vo" | ".vio")) -> + match get_extension f [".vo"; ".vio"; ".vos"] with + | (basename, (".vo" | ".vio" | ".vos")) -> let name = log_dir@[basename] in let paths = if recur then suffixes name else [name] in List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () let add_known recur phys_dir log_dir f = - match get_extension f [".v"; ".vo"; ".vio"] with + match get_extension f [".v"; ".vo"; ".vio"; ".vos"] with | (basename,".v") -> - let name = log_dir@[basename] in - let file = phys_dir//basename in - let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in - if recur then + let name = log_dir@[basename] in + let file = phys_dir//basename in + let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in + if recur then let paths = List.tl (suffixes name) in let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in List.iter iter paths - | (basename, (".vo" | ".vio")) when not(!option_boot) -> + | (basename, (".vo" | ".vio" | ".vos")) when not(!option_boot) -> let name = log_dir@[basename] in - let paths = if recur then suffixes name else [name] in + let paths = if recur then suffixes name else [name] in List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () @@ -576,12 +619,12 @@ let rec treat_file old_dirname old_name = let complete_name = file_name name dirname in match try (stat complete_name).st_kind with _ -> S_BLK with | S_DIR -> - (if name.[0] <> '.' then + (if name.[0] <> '.' then let newdirname = match dirname with | None -> name | Some d -> d//name - in + in Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name)) | S_REG -> (match get_extension name [".v";".ml";".mli";".mlg";".mllib";".mlpack"] with diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 3600658e23..3cbbf3d186 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -88,6 +88,10 @@ let ensure_exists_with_prefix f_in f_out src_suffix tgt_suffix = | Some f -> ensure tgt_suffix long_f_dot_src f in long_f_dot_src, long_f_dot_tgt +let create_empty_file filename = + let f = open_out filename in + close_out f + (* Compile a vernac file *) let compile opts copts ~echo ~f_in ~f_out = let open Vernac.State in @@ -106,43 +110,53 @@ let compile opts copts ~echo ~f_in ~f_out = let output_native_objects = match opts.config.native_compiler with | NativeOff -> false | NativeOn {ondemand} -> not ondemand in - match copts.compilation_mode with - | BuildVo -> - let long_f_dot_v, long_f_dot_vo = - ensure_exists_with_prefix f_in f_out ".v" ".vo" in - + let mode = copts.compilation_mode in + let ext_in, ext_out = + match mode with + | BuildVo -> ".v", ".vo" + | BuildVio -> ".v", ".vio" + | Vio2Vo -> ".vio", ".vo" + | BuildVos -> ".v", ".vos" + | BuildVok -> ".v", ".vok" + in + let long_f_dot_in, long_f_dot_out = + ensure_exists_with_prefix f_in f_out ext_in ext_out in + match mode with + | BuildVo | BuildVok -> let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc - Stm.{ doc_type = VoDoc long_f_dot_vo; + Stm.{ doc_type = VoDoc long_f_dot_out; iload_path; require_libs; stm_options; } in let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file - ~aux_file:(aux_file_name_for long_f_dot_vo) - ~v_file:long_f_dot_v); + ~aux_file:(aux_file_name_for long_f_dot_out) + ~v_file:long_f_dot_in); Dumpglob.set_glob_output copts.glob_out; - Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; + Dumpglob.start_dump_glob ~vfile:long_f_dot_in ~vofile:long_f_dot_out; 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 + let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_in in let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); - Library.save_library_to ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ()); + if mode <> BuildVok (* Don't output proofs in -vok mode *) + then Library.save_library_to ~output_native_objects Library.ProofsTodoNone ldir long_f_dot_out (Global.opaque_tables ()); Aux_file.record_in_aux_at "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); + (* Produce an empty .vos file when producing a .vo in standard mode *) + if mode = BuildVo then create_empty_file (long_f_dot_out ^ "s"); + (* Produce an empty .vok file when in -vok mode *) + if mode = BuildVok then create_empty_file (long_f_dot_out); Dumpglob.end_dump_glob () - | BuildVio -> - let long_f_dot_v, long_f_dot_vio = - ensure_exists_with_prefix f_in f_out ".v" ".vio" in - + | BuildVio | BuildVos -> (* We need to disable error resiliency, otherwise some errors will be ignored in batch mode. c.f. #6707 @@ -158,26 +172,26 @@ let compile opts copts ~echo ~f_in ~f_out = let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc - Stm.{ doc_type = VioDoc long_f_dot_vio; + Stm.{ doc_type = VioDoc long_f_dot_out; iload_path; require_libs; stm_options; } in let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in - let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in + let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_in in let doc = Stm.finish ~doc:state.doc in check_pending_proofs (); - let () = ignore (Stm.snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vio) in + let create_vos = (mode = BuildVos) in + let () = ignore (Stm.snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_out) in Stm.reset_task_queue () | Vio2Vo -> - 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 = - Library.load_library_todo long_f_dot_vio in - let univs, proofs = Stm.finish_tasks long_f_dot_vo univs proofs tasks in - Library.save_library_raw long_f_dot_vo sum lib univs proofs + Library.load_library_todo long_f_dot_in in + let univs, proofs = Stm.finish_tasks long_f_dot_out univs proofs tasks in + Library.save_library_raw long_f_dot_out sum lib univs proofs let compile opts copts ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 98206fb341..178aa362c0 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -30,6 +30,9 @@ coqc specific options:\ \n into fi.vo\ \n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ \n proofs in each fi.vio\ +\n -vos process statements but ignore opaque proofs, and produce a .vos file\ +\n -vok process the file by loading .vos instead of .vo files for\ +\n dependencies, and produce an empty .vok file on success\ \n\ \nUndocumented:\ \n -vio2vo [see manual]\ diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index c4e3571281..e614d4fe6d 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type compilation_mode = BuildVo | BuildVio | Vio2Vo +type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok type t = { compilation_mode : compilation_mode @@ -166,6 +166,13 @@ let parse arglist : t = { oval with compilation_output_name = Some (next ()) } | "-quick" -> set_compilation_mode oval BuildVio + |"-vos" -> + Flags.load_vos_libraries := true; + { oval with compilation_mode = BuildVos } + |"-vok" -> + Flags.load_vos_libraries := true; + { oval with compilation_mode = BuildVok } + | "-check-vio-tasks" -> let tno = get_task_list (next ()) in let tfile = next () in diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli index 13bea3bf3e..677a3f2e48 100644 --- a/toplevel/coqcargs.mli +++ b/toplevel/coqcargs.mli @@ -8,7 +8,21 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type compilation_mode = BuildVo | BuildVio | Vio2Vo +(** Compilation modes: + - BuildVo : process statements and proofs (standard compilation), + and also output an empty .vos file + - BuildVio : process statements, delay proofs in futures + - Vio2Vo : load delayed proofs and process them + - BuildVos : process statements, and discard proofs, + and load .vos files for required libraries + - BuildVok : like BuildVo, but load .vos files for required libraries + + When loading the .vos version of a required library, if the file exists but is + empty, then we attempt to load the .vo version of that library. + This trick is useful to avoid the need for the user to compile .vos version + when an up to date .vo version is already available. +*) +type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok type t = { compilation_mode : compilation_mode diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index eded9f4bcd..309f5b657a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -271,6 +271,8 @@ let init_document opts = state before we take the first snapshot. This was not guaranteed in the past, but now is thanks to the STM API. *) + (* Next line allows loading .vos files when in interactive mode *) + Flags.load_vos_libraries := true; let iload_path = build_load_path opts in let require_libs = require_libs opts in let stm_options = opts.config.stm_flags in diff --git a/vernac/library.ml b/vernac/library.ml index 8125c3de35..244424de6b 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -430,23 +430,33 @@ let error_recursively_dependent_library dir = (* Security weakness: file might have been changed on disk between writing the content and computing the checksum... *) -let save_library_to ?todo ~output_native_objects dir f otab = - let except = match todo with - | None -> - (* XXX *) - (* assert(!Flags.compilation_mode = Flags.BuildVo); *) - assert(Filename.check_suffix f ".vo"); - Future.UUIDSet.empty - | Some (l,_) -> - assert(Filename.check_suffix f ".vio"); - List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) - Future.UUIDSet.empty l in +type ('document,'counters) todo_proofs = + | ProofsTodoNone (* for .vo *) + | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + +let save_library_to todo_proofs ~output_native_objects dir f otab = + assert( + let expected_extension = match todo_proofs with + | ProofsTodoNone -> ".vo" + | ProofsTodoSomeEmpty _ -> ".vos" + | ProofsTodoSome _ -> ".vio" + in + Filename.check_suffix f expected_extension); + let except = match todo_proofs with + | ProofsTodoNone -> Future.UUIDSet.empty + | ProofsTodoSomeEmpty except -> except + | ProofsTodoSome (except,l,_) -> except + in let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in let opaque_table, f2t_map = Opaqueproof.dump ~except otab in let tasks, utab = - match todo with - | None -> None, None - | Some (tasks, rcbackup) -> + match todo_proofs with + | ProofsTodoNone -> None, None + | ProofsTodoSomeEmpty _except -> + None, + Some (Univ.ContextSet.empty,false) + | ProofsTodoSome (_except, tasks, rcbackup) -> let tasks = List.map Stateid.(fun (r,b) -> try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b diff --git a/vernac/library.mli b/vernac/library.mli index 6a32413248..ec485e6408 100644 --- a/vernac/library.mli +++ b/vernac/library.mli @@ -36,10 +36,18 @@ type seg_univ = (* all_cst, finished? *) Univ.ContextSet.t * bool type seg_proofs = Opaqueproof.opaque_proofterm array -(** End the compilation of a library and save it to a ".vo" file. +(** End the compilation of a library and save it to a ".vo" file, + a ".vio" file, or a ".vos" file, depending on the todo_proofs + argument. [output_native_objects]: when producing vo objects, also compile the native-code version. *) + +type ('document,'counters) todo_proofs = + | ProofsTodoNone (* for .vo *) + | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + val save_library_to : - ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> + ('document,'counters) todo_proofs -> output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index bea0c943c3..b3dc254a63 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -138,6 +138,18 @@ let select_vo_file ~warn loadpath base = System.where_in_path ~warn loadpath name in Some (lpath, file) with Not_found -> None in + if !Flags.load_vos_libraries then begin + (* If the .vos file exists and is not empty, it describes the library. + If the .vos file exists and is empty, then load the .vo file. + If the .vos file is missing, then fail. *) + match find ".vos" with + | None -> Error LibNotFound + | Some (_, vos as resvos) -> + if (Unix.stat vos).Unix.st_size > 0 then Ok resvos else + match find ".vo" with + | None -> Error LibNotFound + | Some resvo -> Ok resvo + end else match find ".vo", find ".vio" with | None, None -> Error LibNotFound @@ -189,8 +201,10 @@ let error_unmapped_dir qid = ]) let error_lib_not_found qid = + let vos = !Flags.load_vos_libraries in + let vos_msg = if vos then [Pp.str " (while searching for a .vos file)"] else [] in CErrors.user_err ~hdr:"load_absolute_library_from" - Pp.(seq [ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"]) + Pp.(seq ([ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"]@vos_msg)) let try_locate_absolute_library dir = match locate_absolute_library dir with diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index edff80af00..ade291918e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -406,8 +406,10 @@ let err_notfound_library ?from qid = | Some from -> str " with prefix " ++ DirPath.print from ++ str "." in + let bonus = + if !Flags.load_vos_libraries then " (While searching for a .vos file.)" else "" in user_err ?loc:qid.CAst.loc ~hdr:"locate_library" - (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) + (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix ++ str bonus) let print_located_library qid = let open Loadpath in @@ -830,7 +832,7 @@ let vernac_scheme l = Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid; match s with | InductionScheme (_, r, _) - | CaseScheme (_, r, _) + | CaseScheme (_, r, _) | EqualityScheme r -> dump_global r) l; Indschemes.do_scheme l |