include compile tests in CI elisp compilation

1 files changed, 48 insertions, 0 deletions

diff --git a/ci/compile-tests/002-require-no-dependencies/runtest.el b/ci/compile-tests/002-require-no-dependencies/runtest.el
new file mode 100644
index 00000000..f2feefad
--- /dev/null
+++ b/ci/compile-tests/002-require-no-dependencies/runtest.el
@@ -0,0 +1,48 @@
+;; 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 one require command does
+;; not produce any dependencies.
+;;
+;; The following graph shows the file dependencies in this test:
+;; 
+;;      a    b
+;;           |
+;;           c
+
+
+;; 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-one-require-with-no-dependencies ()
+  "Test background compilation with an require with no dependencies."
+  (find-file "a.v")
+  (cct-process-to-line 25)
+  
+  (cct-check-locked 24 'locked)
+  (cct-locked-ancestors 22 '()))
+    
+(ert-deftest cct-two-requires-first-no-dependencies ()
+  "Test background compilation with an require with no dependencies."
+  (find-file "b.v")
+  (cct-process-to-line 25)
+  
+  (cct-check-locked 24 'locked)
+  (cct-locked-ancestors 22 '())
+  (cct-locked-ancestors 23 '("./c.v")))