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
|
Test files for multiple file handling with Isabelle.
Test schedule
=============
[C depends on A and B, D is independent]
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
Borrowed from Thomas's lego tests: (v 1.2)
1) visit A.ML EFFECTS A
2) visit C.ML EFFECTS A C
3) assert C EFFECTS A* C*
4) visit B.ML,B.thy,C.thy EFFECTS A* B* C* C.thy* B.thy*
5) visit D.ML,D.thy EFFECTS A* B* C* D D.thy
6) retract to middle of B EFFECTS A* B C D B.thy* (*thy remains locked*)
7) assert first command of B EFFECTS A* B+ C D
8) assert C EFFECTS A* B+ C D [error message, correctly]
9) assert B EFFECTS A* B* C D
10) assert D EFFECTS A* B* C D* D.thy*
11) retract B EFFECTS A* B C D? [D* D.thy* for Isabelle]
12) assert C EFFECTS A* B* C* D?
13) retract B EFFECTS A* B C D? [B.thy* D*,D.thy* again]
14) assert B EFFECTS A* B* C D?
15) assert C EFFECTS A* B* C* D? [everything locked]
16) retract to middle of B EFFECTS A* B+ C D?
BROKEN! Now retracts whole thing.
14) M-x proof-restart-script EFFECTS A B C D
MORE TESTS NEEDED FOR ISABELLE:
===============================
Should test assertion of theory files, and watch what happens to ML files.
Because of theory loader's odd behaviour, must watch what happens
to ML files of autoloaded children.
1) visit example.ML, example.thy EFFECT: ML thy
2) assert .ML EFFECT: ML* thy*
3) retract thy EFFECT: ML thy
1) visit example.ML, example.thy ML thy
2) assert thy ML* thy* (reads theory too)
(* Test case for outdating a child theory *)
1) assert C.thy A*, B*, C*
2) retract B.thy A*
3) edit B.thy to touch timestamp
4) assert B.thy A*, B*, C Message: "C out of date"
5) assert C.thy A*, B*, C*
(* Test case for removing a dependency from a theory:
this automatically unlocks the orphaned theory,
is this right??
*)
1) assert C.thy A*, B*, C*
2) retract C.thy A*, B*, C
3) edit C.thy to C=A, remove dependency on B
4) assert C.thy A*, B, C* (B automatically unlocked)
|
