diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-10-18 12:45:03 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-10-18 12:45:03 +0000 |
| commit | b7da9fdb9ad58a645d399a05a1c75b94733302d3 (patch) | |
| tree | 9ca44d6e451aedbb9af78f38648491c0b16484f7 /etc/lego | |
| parent | 94de4a61434e5533ae5e9582b8bd21c2dc6aefa9 (diff) | |
*** empty log message ***
Diffstat (limited to 'etc/lego')
| -rw-r--r-- | etc/lego/multiple/A.l | 1 | ||||
| -rw-r--r-- | etc/lego/multiple/B.l | 4 | ||||
| -rw-r--r-- | etc/lego/multiple/C.l | 1 | ||||
| -rw-r--r-- | etc/lego/multiple/D.l | 1 | ||||
| -rw-r--r-- | etc/lego/multiple/README | 24 |
5 files changed, 31 insertions, 0 deletions
diff --git a/etc/lego/multiple/A.l b/etc/lego/multiple/A.l new file mode 100644 index 00000000..d45f8db8 --- /dev/null +++ b/etc/lego/multiple/A.l @@ -0,0 +1 @@ +Module A;
\ No newline at end of file diff --git a/etc/lego/multiple/B.l b/etc/lego/multiple/B.l new file mode 100644 index 00000000..3a8df7b2 --- /dev/null +++ b/etc/lego/multiple/B.l @@ -0,0 +1,4 @@ +(* B.l Module with a comment *) +Module B; + +[prop = Prop];
\ No newline at end of file diff --git a/etc/lego/multiple/C.l b/etc/lego/multiple/C.l new file mode 100644 index 00000000..5a3afdd6 --- /dev/null +++ b/etc/lego/multiple/C.l @@ -0,0 +1 @@ +Module C Import A B;
\ No newline at end of file diff --git a/etc/lego/multiple/D.l b/etc/lego/multiple/D.l new file mode 100644 index 00000000..b794253b --- /dev/null +++ b/etc/lego/multiple/D.l @@ -0,0 +1 @@ +Module D;
\ No newline at end of file diff --git a/etc/lego/multiple/README b/etc/lego/multiple/README new file mode 100644 index 00000000..37426e61 --- /dev/null +++ b/etc/lego/multiple/README @@ -0,0 +1,24 @@ +Handling of Multiple Files +========================== + + +Test Protocol +------------- + + 1) visit A.l + 2) visit C.l + 3) assert C => all of C should be locked + 4) switch to A.l => all of A should be locked + 5) visit B.l => all of B should be locked + 6) visit D.l => D should not be locked + 7) retract to middle of B => B should be (completely) unlocked + 8) assert first command of B + 9) A should still be locked; C and D should be unlocked +10) assert C => should signal error +11) assert B then D => A,B,D should be locked and C unlocked +12) retract B => A should be locked; B,C should be unlocked + D should be unlocked in systems with linear + dependencies (e.g. LEGO) +13) assert C => A,B,C should be locked; status of D unchanged +14) M-x proof-restart-script => A,B,C,D should be unlocked + |