diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-10-29 18:26:45 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-10-29 18:26:45 +0000 |
| commit | 98a7850c2c60a6da95dff5724437aa7d6fc6d1d4 (patch) | |
| tree | 72105929c59930ab5b1bc00972343f0695b0ca44 /etc/isa/multiple | |
| parent | e893685f06bbc7d8a99d2a2b993712728d6960a8 (diff) | |
Ran tests for Isabelle. Added another test case.
Diffstat (limited to 'etc/isa/multiple')
| -rw-r--r-- | etc/isa/multiple/README | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/etc/isa/multiple/README b/etc/isa/multiple/README index 4c389120..4cd5aa71 100644 --- a/etc/isa/multiple/README +++ b/etc/isa/multiple/README @@ -1 +1,52 @@ 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 +2) assert .ML EFFECT: ML* thy* +3) retract thy EFFECT: ML thy (29.10.98 BREAKS!) + get ML* + + + + |