add Coq compile test for a delayed require

1 files changed, 211 insertions, 0 deletions

diff --git a/ci/compile-tests/007-slow-require/runtest.el b/ci/compile-tests/007-slow-require/runtest.el
new file mode 100644
index 00000000..52c2f392
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/runtest.el
@@ -0,0 +1,211 @@
+;; This file is part of Proof General.
+;; 
+;; © Copyright 2021  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 two require jobs with different delays such that
+;; coq-par-retire-top-level-job happens when the other require job is
+;; 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.
+;;
+;; The dependencies are the same in all projects:
+;; 
+;;           a
+;;          / \
+;;         b   c
+;;          \ /
+;;           d
+;;
+;; Test 1 delays coqdep on require c, such that queue kickoff happens
+;; in state 'enqueued-coqdep, the dependency link d->c is created when
+;; d is ready and kickoff-queue-maybe on require c happens when
+;; require b is in state 'ready.
+;;
+;; Test 2 delays coqdep on c, such that queue kickoff happens in state
+;; 'waiting-dep.
+;;
+;; Test 3 delays coqdep on require b, such that kickoff-queue-maybe on
+;; require c happens when require b is in state 'enqueued-coqdep and
+;; queue kickoff happens in state 'waiting-queue.
+;;
+;; Test 4 delays coqdep on b, such that kickoff-queue-maybe on require
+;; c happens when require b is in state 'waiting-dep.
+;;
+;; Test 5 delays coqdep on d, such that the second dependency on d is
+;; created when d is in state enqueued-coqdep.
+;;
+;; Test 6 delays coqdep on c for 2 seconds and coqc on d for 4
+;; seconds, such that the dependency link d->c is created when d is in
+;; state enqueued-coqc.
+
+;; 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 pre-b-ancestors '("./b" "./d")
+    "Ancestors of b without suffixes.")
+
+(defconst pre-c-ancestors '("./c")
+  "Ancestors of c without suffixes.")
+
+(defconst pre-all-ancestors (append pre-b-ancestors pre-c-ancestors)
+  "All ancestors without suffixes.")
+
+(defun b-ancestors (n)
+  "Ancestors of b for part N."
+  (mapcar (lambda (a) (concat a (format "%d.v" n))) pre-b-ancestors))
+
+(defun c-ancestors (n)
+  "Ancestors of c for part N."
+  (mapcar (lambda (a) (concat a (format "%d.v" n))) pre-c-ancestors))
+
+(defun all-ancestors (n)
+  "All ancestors for part N."
+  (mapcar (lambda (a) (concat a (format "%d.v" n))) pre-all-ancestors))
+
+(defun all-compiled-ancestors (n)
+  "All vo ancestor files for part N."
+  (mapcar 'cct-library-vo-of-v-file (all-ancestors n)))
+
+(defun check-main-buffer (n vo-times new-sum recompiled-files
+                                       other-locked-files)
+  "Perform various checks in buffer aN.v.
+See `cct-generic-check-main-buffer'."
+  (cct-generic-check-main-buffer
+   (format "a%d.v" n)                   ; main-buf
+   25                                   ; main-unlocked
+   41                                   ; main-locked
+   31                                   ; main-sum-line
+   new-sum
+   vo-times
+   recompiled-files
+   `((25 . ,(b-ancestors n)) (26 . ,(c-ancestors n))) ; require-ancestors
+   other-locked-files
+   27                                   ; other-locked-line
+   ))
+
+
+;;; Define the test
+
+(defun test-slow-require (n)
+  "Test part N of slow require job tests.
+XXX Test a setting where the second require job is still in state
+'enqueued-coqdep when the first one finishes."
+  (let*
+      ;; .v file names are used as file and as buffer names
+      ((av (format "a%d.v" n))
+       (bv (format "b%d.v" n))
+       (cv (format "c%d.v" n))
+       (dv (format "d%d.v" n))
+       ;; .vo names compared with ancestors, they need a "./" prefix
+       (bvo (concat "./" (cct-library-vo-of-v-file bv)))
+       (cvo (concat "./" (cct-library-vo-of-v-file cv)))
+       (dvo (concat "./" (cct-library-vo-of-v-file dv)))
+       vo-times other-locked-files)
+
+    ;; (setq cct--debug-tests t)
+    ;; (setq coq--debug-auto-compilation t)
+    (find-file av)
+    (message "coqdep: %s\ncoqc: %s\nPATH %s\nexec-path: %s"
+             coq-dependency-analyzer
+             coq-compiler
+             (getenv "PATH")
+             exec-path)
+
+    ;; 1. process original content - compile everything
+    (message "\n%d.1. process original content - compile everything\n" n)
+    ;;(setq coq--debug-auto-compilation t)
+    (cct-process-to-line 42)
+    (cct-check-locked 41 'locked)
+    (cct-locked-ancestors 25 (b-ancestors n))
+    (cct-locked-ancestors 26 (c-ancestors n))
+
+    ;; (cl-assert nil nil "exit")
+
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    ;; 2. retract and process again - nothing should be compiled
+    (message "\n%d.2. retract and process again - nothing should be compiled\n"
+             n)
+    (cct-process-to-line 24)
+    (check-main-buffer n vo-times "9" nil nil)
+
+    ;; 3. change d and process again - b and c should be compiled
+    (message "\n%d.3. change d and process again - b and c should be compiled\n"
+             n)
+    (find-file dv)
+    (push dv other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 27 "5")
+    (check-main-buffer n vo-times "10" (list bvo cvo dvo)
+                       other-locked-files)
+
+    ;; 4. change b and process again - only b should be compiled
+    (message "\n%d.4. change b and process again - only b should be compiled\n"
+             n)
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    (find-file bv)
+    (push bv other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 27 "4")
+    (check-main-buffer n vo-times "12" (list bvo) other-locked-files)
+
+    ;; 5. change c and process again - only c should be compiled
+    (message "\n%d.5. change c and process again - only c should be compiled\n"
+             n)
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    (find-file cv)
+    (push cv other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 27 "8")
+    (check-main-buffer n vo-times "17" (list cvo) other-locked-files)
+
+    ;; 6. delete d and process again - b and c should be compiled
+    (message "\n%d.6. delete d and process again - b and c should be compiled\n"
+             n)
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    (delete-file dvo)
+    (set-buffer av)
+    (cct-process-to-line 24)
+    (check-main-buffer n vo-times "17" (list bvo cvo dvo)
+                       other-locked-files)
+
+    ;; 7. delete b and process again - only b should be compiled
+    (message "\n%d.7. delete b and process again - only b should be compiled\n"
+             n)
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    (delete-file bvo)
+    (set-buffer av)
+    (cct-process-to-line 24)
+    (check-main-buffer n vo-times "17" (list bvo) other-locked-files)
+
+    ;; 8. delete c and process again - only c should be compiled
+    (message "\n%d.8. delete c and process again - only c should be compiled\n"
+             n)
+    (setq vo-times (cct-record-change-times (all-compiled-ancestors n)))
+    (delete-file cvo)
+    (set-buffer av)
+    (cct-process-to-line 24)
+    (check-main-buffer n vo-times "17" (list cvo) other-locked-files)
+  ))
+
+
+(ert-deftest cct-slow-require-1 () (test-slow-require 1))
+(ert-deftest cct-slow-require-2 () (test-slow-require 2))
+(ert-deftest cct-slow-require-3 () (test-slow-require 3))
+(ert-deftest cct-slow-require-4 () (test-slow-require 4))
+(ert-deftest cct-slow-require-5 () (test-slow-require 5))
+(ert-deftest cct-slow-require-6 () (test-slow-require 6))