From 5bf25dfce23da1cee04b1c886e026f0dbc902c9c Mon Sep 17 00:00:00 2001
From: charguer
Date: Fri, 8 Nov 2019 11:06:10 +0100
Subject: From CoqIDE or -vos or -vok compilation, load .vo when .vos is
 missing (fixing bug #11057). With this new behavior, it is not needed to .vos
 files in user contribs. Also, this commit adds a feature: upon creation of a
 .vo file, an empty .vok file is touched.

---
 doc/sphinx/practical-tools/coq-commands.rst | 10 +++++-----
 test-suite/coq-makefile/coqdoc1/run.sh      |  2 --
 test-suite/coq-makefile/coqdoc2/run.sh      |  2 --
 test-suite/coq-makefile/mlpack1/run.sh      |  1 -
 test-suite/coq-makefile/mlpack2/run.sh      |  1 -
 test-suite/coq-makefile/multiroot/run.sh    |  2 --
 test-suite/coq-makefile/native1/run.sh      |  1 -
 test-suite/coq-makefile/plugin1/run.sh      |  1 -
 test-suite/coq-makefile/plugin2/run.sh      |  1 -
 test-suite/coq-makefile/plugin3/run.sh      |  1 -
 tools/CoqMakefile.in                        |  2 --
 toplevel/ccompile.ml                        |  7 +++++--
 toplevel/coqcargs.mli                       |  2 +-
 vernac/loadpath.ml                          |  8 +++-----
 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 70259ff565..a68078ecd4 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 abfbd66e28..23b9b0bb70 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -249,7 +249,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)
@@ -300,7 +299,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
-- 
cgit v1.2.3