From e858b39c7025ed8ef8178dd3184232e5dfd14ca5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 5 Oct 2021 11:25:17 +0200
Subject: [PATCH] CI: automatically check validation output for unexpected
axioms
Closes #79
---
.gitlab-ci.yml | 4 +-
scripts/check-validation-output.sh | 66 ++++++++++++++++++++++++++++++
2 files changed, 69 insertions(+), 1 deletion(-)
create mode 100755 scripts/check-validation-output.sh
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0db5e979d..dd9c7d3f3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -162,7 +162,9 @@ validate:
needs: ["compile"]
dependencies:
- compile
- script: make validate
+ script:
+ - make validate 2>&1 | tee validation-results.txt
+ - scripts/check-validation-output.sh validation-results.txt
validate-classic:
extends:
diff --git a/scripts/check-validation-output.sh b/scripts/check-validation-output.sh
new file mode 100755
index 000000000..ea9df0320
--- /dev/null
+++ b/scripts/check-validation-output.sh
@@ -0,0 +1,66 @@
+#!/bin/sh
+set -e
+
+RESULTS="$1"
+
+[ -e "$RESULTS" ] || exit 2
+
+OBSERVED="/tmp/observed-validation-output"
+EXPECTED="/tmp/expected-validation-output"
+
+# strip the list of files and COQDEP output
+grep -v 'COQDEP VFILES' "$RESULTS" | grep -v '"coqchk" -silent' > "$OBSERVED"
+
+cat > $EXPECTED <<EOF
+
+CONTEXT SUMMARY
+===============
+
+* Theory: Set is predicative
+
+* Axioms: <none>
+
+* Constants/Inductives relying on type-in-type: <none>
+
+* Constants/Inductives relying on unsafe (co)fixpoints: <none>
+
+* Inductives whose positivity is assumed: <none>
+
+EOF
+
+if ! diff --brief "$OBSERVED" "$EXPECTED" > /dev/null
+then
+ echo "[!!] Validation output does not match expected output."
+ echo "[II] Trying workaround for https://github.com/coq/coq/issues/13324"
+
+ # strip the list of files, COQDEP output, and
+ # filter bogus ltac: axioms (see Coq issue 13324)
+ grep -v 'COQDEP VFILES' "$RESULTS" | grep -v '"coqchk" -silent' | grep -v "ltac_gen_subproof" > "$OBSERVED"
+ # the list of axioms should now be an empty list
+ cat > $EXPECTED <<EOF
+
+CONTEXT SUMMARY
+===============
+
+* Theory: Set is predicative
+
+* Axioms:
+
+* Constants/Inductives relying on type-in-type: <none>
+
+* Constants/Inductives relying on unsafe (co)fixpoints: <none>
+
+* Inductives whose positivity is assumed: <none>
+
+EOF
+ if ! diff --brief "$OBSERVED" "$EXPECTED" > /dev/null
+ then
+ echo "[!!] Validation output still does not match expected output."
+ diff -u "$OBSERVED" "$EXPECTED"
+ exit 3
+ fi
+fi
+
+# if we get here, we saw the expected output
+echo "[II] Validation succeeded."
+exit 0
--
GitLab