blob: c5e2a713c87cc0e3504eaf2d9f6ff6dc6c0079d8 (
plain)
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
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)))
|
