include compile tests in CI elisp compilation

13 files changed, 54 insertions, 15 deletions

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)