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
|
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]
BROKEN 11.12.98: B.ML *may* not be locked?
16) retract to middle of B EFFECTS A* B+ C D?
BROKEN! Now retracts whole thing.
14) M-x proof-shell-restart 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)
-----------------------------------------------------------------
Question:
We assert script A.
We assert script B.
Can we retract to middle of A? Yes, we should be able to!
-----------------------------------------------------------------
Tester:
Visit A.ML. Assert partly.
Visit C.thy. Assert it.
This should lock remainder of A.ML, since it has now been read
completely.
|
