From 12be85a9032ebed02d9b65da7848ab173081f41a Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Tue, 15 Dec 2020 21:54:53 +0100
Subject: include compile tests in CI elisp compilation

---
 ci/compile-tests/003-require-error/Makefile   |  4 +--
 ci/compile-tests/003-require-error/runtest.el | 45 +++++++++++++++++++++++++++
 ci/compile-tests/003-require-error/test.el    | 42 -------------------------
 3 files changed, 47 insertions(+), 44 deletions(-)
 create mode 100644 ci/compile-tests/003-require-error/runtest.el
 delete mode 100644 ci/compile-tests/003-require-error/test.el

(limited to 'ci/compile-tests/003-require-error')

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/runtest.el b/ci/compile-tests/003-require-error/runtest.el
new file mode 100644
index 00000000..c5e2a713
--- /dev/null
+++ b/ci/compile-tests/003-require-error/runtest.el
@@ -0,0 +1,45 @@
+;; This file is part of Proof General.
+;;
+;; © Copyright 2020  Hendrik Tews
+;;
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hendrik@askra.de>
+;;
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+;; Coq Compile Tests (cct) --
+;; ert tests for parallel background compilation for Coq
+;;
+;; Test parallel background compilation when coqdep fails on a require
+;; command.
+;;
+;; The following graph shows the file dependencies in this test, where
+;; X does not exist:
+;;
+;;   a1    a2   a3
+;;   |    /  \ /
+;;   b   X    c
+;;
+;; 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)
+
+;;; Define the tests
+
+(ert-deftest cct-require-error ()
+  "Test background compilation with an require that yields a coqdep error."
+  (let ((test-start-time (current-time)))
+    (find-file "a.v")
+    (cct-process-to-line 26)
+
+    (cct-check-locked 22 'locked)
+    (cct-check-locked 23 'unlocked)
+    (cct-file-newer "b.vo" test-start-time)
+    (cct-file-newer "c.vo" test-start-time)))
diff --git a/ci/compile-tests/003-require-error/test.el b/ci/compile-tests/003-require-error/test.el
deleted file mode 100644
index 0a0dd3d4..00000000
--- a/ci/compile-tests/003-require-error/test.el
+++ /dev/null
@@ -1,42 +0,0 @@
-;; This file is part of Proof General.
-;;
-;; © Copyright 2020  Hendrik Tews
-;;
-;; Authors: Hendrik Tews
-;; Maintainer: Hendrik Tews <hendrik@askra.de>
-;;
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-
-;;; Commentary:
-;;
-;; Coq Compile Tests (cct) --
-;; ert tests for parallel background compilation for Coq
-;;
-;; Test parallel background compilation when coqdep fails on a require
-;; command.
-;;
-;; The following graph shows the file dependencies in this test, where
-;; X does not exist:
-;;
-;;   a1    a2   a3
-;;   |    /  \ /
-;;   b   X    c
-;;
-;; and where a1, a2 and a3 are the 3 require commands in file a.v
-
-
-;;; set configuration
-(cct-configure-proof-general)
-
-;;; Define the tests
-
-(ert-deftest cct-require-error ()
-  "Test background compilation with an require that yields a coqdep error."
-  (let ((test-start-time (current-time)))
-    (find-file "a.v")
-    (cct-process-to-line 26)
-
-    (cct-check-locked 22 'locked)
-    (cct-check-locked 23 'unlocked)
-    (cct-file-newer "b.vo" test-start-time)
-    (cct-file-newer "c.vo" test-start-time)))
-- 
cgit v1.2.3