include compile tests in CI elisp compilation

15 files changed, 79 insertions, 24 deletions

diff --git a/Makefile b/Makefile
index 3bc393ed..21aed373 100644
--- a/Makefile
+++ b/Makefile
@@ -33,10 +33,26 @@ EMACS=$(shell if [ -z "`which emacs`" ]; then echo "Emacs executable not found";
 PREFIX=$(DESTDIR)/usr
 DEST_PREFIX=$(DESTDIR)/usr
 
+# subdirectories for provers: to be compiled and installed
 PROVERS=acl2 ccc coq easycrypt hol-light hol98 isar lego pghaskell pgocaml pgshell phox twelf
+
+# generic lisp code: to be compiled and installed
 OTHER_ELISP=generic lib
-ELISP_DIRS=${PROVERS} ${OTHER_ELISP}
+
+# additional lisp code: to be compiled but not installed
+ADDITIONAL_ELISP:=ci/compile-tests \
+		$(wildcard ci/compile-tests/[0-9][0-9][0-9]-*)
+
+# directories with lisp code to be installed
+ELISP_DIRS_INST=${PROVERS} ${OTHER_ELISP}
+
+# directories with lisp code to be compiled (superset of ELISP_DIRS_INST
+ELISP_DIRS_COMP=${ELISP_DIRS_INST} ${ADDITIONAL_ELISP}
+
+# to be installed
 ELISP_EXTRAS=
+
+# to be installed
 EXTRA_DIRS = images
 
 DOC_FILES=AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER doc/*.pdf
@@ -54,11 +70,11 @@ BIN_SCRIPTS = lego/legotags coq/coqtags isar/isartags
 
 # Setting load path might be better in Elisp, but seems tricky to do
 # only during compilation.  Another idea: put a function in proof-site
-# to output the compile-time load path and ELISP_DIRS so these are set
+# to output the compile-time load path and ELISP_DIRS_COMP so these are set
 # just in that one place.
 ERROR_ON_WARN = nil
-BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (${ELISP_DIRS}))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn $(ERROR_ON_WARN)))' -f batch-byte-compile
-EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done)
+BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (${ELISP_DIRS_COMP}))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn $(ERROR_ON_WARN)))' -f batch-byte-compile
+EL=$(shell for f in $(ELISP_DIRS_COMP); do ls $$f/*.el; done)
 ELC=$(EL:.el=.elc)
 
 .SUFFIXES:	.el .elc
@@ -189,15 +205,15 @@ install-elisp: install-el install-elc
 # Should use install program or fix ownerships afterwards here.
 install-el:
 	mkdir -p ${ELISP}
-	for f in ${ELISP_DIRS} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done
-	for f in ${ELISP_DIRS}; do cp -pf $$f/*.el ${ELISP}/$$f; done
+	for f in ${ELISP_DIRS_INST} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done
+	for f in ${ELISP_DIRS_INST}; do cp -pf $$f/*.el ${ELISP}/$$f; done
 	for f in ${EXTRA_DIRS}; do cp -prf $$f/* ${ELISP}/$$f; done
 	for f in ${ELISP_EXTRAS}; do cp -pf $$f ${ELISP}/$$f; done
 
 install-elc: compile
 	mkdir -p ${ELISP}
-	for f in ${ELISP_DIRS} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done
-	for f in ${ELISP_DIRS}; do cp -pf $$f/*.elc ${ELISP}/$$f; done
+	for f in ${ELISP_DIRS_INST} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done
+	for f in ${ELISP_DIRS_INST}; do cp -pf $$f/*.elc ${ELISP}/$$f; done
 	for f in ${ELISP_EXTRAS}; do cp -pf $$f ${ELISP}/$$f; done
 
 install-init:
diff --git a/Makefile.devel b/Makefile.devel
index d4339a46..8705af31 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -169,7 +169,7 @@ RELEASENAMEDMG = $(RELEASENAME).dmg
 # Where to install a distribution
 DISTINSTALLDIR=/usr/local/share/elisp/proofgeneral
 
-SUBDIRS=$(ELISP_DIRS) etc doc images
+SUBDIRS=$(ELISP_DIRS_COMP) etc doc images
 
 PWD=$(shell pwd)
 
diff --git a/ci/compile-tests/001-mini-project/Makefile b/ci/compile-tests/001-mini-project/Makefile
index 4ae0a433..95f05017 100644
--- a/ci/compile-tests/001-mini-project/Makefile
+++ b/ci/compile-tests/001-mini-project/Makefile
@@ -11,8 +11,8 @@
 .PHONY: test
 test:
 	$(MAKE) clean
-	emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \
-		-l test.el -f ert-run-tests-batch-and-exit
+	emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \
+		-l runtest.el -f ert-run-tests-batch-and-exit
 
 .PHONY: clean
 clean:
diff --git a/ci/compile-tests/001-mini-project/test.el b/ci/compile-tests/001-mini-project/runtest.el
index 49cc91f7..9edbcbd5 100644
--- a/ci/compile-tests/001-mini-project/test.el
+++ b/ci/compile-tests/001-mini-project/runtest.el
@@ -25,6 +25,9 @@
 ;;       d   e   f
 
 
+;; require cct-lib for the elisp compilation, otherwise this is present already
+(require 'cct-lib)
+
 ;;; set configuration
 (cct-configure-proof-general)
 
diff --git a/ci/compile-tests/002-require-no-dependencies/Makefile b/ci/compile-tests/002-require-no-dependencies/Makefile
index 4ae0a433..95f05017 100644
--- a/ci/compile-tests/002-require-no-dependencies/Makefile
+++ b/ci/compile-tests/002-require-no-dependencies/Makefile
@@ -11,8 +11,8 @@
 .PHONY: test
 test:
 	$(MAKE) clean
-	emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \
-		-l test.el -f ert-run-tests-batch-and-exit
+	emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \
+		-l runtest.el -f ert-run-tests-batch-and-exit
 
 .PHONY: clean
 clean:
diff --git a/ci/compile-tests/002-require-no-dependencies/test.el b/ci/compile-tests/002-require-no-dependencies/runtest.el
index 69de9baa..f2feefad 100644
--- a/ci/compile-tests/002-require-no-dependencies/test.el
+++ b/ci/compile-tests/002-require-no-dependencies/runtest.el
@@ -22,6 +22,9 @@
 ;;           c
 
 
+;; require cct-lib for the elisp compilation, otherwise this is present already
+(require 'cct-lib)
+
 ;;; set configuration
 (cct-configure-proof-general)
 
diff --git a/ci/compile-tests/003-require-error/Makefile b/ci/compile-tests/003-require-error/Makefile
index 4ae0a433..95f05017 100644
--- a/ci/compile-tests/003-require-error/Makefile
+++ b/ci/compile-tests/003-require-error/Makefile
@@ -11,8 +11,8 @@
 .PHONY: test
 test:
 	$(MAKE) clean
-	emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \
-		-l test.el -f ert-run-tests-batch-and-exit
+	emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \
+		-l runtest.el -f ert-run-tests-batch-and-exit
 
 .PHONY: clean
 clean:
diff --git a/ci/compile-tests/003-require-error/test.el b/ci/compile-tests/003-require-error/runtest.el
index 0a0dd3d4..c5e2a713 100644
--- a/ci/compile-tests/003-require-error/test.el
+++ b/ci/compile-tests/003-require-error/runtest.el
@@ -25,6 +25,9 @@
 ;; and where a1, a2 and a3 are the 3 require commands in file a.v
 
 
+;; require cct-lib for the elisp compilation, otherwise this is present already
+(require 'cct-lib)
+
 ;;; set configuration
 (cct-configure-proof-general)
 
diff --git a/ci/compile-tests/004-dependency-cycle/Makefile b/ci/compile-tests/004-dependency-cycle/Makefile
index 4ae0a433..95f05017 100644
--- a/ci/compile-tests/004-dependency-cycle/Makefile
+++ b/ci/compile-tests/004-dependency-cycle/Makefile
@@ -11,8 +11,8 @@
 .PHONY: test
 test:
 	$(MAKE) clean
-	emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \
-		-l test.el -f ert-run-tests-batch-and-exit
+	emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \
+		-l runtest.el -f ert-run-tests-batch-and-exit
 
 .PHONY: clean
 clean:
diff --git a/ci/compile-tests/004-dependency-cycle/test.el b/ci/compile-tests/004-dependency-cycle/runtest.el
index 5f9f63f3..97d60fb5 100644
--- a/ci/compile-tests/004-dependency-cycle/test.el
+++ b/ci/compile-tests/004-dependency-cycle/runtest.el
@@ -25,6 +25,9 @@
 ;; where a1 and a2 are the 2 require commands in file a.v.
 
 
+;; require cct-lib for the elisp compilation, otherwise this is present already
+(require 'cct-lib)
+
 ;;; set configuration
 (cct-configure-proof-general)
 
diff --git a/ci/compile-tests/005-change-recompile/Makefile b/ci/compile-tests/005-change-recompile/Makefile
index 983227be..4cdc6503 100644
--- a/ci/compile-tests/005-change-recompile/Makefile
+++ b/ci/compile-tests/005-change-recompile/Makefile
@@ -17,8 +17,8 @@ TEST_SOURCES:=a.v b.v c.v d.v e.v f.v g.v h.v
 test:
 	$(MAKE) clean
 	$(MAKE) $(TEST_SOURCES)
-	emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \
-		-l test.el -f ert-run-tests-batch-and-exit
+	emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \
+		-l runtest.el -f ert-run-tests-batch-and-exit
 
 %.v: %.v.orig
 	cp $< $@
diff --git a/ci/compile-tests/005-change-recompile/test.el b/ci/compile-tests/005-change-recompile/runtest.el
index 4bbc4f81..c5d7f9b3 100644
--- a/ci/compile-tests/005-change-recompile/test.el
+++ b/ci/compile-tests/005-change-recompile/runtest.el
@@ -35,6 +35,9 @@
 ;;
 ;;
 
+;; require cct-lib for the elisp compilation, otherwise this is present already
+(require 'cct-lib)
+
 ;;; set configuration
 (cct-configure-proof-general)
 
diff --git a/ci/compile-tests/006-ready-dependee/Makefile b/ci/compile-tests/006-ready-dependee/Makefile
index fe014bfc..eb622301 100644
--- a/ci/compile-tests/006-ready-dependee/Makefile
+++ b/ci/compile-tests/006-ready-dependee/Makefile
@@ -17,8 +17,8 @@ TEST_SOURCES:=a.v b.v c.v d.v e.v f.v g.v h.v i.v j.v k.v
 test:
 	$(MAKE) clean
 	$(MAKE) $(TEST_SOURCES)
-	emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \
-		-l test.el -f ert-run-tests-batch-and-exit
+	emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \
+		-l runtest.el -f ert-run-tests-batch-and-exit
 
 %.v: %.v.orig
 	cp $< $@
diff --git a/ci/compile-tests/006-ready-dependee/test.el b/ci/compile-tests/006-ready-dependee/runtest.el
index 7105c6e7..9f4a2ce0 100644
--- a/ci/compile-tests/006-ready-dependee/test.el
+++ b/ci/compile-tests/006-ready-dependee/runtest.el
@@ -34,6 +34,9 @@
 ;; recompiled after k has changed.
 
 
+;; require cct-lib for the elisp compilation, otherwise this is present already
+(require 'cct-lib)
+
 ;;; set configuration
 (cct-configure-proof-general)
 
@@ -97,7 +100,6 @@ Combine all the following tests in this order:
 
 (ert-deftest cct-change-recompile ()
   "Test successful recompilation for a dependency in state ready."
-  ;; :expected-result :failed
   ;;(setq coq--debug-auto-compilation t)
   (find-file "a.v")
 
diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el
index 532cd92a..1a10fc15 100644
--- a/ci/compile-tests/cct-lib.el
+++ b/ci/compile-tests/cct-lib.el
@@ -16,6 +16,27 @@
 ;; This file contains common definitions for the automated tests of
 ;; parallel background compilation.
 
+;; Require some libraries for the elisp compilation. When compiling,
+;; nothing is loaded, but all Proof General directories are in the
+;; load path. When this file is loaded as part of a test, proof-site
+;; has been loaded but only the generic subdir is in the load path.
+;; This file references variables from coq-compile-common and
+;; functions from proof-shell, therefore coq-compile-common must be
+;; required for compilation. When running a test, these files would be
+;; loaded anyway when the test visits the first Coq file. For
+;; executing tests, the coq subdir will only be added to the load path
+;; when the first Coq file is visited. Therefore we have to add it
+;; here via proof-ready-for-assistant. For compilation, we have to
+;; require proof-site, otherwise proof-ready-for-assistant won't be
+;; defined.
+(require 'proof-site)
+(proof-ready-for-assistant 'coq)
+(require 'coq-compile-common)
+(require 'ert)
+
+;; needed for seq-set-equal-p
+(require 'seq)
+
 
 (defmacro cct-implies (p q)
   "Short-circuit logical implication.
@@ -97,8 +118,7 @@ reports a test failure if there is none or more than one vanilla spans."
   "Extract the last line from the *Messages* buffer.
 Useful if the message is not present in the echo area any more
 and `current-message' does not return anything."
-  (save-excursion
-    (set-buffer "*Messages*")
+  (with-current-buffer "*Messages*"
     (goto-char (point-max))
     (forward-line -1)
     (buffer-substring (point) (- (point-max) 1))))
@@ -193,3 +213,5 @@ or changed since recording the time in the association."
         proof-three-window-enable nil
         coq-compile-auto-save 'save-coq
         coq--debug-auto-compilation nil))
+
+(provide 'cct-lib)