diff options
Diffstat (limited to 'ci/compile-tests/003-require-error/runtest.el')
| -rw-r--r-- | ci/compile-tests/003-require-error/runtest.el | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/ci/compile-tests/003-require-error/runtest.el b/ci/compile-tests/003-require-error/runtest.el new file mode 100644 index 00000000..c5e2a713 --- /dev/null +++ b/ci/compile-tests/003-require-error/runtest.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 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 + + +;; require cct-lib for the elisp compilation, otherwise this is present already +(require 'cct-lib) + +;;; 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))) |