diff options
Diffstat (limited to 'ci/compile-tests')
27 files changed, 701 insertions, 0 deletions
diff --git a/ci/compile-tests/001-mini-project/Makefile b/ci/compile-tests/001-mini-project/Makefile new file mode 100644 index 00000000..4ae0a433 --- /dev/null +++ b/ci/compile-tests/001-mini-project/Makefile @@ -0,0 +1,19 @@ +# 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) + + +.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 + +.PHONY: clean +clean: + rm -f *.vo *.glob *.vio *.vos *.vok .*.aux diff --git a/ci/compile-tests/001-mini-project/a.v b/ci/compile-tests/001-mini-project/a.v new file mode 100644 index 00000000..fe3521ba --- /dev/null +++ b/ci/compile-tests/001-mini-project/a.v @@ -0,0 +1,24 @@ +(* 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) + * + * + * 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 21 *) +Require b. +Require c. +(* This is line 24 *) diff --git a/ci/compile-tests/001-mini-project/b.v b/ci/compile-tests/001-mini-project/b.v new file mode 100644 index 00000000..ed30f615 --- /dev/null +++ b/ci/compile-tests/001-mini-project/b.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Require d e. diff --git a/ci/compile-tests/001-mini-project/c.v b/ci/compile-tests/001-mini-project/c.v new file mode 100644 index 00000000..a8799333 --- /dev/null +++ b/ci/compile-tests/001-mini-project/c.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Require e f. diff --git a/ci/compile-tests/001-mini-project/d.v b/ci/compile-tests/001-mini-project/d.v new file mode 100644 index 00000000..ca175bfc --- /dev/null +++ b/ci/compile-tests/001-mini-project/d.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Definition d : nat := 0. diff --git a/ci/compile-tests/001-mini-project/e.v b/ci/compile-tests/001-mini-project/e.v new file mode 100644 index 00000000..7cd08e90 --- /dev/null +++ b/ci/compile-tests/001-mini-project/e.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Definition e : nat := 1. diff --git a/ci/compile-tests/001-mini-project/f.v b/ci/compile-tests/001-mini-project/f.v new file mode 100644 index 00000000..f5e47cd8 --- /dev/null +++ b/ci/compile-tests/001-mini-project/f.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Definition f : nat := 2. diff --git a/ci/compile-tests/001-mini-project/test.el b/ci/compile-tests/001-mini-project/test.el new file mode 100644 index 00000000..49cc91f7 --- /dev/null +++ b/ci/compile-tests/001-mini-project/test.el @@ -0,0 +1,40 @@ +;; 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 that parallel background compilation works for a simple +;; project and that the right files are recorded for unlocking at the +;; right places. +;; +;; The following graph shows the file dependencies in this test: +;; +;; a +;; / \ +;; b c +;; / \ / \ +;; d e f + + +;;; set configuration +(cct-configure-proof-general) + +;;; Define the test + +(ert-deftest cct-mini-project () + "Test successful background compilation and ancestor recording." + (find-file "a.v") + (cct-process-to-line 25) + + (cct-check-locked 24 'locked) + (cct-locked-ancestors 22 '("./b.v" "./d.v" "./e.v")) + (cct-locked-ancestors 23 '("./c.v" "./f.v"))) diff --git a/ci/compile-tests/002-require-no-dependencies/Makefile b/ci/compile-tests/002-require-no-dependencies/Makefile new file mode 100644 index 00000000..4ae0a433 --- /dev/null +++ b/ci/compile-tests/002-require-no-dependencies/Makefile @@ -0,0 +1,19 @@ +# 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) + + +.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 + +.PHONY: clean +clean: + rm -f *.vo *.glob *.vio *.vos *.vok .*.aux diff --git a/ci/compile-tests/002-require-no-dependencies/a.v b/ci/compile-tests/002-require-no-dependencies/a.v new file mode 100644 index 00000000..b44c78f3 --- /dev/null +++ b/ci/compile-tests/002-require-no-dependencies/a.v @@ -0,0 +1,24 @@ +(* 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) + * + * + * 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 21 *) +Require Coq.Bool.Bool. +Definition a : nat := 0. +(* This is line 24 *) diff --git a/ci/compile-tests/002-require-no-dependencies/b.v b/ci/compile-tests/002-require-no-dependencies/b.v new file mode 100644 index 00000000..d37d48bb --- /dev/null +++ b/ci/compile-tests/002-require-no-dependencies/b.v @@ -0,0 +1,24 @@ +(* 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) + * + * + * 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 21 *) +Require Coq.Bool.Bool. +Require c. +(* This is line 24 *) diff --git a/ci/compile-tests/002-require-no-dependencies/c.v b/ci/compile-tests/002-require-no-dependencies/c.v new file mode 100644 index 00000000..8619c90b --- /dev/null +++ b/ci/compile-tests/002-require-no-dependencies/c.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Definition c : nat := 0. diff --git a/ci/compile-tests/002-require-no-dependencies/test.el b/ci/compile-tests/002-require-no-dependencies/test.el new file mode 100644 index 00000000..69de9baa --- /dev/null +++ b/ci/compile-tests/002-require-no-dependencies/test.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 one require command does +;; not produce any dependencies. +;; +;; The following graph shows the file dependencies in this test: +;; +;; a b +;; | +;; c + + +;;; 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"))) diff --git a/ci/compile-tests/003-require-error/Makefile b/ci/compile-tests/003-require-error/Makefile new file mode 100644 index 00000000..4ae0a433 --- /dev/null +++ b/ci/compile-tests/003-require-error/Makefile @@ -0,0 +1,19 @@ +# 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) + + +.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 + +.PHONY: clean +clean: + rm -f *.vo *.glob *.vio *.vos *.vok .*.aux diff --git a/ci/compile-tests/003-require-error/a.v b/ci/compile-tests/003-require-error/a.v new file mode 100644 index 00000000..d5716ae0 --- /dev/null +++ b/ci/compile-tests/003-require-error/a.v @@ -0,0 +1,25 @@ +(* 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) + * + * + * 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 21 *) +Require b. +Require X c. +Require c. +(* This is line 25 *) diff --git a/ci/compile-tests/003-require-error/b.v b/ci/compile-tests/003-require-error/b.v new file mode 100644 index 00000000..e3f5da5f --- /dev/null +++ b/ci/compile-tests/003-require-error/b.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Definition b : nat := 2. diff --git a/ci/compile-tests/003-require-error/c.v b/ci/compile-tests/003-require-error/c.v new file mode 100644 index 00000000..bd60ca0d --- /dev/null +++ b/ci/compile-tests/003-require-error/c.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Definition c : nat := 3. diff --git a/ci/compile-tests/003-require-error/test.el b/ci/compile-tests/003-require-error/test.el new file mode 100644 index 00000000..0a0dd3d4 --- /dev/null +++ b/ci/compile-tests/003-require-error/test.el @@ -0,0 +1,42 @@ +;; 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))) diff --git a/ci/compile-tests/004-dependency-cycle/Makefile b/ci/compile-tests/004-dependency-cycle/Makefile new file mode 100644 index 00000000..4ae0a433 --- /dev/null +++ b/ci/compile-tests/004-dependency-cycle/Makefile @@ -0,0 +1,19 @@ +# 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) + + +.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 + +.PHONY: clean +clean: + rm -f *.vo *.glob *.vio *.vos *.vok .*.aux diff --git a/ci/compile-tests/004-dependency-cycle/a.v b/ci/compile-tests/004-dependency-cycle/a.v new file mode 100644 index 00000000..d84f5d10 --- /dev/null +++ b/ci/compile-tests/004-dependency-cycle/a.v @@ -0,0 +1,24 @@ +(* 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) + * + * + * 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 21 *) +Require b. +Require f. +(* This is line 24 *) diff --git a/ci/compile-tests/004-dependency-cycle/b.v b/ci/compile-tests/004-dependency-cycle/b.v new file mode 100644 index 00000000..c703c3ae --- /dev/null +++ b/ci/compile-tests/004-dependency-cycle/b.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Require c. diff --git a/ci/compile-tests/004-dependency-cycle/c.v b/ci/compile-tests/004-dependency-cycle/c.v new file mode 100644 index 00000000..53bc67d5 --- /dev/null +++ b/ci/compile-tests/004-dependency-cycle/c.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Require d. diff --git a/ci/compile-tests/004-dependency-cycle/d.v b/ci/compile-tests/004-dependency-cycle/d.v new file mode 100644 index 00000000..d06e5fec --- /dev/null +++ b/ci/compile-tests/004-dependency-cycle/d.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Require e. diff --git a/ci/compile-tests/004-dependency-cycle/e.v b/ci/compile-tests/004-dependency-cycle/e.v new file mode 100644 index 00000000..604b44e0 --- /dev/null +++ b/ci/compile-tests/004-dependency-cycle/e.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Require b. diff --git a/ci/compile-tests/004-dependency-cycle/f.v b/ci/compile-tests/004-dependency-cycle/f.v new file mode 100644 index 00000000..e3f5da5f --- /dev/null +++ b/ci/compile-tests/004-dependency-cycle/f.v @@ -0,0 +1,15 @@ +(* 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) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +Definition b : nat := 2. diff --git a/ci/compile-tests/004-dependency-cycle/test.el b/ci/compile-tests/004-dependency-cycle/test.el new file mode 100644 index 00000000..5f9f63f3 --- /dev/null +++ b/ci/compile-tests/004-dependency-cycle/test.el @@ -0,0 +1,58 @@ +;; 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 for a dependency cycle. +;; +;; The following graph shows the file dependencies in this test: +;; +;; a1 a2 +;; / | +;; b<-e f +;; | | +;; c->d +;; +;; where a1 and a2 are the 2 require commands in file a.v. + + +;;; set configuration +(cct-configure-proof-general) + +;;; Define the tests + +(ert-deftest cct-require-error () + "Test background compilation on cyclic dependencies." + (find-file "a.v") + (cct-process-to-line 25) + (let ((last-message (cct-last-message-line)) + message-cycle) + (should (equal "Coq compilation error: Circular dependency" + (substring last-message 0 42))) + + (should + (string-match + (concat + "\\./\\([b-e]\\).v -> \\./\\([b-e]\\).v -> " + "\\./\\([b-e]\\).v -> \\./\\([b-e]\\).v") + last-message)) + (setq message-cycle + (list (match-string 1 last-message) (match-string 2 last-message) + (match-string 3 last-message) (match-string 4 last-message))) + (should + (or (equal message-cycle '("b" "c" "d" "e")) + (equal message-cycle '("c" "d" "e" "b")) + (equal message-cycle '("d" "e" "b" "c")) + (equal message-cycle '("e" "b" "c" "d")))) + + (cct-check-locked 21 'locked) + (cct-check-locked 22 'unlocked))) diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el new file mode 100644 index 00000000..42003d1c --- /dev/null +++ b/ci/compile-tests/cct-lib.el @@ -0,0 +1,124 @@ +;; 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 +;; +;; This file contains common definitions for the automated tests of +;; parallel background compilation. + + +(defmacro cct-implies (p q) + "Short-circuit logical implication. +Evaluate Q only if P is non-nil." + `(or (not ,p) ,q)) + +(defun cct-goto-line (line) + "Put point on start of line LINE. +Very similar to `goto-line', but the documentation of `goto-line' +says, programs should use this piece of code." + (goto-char (point-min)) + (forward-line (1- line))) + +(defun cct-process-to-line (line) + "Assert/retract to line LINE and wait until processing completed." + (cct-goto-line line) + (proof-goto-point) + + (while (or proof-second-action-list-active (consp proof-action-list)) + ;; (message "wait for coq/compilation with %d items queued\n" + ;; (length proof-action-list)) + ;; + ;; accept-process-output without timeout returns rather quickly, + ;; apparently most times without process output or any other event + ;; to process. + (accept-process-output nil 0.1))) + +(defun cct-get-vanilla-span (line) + "Get THE vanilla span for line LINE, report an error if there is none. +PG uses a number of overlapping and non-overlapping spans (read +overlays) in the asserted and queue region of the proof buffer, +see the comments in generic/proof-script.el. Spans of type +vanilla (stored at 'type in the span property list) are created +for real commands (not for comments). They hold various +information that is used, among others, for backtracking. + +This function returns the vanilla span that covers line LINE and +reports a test failure if there is none or more than one vanilla spans." + (let (spans) + (cct-goto-line line) + (setq spans (spans-filter (overlays-at (point)) 'type 'vanilla)) + (should (eq (length spans) 1)) + (car spans))) + +(defun cct-last-message-line () + "Extract the last line from the *Messages* buffer. +Useful if the message is not present in the echo area any more +and `current-message' does not return anything." + (save-excursion + (set-buffer "*Messages*") + (goto-char (point-max)) + (forward-line -1) + (buffer-substring (point) (- (point-max) 1)))) + +(defun cct-check-locked (line locked-state) + "Check that line LINE has locked state LOCKED-STATE +LOCKED-STATE must be 'locked or 'unlocked. This function checks +whether line LINE is inside or outside the asserted (locked) +region of the buffer and signals a test failure if not." + (let ((locked (eq locked-state 'locked))) + ;; (message "tcl line %d check %s: %s %s\n" + ;; line (if locked "locked" "unlocked") + ;; proof-locked-span + ;; (if (overlayp proof-locked-span) + ;; (span-end proof-locked-span) + ;; "no-span")) + (cl-assert (or locked (eq locked-state 'unlocked)) + nil "test-check-locked 2nd argument wrong") + (cct-goto-line line) + (should (cct-implies locked (span-end proof-locked-span))) + + (should + (or + (and (not locked) + (or (not proof-locked-span) (not (span-end proof-locked-span)))) + (and (span-end proof-locked-span) + (funcall (if locked '< '>) + (point) (span-end proof-locked-span))))))) + +(defun cct-locked-ancestors (line ancestors) + "Check that the vanilla span at line LINE has ANCESTORS recorded. +The comparison treats ANCESTORS as set but the file names must +be `equal' as strings. + +Ancestors are recoreded in the 'coq-locked-ancestors property of +the vanilla spans of require commands, see the in-file +documentation of coq/coq-par-compile.el." + (let ((locked-ancestors + (span-property (cct-get-vanilla-span line) 'coq-locked-ancestors))) + (should + (seq-set-equal-p locked-ancestors ancestors)))) + +(defun cct-file-newer (file time) + "Check that FILE exists and its modification time is more recent than TIME." + (let ((file-time (nth 5 (file-attributes file)))) + (should (and file-time (time-less-p time file-time))))) + +(defun cct-configure-proof-general () + "Configure Proof General for test execution." + (setq delete-old-versions t + coq-compile-before-require t + coq-compile-keep-going t + proof-auto-action-when-deactivating-scripting 'retract + proof-three-window-enable nil + coq-compile-auto-save 'save-coq + coq--debug-auto-compilation nil)) |