From 72dc33fb0f99d403e8693db178a73c1e28096400 Mon Sep 17 00:00:00 2001 From: charguer Date: Thu, 8 Nov 2018 16:50:13 +0100 Subject: 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. --- test-suite/Makefile | 23 ++++++++++++++++++++++- test-suite/misc/deps/deps.out | 2 +- test-suite/vos/A.v | 4 ++++ test-suite/vos/B.v | 34 ++++++++++++++++++++++++++++++++++ test-suite/vos/C.v | 13 +++++++++++++ test-suite/vos/run.sh | 23 +++++++++++++++++++++++ 6 files changed, 97 insertions(+), 2 deletions(-) create mode 100644 test-suite/vos/A.v create mode 100644 test-suite/vos/B.v create mode 100644 test-suite/vos/C.v create mode 100755 test-suite/vos/run.sh (limited to 'test-suite') 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 -- cgit v1.2.3 From 76c72065a10381d91317c12436e3d6c1cd2e7348 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 28 Oct 2019 12:51:49 +0100 Subject: [test-suite] acknowledge coq_mafile installs .vos --- 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 + 9 files changed, 12 insertions(+) (limited to 'test-suite') 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 < desired < desired < desired < desired < desired < desired < desired < desired <