branch: elpa/proof-general
commit eb978573c372913a7465817ce00a9fdf2871648f
Merge: 32b15ff ce0f2f3
Author: Erik Martin-Dorel <e...@martin-dorel.org>
Commit: GitHub <nore...@github.com>
Merge pull request #593 from ProofGeneral/stefan
Minor tweaks encountered while trying to run the CI tests
---
.github/workflows/test.yml | 4 ++--
.gitignore | 1 +
Makefile | 32 +++++++++++++++++++++++++++-----
ci/coq-tests.el | 2 +-
4 files changed, 31 insertions(+), 8 deletions(-)
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 9874fa4..826ed74 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -73,7 +73,7 @@ jobs:
- run: emacs --version
- run: make -C doc magic
- - run: git diff --exit-code
+ - run: git diff --exit-code -- doc
test:
runs-on: ubuntu-latest
@@ -123,7 +123,7 @@ jobs:
endGroup
startGroup Run tests
sudo chown -R coq:coq ./ci
- ./ci/test.sh
+ make tests
endGroup
# - run: echo "::remove-matcher owner=ert-problem-matcher::"
diff --git a/.gitignore b/.gitignore
index 2039757..0af17ea 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,3 +5,4 @@ ChangeLog
proof-general-autoloads.el
*.elc
*~
+/ci/.lia.cache
diff --git a/Makefile b/Makefile
index 265aad6..4db14a0 100644
--- a/Makefile
+++ b/Makefile
@@ -9,6 +9,7 @@
## make scripts - edit paths to bash/perl/PGHOME in scripts
## make install - install into system directories
## make clean - return to clean source
+## make tests - run the suite of regression tests
##
## Edit the EMACS setting below or call with an explicit one, like this:
##
@@ -103,14 +104,12 @@ compile: $(EL)
@echo "****************************************************************"
##
-## compile : byte compile all lisp files
-##
-## Compiling can show up errors in the code, but be wary of fixing obsoletion
-## or argument call warnings unless they're valid for all supported Emacsen.
+## check : make sure compilation doesn't emit warnings
##
## The check target aborts compilation on any byte-compiler warning.
-## Compile with this target once before commiting your changes to
+## Compile with this target once before commiting your changes to
## the repository.
+## FIXME: Compilation currently emits many warnings :-(
##
check: $(EL)
@echo "****************************************************************"
@@ -121,6 +120,29 @@ check: $(EL)
@echo " Finished."
@echo "****************************************************************"
+##
+## tests : run a selection of regression tests
+##
+.PHONY: tests
+tests:
+ ci/test.sh
+
+##
+## dist-tests : run all regression tests
+##
+.PHONY: dist-tests
+dist-tests: tests check-doc-magic
+ +$(MAKE) -C ci/simple-tests all
+ +$(MAKE) -C ci/compile-tests test
+ +$(MAKE) -C ci/test-indent
+
+##
+## check-doc-magic : check *.texi are up-to-date w.r.t. docstrings
+##
+.PHONY: check-doc-magic
+check-doc-magic:
+ +$(MAKE) -C doc magic
+ git diff --exit-code -- doc
##
## Make an individual .elc. Building separately means we need to be
diff --git a/ci/coq-tests.el b/ci/coq-tests.el
index ff762d9..fb5635f 100644
--- a/ci/coq-tests.el
+++ b/ci/coq-tests.el
@@ -274,7 +274,7 @@ For example, COMMENT could be (*test-definition*)"
(proof-shell-wait)
(goto-char (point-min))
(insert "(*.*)")
- (should (equal (proof-queue-or-locked-end) 1)))))
+ (should (equal (proof-queue-or-locked-end) (point-min))))))
(ert-deftest 080_coq-test-regression-show-proof-stepwise()
"Regression test for the \"Show Proof\" option"
