diff options
Diffstat (limited to 'coq/ex/test-cases/multiple-files-multiple-dir')
5 files changed, 55 insertions, 0 deletions
diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/README b/coq/ex/test-cases/multiple-files-multiple-dir/README new file mode 100644 index 00000000..82c7fc2a --- /dev/null +++ b/coq/ex/test-cases/multiple-files-multiple-dir/README @@ -0,0 +1,23 @@ +Test multiple file support when files are distributed over +different directories. + +Dependency graph + + a/a.v + \ + \ + b/b1.v --- b/b2.v + \ + \ + c/c.v + +That is, c depends on b2, which depends on b1, which depends on +a. + +Script c.v and watch the compilation messages in *Messages*. +Touch any file and retract and assert the Require in c. + +The bugs described in ../multiple-files-single-dir/README can +also be reproduced here. + + diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/a/a.v b/coq/ex/test-cases/multiple-files-multiple-dir/a/a.v new file mode 100644 index 00000000..e4dadf39 --- /dev/null +++ b/coq/ex/test-cases/multiple-files-multiple-dir/a/a.v @@ -0,0 +1,3 @@ +(* this file depends on nothing *) + +Definition a := 0.
\ No newline at end of file diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/b/b1.v b/coq/ex/test-cases/multiple-files-multiple-dir/b/b1.v new file mode 100644 index 00000000..afcd3941 --- /dev/null +++ b/coq/ex/test-cases/multiple-files-multiple-dir/b/b1.v @@ -0,0 +1,9 @@ +(* this file depends on ../a/a.v *) + +Definition a := 1. + +Require a. + +(*** Local Variables: ***) +(*** coq-load-path: ("../a") ***) +(*** End: ***) diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/b/b2.v b/coq/ex/test-cases/multiple-files-multiple-dir/b/b2.v new file mode 100644 index 00000000..6d79572a --- /dev/null +++ b/coq/ex/test-cases/multiple-files-multiple-dir/b/b2.v @@ -0,0 +1,9 @@ +(* this file depends on b1 and therefore indirectly on ../a/a.v *) + +Definition a := 2. + +Require b1. + +(*** Local Variables: ***) +(*** coq-load-path: ("../a") ***) +(*** End: ***) diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/c/c.v b/coq/ex/test-cases/multiple-files-multiple-dir/c/c.v new file mode 100644 index 00000000..5171340c --- /dev/null +++ b/coq/ex/test-cases/multiple-files-multiple-dir/c/c.v @@ -0,0 +1,11 @@ +(* this file depends on ../b/b2 and therefore indirectly + * on ../b/b1 and ../a/a.v + *) + +Definition a := 2. + +Require b2. + +(*** Local Variables: ***) +(*** coq-load-path: ("../a" "../b") ***) +(*** End: ***) |