Implementing support for vos/vok files.

A .vos file stores the result of compiling statements (defs, lemmas)
but not proofs.
A .vok file is an empty file that denotes successful compilation of
the full contents of a .v file.
Unlike a .vio file, a .vos file does not store suspended proofs,
so it is more lightweight. It cannot be completed into a .vo file.

6 files changed, 97 insertions, 2 deletions

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/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