1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
;; This file is part of Proof General. -*- lexical-binding: t; -*-
;;
;; © Copyright 2020 Hendrik Tews
;;
;; Authors: Hendrik Tews
;; Maintainer: Hendrik Tews <hendrik@askra.de>
;;
;; SPDX-License-Identifier: GPL-3.0-or-later
;;; 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
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
;;; 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")
; (setq coq--debug-auto-compilation t)
(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")))
|
