blob: 0ea75fcc385412b2c2b816f34539b4b7f0ccb6d4 (
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
|
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 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?
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 (29.10.98 BREAKS!)
get ML*
1) visit example.ML, example.thy ML thy
2) assert thy ML thy* (29.10.98: works, but
example.ML is on included
files list: Isabelle problem)
|
