branch: elpa/proof-general
commit e2138d0b8248ef85d8fb2bc8c89a6c5f33f9f28f
Author: Pierre COURTIEU <pierre.court...@cnam.fr>
Commit: Pierre Courtieu <mata...@users.noreply.github.com>
Indentation testing CI ready (hopefully).
---
ci/test-indent/Makefile | 22 ++++++++++++++++++++++
ci/test-indent/coq-test-indent.sh | 12 +++++++++---
.../{indent_equations.v => indent-equations.v} | 0
.../{indent_monadic.v => indent-monadic.v} | 0
ci/test-indent/tests.sh | 1 +
5 files changed, 32 insertions(+), 3 deletions(-)
diff --git a/ci/test-indent/Makefile b/ci/test-indent/Makefile
new file mode 100644
index 0000000..5aa999a
--- /dev/null
+++ b/ci/test-indent/Makefile
@@ -0,0 +1,22 @@
+# This file is part of Proof General.
+#
+# © Copyright 2021 Pierre Courtieu
+#
+# Authors: Pierre Courtieu
+# Maintainer: Pierre Courtieu <pierre.court...@cnam.fr>
+#
+# License: GPL2+ (GNU GENERAL PUBLIC LICENSE)
+
+TESTS:=$(wildcard indent-*.v)
+INDENTED:=$(subst indent-,indented_indent-, $(TESTS))
+
+all: $(INDENTED)
+
+indented_%.v: %.v
+ @echo "### testing indentation of $<..."
+ @./coq-test-indent.sh $<
+
+.PHONY: clean
+
+clean:
+ rm -f indented_indent*
diff --git a/ci/test-indent/coq-test-indent.sh
b/ci/test-indent/coq-test-indent.sh
index 7204d00..2f35397 100755
--- a/ci/test-indent/coq-test-indent.sh
+++ b/ci/test-indent/coq-test-indent.sh
@@ -1,3 +1,4 @@
+#!/bin/bash
# This script should be launched from its own directory, so that file
# coq-test-indent.el is accessible.
@@ -24,14 +25,19 @@ emacs -q -batch --eval "(progn (load-file
\"coq-test-indent.el\") (launch-test \
# echo "grep \"INDENT CHANGED\" $INDENTEDTESTFILE"
# grep "INDENT CHANGED" $INDENTEDTESTFILE
echo -n " diff -q $TESTFILE $INDENTEDTESTFILE..."
-diff -q $TESTFILE $INDENTEDTESTFILE > /dev/null
-if [[ $? == 1 ]] ;
+diff -q $TESTFILE $INDENTEDTESTFILE
+if [[ "$?" == 1 ]] ;
then echo " DIFFERENCES FOUND"
+ diff -u $TESTFILE $INDENTEDTESTFILE
printf "${RED} TEST FAILURE ***${NC}\n"
- echo " *** details can be seen with:"
+ echo " *** details can be seen by reproducing the tests:"
+ echo " *** cd ci/test-indent"
+ echo " *** make"
echo " *** diff --side-by-side --suppress-common-lines $TESTFILE
$INDENTEDTESTFILE"
echo " *** or graphically: "
echo " *** meld $TESTFILE $INDENTEDTESTFILE"
+ exit 1 # Make the test program fail, so that CI knows.
else echo "NO DIFFERENCE"
printf "${GREEN} TEST SUCCESS *** ${NC}\n"
+ exit 0
fi
diff --git a/ci/test-indent/indent_equations.v
b/ci/test-indent/indent-equations.v
similarity index 100%
rename from ci/test-indent/indent_equations.v
rename to ci/test-indent/indent-equations.v
diff --git a/ci/test-indent/indent_monadic.v b/ci/test-indent/indent-monadic.v
similarity index 100%
rename from ci/test-indent/indent_monadic.v
rename to ci/test-indent/indent-monadic.v
diff --git a/ci/test-indent/tests.sh b/ci/test-indent/tests.sh
index 9dcd5c0..ef2c23e 100755
--- a/ci/test-indent/tests.sh
+++ b/ci/test-indent/tests.sh
@@ -1,3 +1,4 @@
+#!/bin/bash
