enable Tramp support for Emacs 26 or later

ci/compile-tests/007-slow-require/Makefile

@@ -19,6 +19,11 @@ TEST_SOURCES:=\
 	a5.v b5.v c5.v d5.v \
 	a6.v b6.v c6.v d6.v
 
+# This test uses ../bin/compile-test-start-delayed to start certain
+# commands with specified delays to check carfully constructed
+# internal states. compile-test-start-delayed outputs diagnostics on
+# file descriptor 9, which bypasses emacs and is joined with stderr of
+# the current make. Open file descriptor 9 here.
 .PHONY: test
 test:
 	$(MAKE) clean

ci/compile-tests/007-slow-require/b1.v.orig

@@ -23,5 +23,5 @@
 
 Require Export d1.
 
-(* This is line 27 *)
+(* This is line 26 *)
 Definition b : nat := 2.

ci/compile-tests/007-slow-require/b3.v.orig

@@ -23,5 +23,5 @@
 
 Require Export d3.
 
-(* This is line 27 *)
+(* This is line 26 *)
 Definition b : nat := 2.

ci/compile-tests/007-slow-require/b4.v.orig

@@ -23,5 +23,5 @@
 
 Require Export d4.
 
-(* This is line 27 *)
+(* This is line 26 *)
 Definition b : nat := 2.

ci/compile-tests/007-slow-require/b5.v.orig

@@ -23,5 +23,5 @@
 
 Require Export d5.
 
-(* This is line 27 *)
+(* This is line 26 *)
 Definition b : nat := 2.

ci/compile-tests/007-slow-require/b6.v.orig

@@ -23,5 +23,5 @@
 
 Require Export d6.
 
-(* This is line 27 *)
+(* This is line 26 *)
 Definition b : nat := 2.

ci/compile-tests/007-slow-require/runtest.el

@@ -17,7 +17,11 @@
 ;; in each possible state. For specifying the different delays there
 ;; are 6 mini projects, one for each test in this file. Each project
 ;; consists of four files, a1.v, b1.v, c1.v and d1.v for the first one
-;; and a6.v, b6.v, c6.v and d6.v for the sixth one.
+;; and a6.v, b6.v, c6.v and d6.v for the sixth one. Each project is
+;; one ert test, described further below. In each project or test, the
+;; top level require commands are asserted and retracted several times
+;; with changes in different files to test (almost) all possible
+;; internal state combinations.
 ;;
 ;; The dependencies are the same in all projects:
 ;; 

ci/compile-tests/008-default-dir/Makefile

@@ -0,0 +1,34 @@
+# This file is part of Proof General.
+# 
+# © Copyright 2021  Hendrik Tews
+# 
+# Authors: Hendrik Tews
+# Maintainer: Hendrik Tews <[email protected]>
+# 
+# License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+
+# This test modifies some .v files during the test. The original
+# versions are in .v.orig files. They are moved to the corresponding
+# .v files before the test starts.
+TEST_SOURCES:= a.v b.v c.v
+
+# This test uses ../bin/compile-test-start-delayed to start certain
+# commands with specified delays to check carfully constructed
+# internal states. compile-test-start-delayed outputs diagnostics on
+# file descriptor 9, which bypasses emacs and is joined with stderr of
+# the current make. Open file descriptor 9 here.
+.PHONY: test
+test:
+	$(MAKE) clean
+	$(MAKE) $(TEST_SOURCES)
+	emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \
+		-l runtest.el -f ert-run-tests-batch-and-exit \
+		9>&1
+
+%.v: %.v.orig
+	cp $< $@
+
+.PHONY: clean
+clean:
+	rm -f *.vo *.glob *.vio *.vos *.vok .*.aux $(TEST_SOURCES)

ci/compile-tests/008-default-dir/a.v.orig

@@ -0,0 +1,40 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+(* The delay for coqdep is specified in comments with key coqdep-delay,
+ * see compile-test-start-delayed.
+ *)
+
+
+(* This is line 24 *)
+Require Export (* coqdep-delay 1 *) b.
+(* This is line 26 *)
+
+
+(* This is line 29 *)
+Definition sum : nat := 5.
+
+
+(* This is line 33 *)
+Lemma x : b + c = sum.
+Proof using.
+  unfold b, c, sum in *.
+  simpl.
+  trivial.
+Qed.
+(* This is line 40 *)

ci/compile-tests/008-default-dir/b.v.orig

@@ -0,0 +1,23 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+
+Require Export c.
+
+(* This is line 22 *)
+Definition b : nat := 2.

ci/compile-tests/008-default-dir/c.v.orig

@@ -0,0 +1,23 @@
+(* This file is part of Proof General.
+ *
+ * © Copyright 2021  Hendrik Tews
+ *
+ * Authors: Hendrik Tews
+ * Maintainer: Hendrik Tews <[email protected]>
+ *
+ * License:     GPL (GNU GENERAL PUBLIC LICENSE)
+ *
+ *
+ * This file is part of an automatic test case for parallel background
+ * compilation in coq-par-compile.el. See test.el in this directory.
+ *)
+
+(* The test script relies on absolute line numbers. 
+ * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING.
+ *)
+
+
+
+
+(* This is line 22 *)
+Definition c : nat := 3.

ci/compile-tests/008-default-dir/runtest.el

@@ -0,0 +1,143 @@
+;; This file is part of Proof General.
+;; 
+;; © Copyright 2021  Hendrik Tews
+;; 
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <[email protected]>
+;; 
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+;; Coq Compile Tests (cct) --
+;; ert tests for parallel background compilation for Coq
+;;
+;; Test that default-directory is correctly set independently of the
+;; current buffer in the foreground.
+;;
+;; The dependencies in this test are:
+;; 
+;;           a
+;;           |
+;;           b
+;;           |
+;;           c
+;;
+
+
+;; require cct-lib for the elisp compilation, otherwise this is present already
+(require 'cct-lib)
+
+;;; set configuration
+(cct-configure-proof-general)
+(configure-delayed-coq)    
+
+(defconst all-ancestors '("./b.v" "./c.v")
+  "All ancestors.")
+
+(defconst all-compiled-ancestors
+  (mapcar 'cct-library-vo-of-v-file all-ancestors)
+  "All vo ancestors files.")
+
+(defun check-main-buffer (vo-times new-sum recompiled-files
+                                       other-locked-files)
+  "Perform various checks in buffer a.v.
+See `cct-generic-check-main-buffer'."
+  (cct-generic-check-main-buffer
+   "a.v"                                ; main-buf
+   24                                   ; main-unlocked
+   40                                   ; main-locked
+   30                                   ; main-sum-line
+   new-sum
+   vo-times
+   recompiled-files
+   `((25 . ,all-ancestors))             ; require-ancestors
+   other-locked-files
+   23                                   ; other-locked-line
+   ))
+
+
+;;; The test itself
+
+(ert-deftest test-default-dir ()
+  "`default-directory' test.
+Test that `default-directory' is correctly set independently of the
+current buffer in the foreground."
+  (let (vo-times av-buffer ci-buffer other-locked-files
+        vok-times vos-vio-files)
+
+    ;; (setq cct--debug-tests t)
+    ;; (setq coq--debug-auto-compilation t)
+    (find-file "a.v")
+    (setq av-buffer (current-buffer))
+
+    (message
+     "coqdep: %s\ncoqc: %s\nPATH %s\nexec-path: %s\ndetected coq version: %s"
+     coq-dependency-analyzer
+     coq-compiler
+     (getenv "PATH")
+     exec-path
+     coq-autodetected-version)
+
+    (find-file "../..")
+    (setq ci-buffer (current-buffer))
+
+    (add-hook 'cct-before-busy-waiting-hook (lambda () (set-buffer ci-buffer)))
+    (add-hook 'cct-after-busy-waiting-hook (lambda () (set-buffer av-buffer)))
+
+    ;; 1. process original content - compile everything
+    (message "\n1. process original content - compile everything\n")
+    (check-main-buffer vo-times "5" nil other-locked-files)
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+
+    ;; 2. retract and process again - nothing should be compiled
+    (message "\n2. retract and process again - nothing should be compiled\n")
+    (cct-process-to-line 21)
+    (check-main-buffer vo-times "5" nil other-locked-files)
+
+    ;; 3. change b and process again - only b should get compiled
+    (message "\n3. change b and process again - only b should get compiled\n")
+    (find-file "b.v")
+    (push "b.v" other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 23 "3")
+    (check-main-buffer vo-times "6" '("./b.vo") other-locked-files)
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+
+    ;; 4. change c and process again - b and c should get compiled
+    (message "\n4. change c and process again - b and c should get compiled\n")
+    (find-file "c.v")
+    (push "c.v" other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 23 "5")
+    (check-main-buffer vo-times "8" '("./b.vo" "./c.vo") other-locked-files)
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+
+    ;; 5. change b and c and reprocess with vos-and-vok/quick-and-vio2vo
+    (message
+     "\n5. change b and c and reprocess with vos-and-vok/quick-and-vio2vo\n")
+    (if (coq--post-v811)
+        (setq coq-compile-vos 'vos-and-vok
+              vos-vio-files '("./b.vos" "./c.vos")
+              vok-times (cct-record-change-times '("./b.vok" "./c.vok")))
+      (setq coq-compile-quick 'quick-and-vio2vo
+            vos-vio-files '("./b.vio" "./c.vio")))
+
+    (set-buffer "b.v")
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 23 "7")
+    (set-buffer "c.v")
+    (cct-check-locked 23 'unlocked)
+    (cct-replace-last-word 23 "10")
+    (check-main-buffer nil "17" nil other-locked-files)
+
+    (cct-files-are-readable vos-vio-files)
+    ;; this will switch to a different default-directory, see the
+    ;; hooks above
+    (cct-wait-for-second-stage)
+    (if (coq--post-v811)
+        (progn
+          (cct-older-change-times vok-times)
+          (cct-unmodified-change-times vo-times))
+      (cct-older-change-times vo-times))
+    ))

ci/compile-tests/README.md

@@ -9,7 +9,32 @@ Each test comes with a hand-crafted set of Coq source files that
 implement a particular dependency tree. Therefore, most of the
 tests have a subdirectory on their own.
 
-Tests currently missing:
+# Overview of existing tests
+
+All tests are for parallel background compilation.
+
+001-mini-project
+: test compilation for a simple project
+002-require-no-dependencies
+: Test a require that does not produce any dependencies.
+003-require-error
+: coqdep fails on a require
+004-dependency-cycle
+: dependency cycle
+005-change-recompile
+: test that the right files are recompiled when changes are made
+006-ready-dependee
+: dependency in state ready
+007-slow-require
+: test almost all internal state combinations with delay on
+  coqdep and coqc
+008-default-dir
+: test that the default/current directory is set correctly
+  independent of user/emacs changing the current buffer during
+  first and second stage compilation
+
+# Tests currently missing
+
 - unlock checks for ancestors of failed jobs in different cases
 - a job depending on a failed dependee, where the dependee has
   been finished before
@@ -19,3 +44,8 @@ Tests currently missing:
   in state waiting-queue
 - coq-par-create-file-job finds a failed job
 - all tests in all quick and all vos variants
+- test two coq-par-kickoff-queue-from-action-list entries being
+  active at the same time: assert one region, let compilation
+  fail, assert second region, while first region is still busy,
+  this should fail in some weird way, because failed is not
+  propagated