aboutsummaryrefslogtreecommitdiff
path: root/ci/compile-tests/007-slow-require/runtest.el
diff options
context:
space:
mode:
Diffstat (limited to 'ci/compile-tests/007-slow-require/runtest.el')
-rw-r--r--ci/compile-tests/007-slow-require/runtest.el211
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))
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:35:50 +0000