blob: 9f4a2ce0b77707d1d23f98b28b861b2dfe8930f0 (
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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
;; 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 recompilation and ancestor registration for the case a
;; dependency is in state ready already.
;;
;; The following graph shows the file dependencies in this test:
;;
;; a
;; / \
;; b c
;; | |____________
;; d \
;; | |
;; e--f--g--h--i--j--k
;;
;; The idea is that the coqdep chain from b to j takes so long, that k
;; has been compiled and is in state ready before the coqdep results
;; from j are processed. This works - unless the disk cache is cold.
;; If it works the test triggers two bugs. First, k is locked with the
;; require command of c. Second, the modification time of k is not
;; propagated to j, such that the whole chain from j to b is not
;; recompiled after k has changed.
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib)
;;; set configuration
(cct-configure-proof-general)
;;; Data and utility functions
(defconst b-ancestors '("./b.v" "./d.v" "./e.v" "./f.v" "./g.v"
"./h.v" "./i.v" "./j.v" "./k.v")
"Ancestors of b.v.")
(defconst c-ancestors '("./c.v")
"Ancestors of c.v.")
(defconst all-ancestors (append b-ancestors c-ancestors)
"All ancestors.")
(defconst all-compiled-ancestors
(mapcar 'cct-library-vo-of-v-file all-ancestors)
"All vo ancestors files.")
(defun cct-replace-last-word (line word)
"Replace last word in line LINE with WORD.
In current buffer, go to the end of line LINE and one word
backward. Replace the word there with WORD."
(cct-goto-line line)
(end-of-line)
(backward-word)
(kill-word 1)
(insert word))
(defun cct-check-main-buffer (vo-times new-sum recompiled-files
other-locked-files)
"Perform various checks for recompilation in buffer a.v.
Combine all the following tests in this order:
- line 21 in a.v is unlocked
- after replacing the sum on line 28 with NEW-SUM, a.v can be
processed until line 38
- files in VO-TIMES not listed in RECOMPILED-FILES have the same
last change time as in VO-TIMES
- files in RECOMPILED-FILES have a newer change time
- the spans in line 22 and 23 hold the ancestors of b and c, respectively.
- all the buffers in OTHER-LOCKED-FILES are locked until line 18."
(let (splitted)
(set-buffer "a.v")
(cct-check-locked 21 'unlocked)
(cct-replace-last-word 28 new-sum)
(cct-process-to-line 38)
(cct-check-locked 37 'locked)
(setq splitted (cct-split-change-times vo-times recompiled-files))
(cct-unmodified-change-times (car splitted))
(cct-older-change-times (cdr splitted))
(cct-locked-ancestors 22 b-ancestors)
(cct-locked-ancestors 23 c-ancestors)
(mapc
(lambda (b)
(set-buffer b)
(cct-check-locked 18 'locked))
other-locked-files)))
;;; The test itself
(ert-deftest cct-change-recompile ()
"Test successful recompilation for a dependency in state ready."
;;(setq coq--debug-auto-compilation t)
(find-file "a.v")
;; 1. process original content - compile everything
(message "\n1. process original content - compile everything\n")
(cct-process-to-line 38)
(cct-check-locked 37 'locked)
(cct-locked-ancestors 22 b-ancestors)
(cct-locked-ancestors 23 c-ancestors)
(let ((vo-times (cct-record-change-times all-compiled-ancestors))
other-locked-files)
;; 2. retract and process again - nothing should be compiled
(message "\n2. retract and process again - nothing should be compiled\n")
(cct-process-to-line 21)
(cct-check-main-buffer vo-times "9" nil nil)
;; 3. change k and process again - everything should be compiled
(message "\n3. change k and process again - everything should be compiled\n")
(find-file "k.v")
(push "k.v" other-locked-files)
(cct-check-locked 21 'locked)
(cct-replace-last-word 21 "5")
(cct-check-main-buffer
vo-times "10"
'("./b.vo" "./c.vo" "./d.vo" "./e.vo" "./f.vo" "./g.vo"
"./h.vo" "./i.vo" "./j.vo" "./k.vo")
other-locked-files)
))
|
