From b9f300847618dab5d58a5092d2089d90794078f4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Mon, 16 Dec 2024 17:48:36 +0100
Subject: [PATCH] CI: replace `make validate` with `Print Assumptions`
Since `coqchk` is not precise, we keep running into false positives
when packages that we (indirectly) depend on (in particular,`coq-elpi`)
load the standard library. Currently, this blocks the upgrade to Coq 8.20.
This patch disables `make validate` and instead introduces a check
that runs `Print Assumptions` for each theorem in the `prosa.results`
module, which are all the main results we care about.
---
.gitlab-ci.yml | 12 +++++++----
scripts/check-axiom-free.sh | 42 +++++++++++++++++++++++++++++++++++++
2 files changed, 50 insertions(+), 4 deletions(-)
create mode 100755 scripts/check-axiom-free.sh
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 01fba9abc..2b30bc1bc 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -102,8 +102,10 @@ compile-and-doc-and-validate:
- make -j ${NJOBS} all 2>&1 | tee coqc-messages.txt
- if grep -q Warning coqc-messages.txt; then (echo "Please fix all Coq warnings:"; echo "--"; grep -B1 Warning coqc-messages.txt; exit 1); fi
- !reference [.make-html, script]
- - make validate 2>&1 | tee validation-results.txt
- - scripts/check-validation-output.sh --accept-proof-irrelevance validation-results.txt
+ - scripts/check-axiom-free.sh results
+##### `make validate` disabled because of https://github.com/LPCIC/coq-elpi/issues/677 and https://github.com/coq/coq/issues/17345
+# - make validate 2>&1 | tee validation-results.txt
+# - scripts/check-validation-output.sh --accept-proof-irrelevance validation-results.txt
artifacts:
name: "prosa-spec-$CI_COMMIT_REF_NAME"
paths:
@@ -128,8 +130,10 @@ compile-and-validate:
- .preferred-stable-version
script:
- make -j ${NJOBS}
- - make validate 2>&1 | tee validation-results.txt
- - scripts/check-validation-output.sh validation-results.txt
+ - scripts/check-axiom-free.sh results
+##### `make validate` disabled because of https://github.com/LPCIC/coq-elpi/issues/677 and https://github.com/coq/coq/issues/17345
+# - make validate 2>&1 | tee validation-results.txt
+# - scripts/check-validation-output.sh validation-results.txt
proof-length:
stage: build
diff --git a/scripts/check-axiom-free.sh b/scripts/check-axiom-free.sh
new file mode 100755
index 000000000..78141f3d6
--- /dev/null
+++ b/scripts/check-axiom-free.sh
@@ -0,0 +1,42 @@
+#!/bin/bash
+
+function check_one_file {
+ FILE="$1"
+ MOD="${FILE//\//.}"
+ MOD="prosa.${MOD/.v/}"
+
+ THEOREMS=$(grep -E '^ *Theorem [^ ]+ *:' "$FILE" | sed -e 's/^ *Theorem//' -e 's/ *:$//')
+ for THM in $THEOREMS
+ do
+ OUTPUT=$(mktemp)
+ (
+ echo "Require ${MOD}."
+ echo "Print Assumptions ${MOD}.${THM}."
+ ) \
+ | coqtop -nois -R . prosa > "$OUTPUT" 2>&1 || exit 2
+ if grep -q "Closed under the global context" "$OUTPUT"
+ then
+ echo "OK ${MOD}.${THM}"
+ else
+ echo "FAIL ${MOD}.${THM}"
+ cat "$OUTPUT"
+ exit 1
+ fi
+ rm "$OUTPUT"
+ done
+}
+
+
+while [ -n "$1" ]
+do
+ if [ -d "$1" ]
+ then
+ for F in $(find "$1" -iname '*.v')
+ do
+ check_one_file "$F" || exit 1
+ done
+ else
+ check_one_file "$1" || exit 1
+ fi
+ shift
+done
--
GitLab