diff options
Diffstat (limited to 'coq/ex/test-cases/multiple-files-single-dir/README')
| -rw-r--r-- | coq/ex/test-cases/multiple-files-single-dir/README | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/coq/ex/test-cases/multiple-files-single-dir/README b/coq/ex/test-cases/multiple-files-single-dir/README new file mode 100644 index 00000000..db1a6a9b --- /dev/null +++ b/coq/ex/test-cases/multiple-files-single-dir/README @@ -0,0 +1,32 @@ +Test multiple file support for the simple case in which all files +are in one directory. + +Dependency graph: + + a.v b.v c.v + \ / \ / + \ / \ / + d.v e.v + \ / + \ / + f.v + +That is, d.v depends on a.v and b.v, and so on. + +Some tests: + +- first visit f.v and display the *Message* buffer in some other + frame +- script f.v and watch the recompilation messages in the + *Message* buffer +- Change now an arbitrary file (either from within emacs or + simply do touch), retract the Require in f.v, and watch the + compilation messages when you assert it again. + +The implementation in Proof General cvs at 2011-01-14 20:03:51 UTC +has an embarrassing bug: Touching b.v causes recompilation of b.v +and d.v but not of e.v! + +Another problem is the following: After a consistent compilation, +change b.v and recompile it outside of Proof General. Then script +f.v -- Proof General will not recompile d and e! |