diff options
Diffstat (limited to 'ci/compile-tests/003-require-error/test.el')
| -rw-r--r-- | ci/compile-tests/003-require-error/test.el | 42 |
1 files changed, 42 insertions, 0 deletions
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))) |