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