blob: 8b8ed79ba4b2c93bc4241706a157a4de22b6569d (
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
|
Handling of Multiple Files
==========================
[C depends on A and B]
Notation: A means that buffer A.l is unlocked
A+ means that buffer A.l is partly locked
A* means that buffer A.l is locked
? means that behaviour might be different for proof systems
with non-linear contexts
Test Protocol
-------------
1) visit A.l EFFECTS A
2) visit C.l EFFECTS A C
3) assert C EFFECTS A* C*
4) visit B.l EFFECTS A* B* C*
5) visit D.l EFFECTS A* B* C* D
6) retract to middle of B EFFECTS A* B C D
7) assert first command of B EFFECTS A* B+ C D
8) assert C EFFECTS A* B+ C D [error message]
9) assert B EFFECTS A* B* C D
10) assert D EFFECTS A* B* C D*
11) retract B EFFECTS A* B C D?
12) assert C EFFECTS A* B* C* D?
13) retract B EFFECTS A* B C D?
14) assert B EFFECTS A* B* C D?
15) assert C EFFECTS A* B* C* D?
16) retract to middle of B EFFECTS A* B+ C D?
14) M-x proof-restart-script EFFECTS A B C D
|
