aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/practical-tools/coq-commands.rst10
-rwxr-xr-xtest-suite/coq-makefile/coqdoc1/run.sh2
-rwxr-xr-xtest-suite/coq-makefile/coqdoc2/run.sh2
-rwxr-xr-xtest-suite/coq-makefile/mlpack1/run.sh1
-rwxr-xr-xtest-suite/coq-makefile/mlpack2/run.sh1
-rwxr-xr-xtest-suite/coq-makefile/multiroot/run.sh2
-rwxr-xr-xtest-suite/coq-makefile/native1/run.sh1
-rwxr-xr-xtest-suite/coq-makefile/plugin1/run.sh1
-rwxr-xr-xtest-suite/coq-makefile/plugin2/run.sh1
-rwxr-xr-xtest-suite/coq-makefile/plugin3/run.sh1
-rw-r--r--tools/CoqMakefile.in2
-rw-r--r--toplevel/ccompile.ml7
-rw-r--r--toplevel/coqcargs.mli2
-rw-r--r--vernac/loadpath.ml8
14 files changed, 14 insertions, 27 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 97e7af8cb4..514f5acc8e 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -354,11 +354,11 @@ within a 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``.
+``-vos`` nor ``-vok``), an empty file ``foo.vos`` and an empty file ``foo.vok``
+are 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
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index 0d9b9ea867..88237815b1 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -28,12 +28,10 @@ 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 852ac372f4..5811dd17e4 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -26,12 +26,10 @@ 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 1303aa90b6..bbd2fc460c 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -19,6 +19,5 @@ 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 1303aa90b6..bbd2fc460c 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -19,6 +19,5 @@ 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 3a5425c8bf..45bf1481df 100755
--- a/test-suite/coq-makefile/multiroot/run.sh
+++ b/test-suite/coq-makefile/multiroot/run.sh
@@ -29,12 +29,10 @@ 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 588de82613..8f9ab9a711 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -22,7 +22,6 @@ 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 cd47187582..1e2bd979b3 100755
--- a/test-suite/coq-makefile/plugin1/run.sh
+++ b/test-suite/coq-makefile/plugin1/run.sh
@@ -22,6 +22,5 @@ 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 cd47187582..1e2bd979b3 100755
--- a/test-suite/coq-makefile/plugin2/run.sh
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -22,6 +22,5 @@ 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 cd47187582..1e2bd979b3 100755
--- a/test-suite/coq-makefile/plugin3/run.sh
+++ b/test-suite/coq-makefile/plugin3/run.sh
@@ -22,6 +22,5 @@ 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/tools/CoqMakefile.in b/tools/CoqMakefile.in
index fa186af13a..7c53ecfe18 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -254,7 +254,6 @@ 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)
@@ -305,7 +304,6 @@ ALLNATIVEFILES = \
NATIVEFILES = $(wildcard $(ALLNATIVEFILES))
FILESTOINSTALL = \
$(VOFILES) \
- $(VOSFILES) \
$(VFILES) \
$(GLOBFILES) \
$(NATIVEFILES) \
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 3cbbf3d186..3c198dc600 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -150,8 +150,11 @@ let compile opts copts ~echo ~f_in ~f_out =
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 .vos file and an empty .vok file when producing a .vo in standard mode *)
+ if mode = BuildVo then begin
+ create_empty_file (long_f_dot_out ^ "s");
+ create_empty_file (long_f_dot_out ^ "k");
+ end;
(* Produce an empty .vok file when in -vok mode *)
if mode = BuildVok then create_empty_file (long_f_dot_out);
Dumpglob.end_dump_glob ()
diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli
index 677a3f2e48..18c51f4229 100644
--- a/toplevel/coqcargs.mli
+++ b/toplevel/coqcargs.mli
@@ -10,7 +10,7 @@
(** Compilation modes:
- BuildVo : process statements and proofs (standard compilation),
- and also output an empty .vos file
+ and also output an empty .vos file and .vok file
- BuildVio : process statements, delay proofs in futures
- Vio2Vo : load delayed proofs and process them
- BuildVos : process statements, and discard proofs,
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index b3dc254a63..a8462e31e1 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -140,12 +140,10 @@ let select_vo_file ~warn loadpath base =
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. *)
+ Otherwise, load the .vo file, or fail if is missing. *)
match find ".vos" with
- | None -> Error LibNotFound
- | Some (_, vos as resvos) ->
- if (Unix.stat vos).Unix.st_size > 0 then Ok resvos else
+ | Some (_, vos as resvos) when (Unix.stat vos).Unix.st_size > 0 -> Ok resvos
+ | _ ->
match find ".vo" with
| None -> Error LibNotFound
| Some resvo -> Ok resvo
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:39:25 +0000