diff options
Diffstat (limited to 'ci/compile-tests/001-mini-project/test.el')
| -rw-r--r-- | ci/compile-tests/001-mini-project/test.el | 40 |
1 files changed, 40 insertions, 0 deletions
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"))) |