diff options
| author | Hendrik Tews | 2021-01-01 22:56:48 +0100 |
|---|---|---|
| committer | hendriktews | 2021-01-10 20:59:43 +0100 |
| commit | 0d731606bee81b2d73895a23b69e84796ea7e4e7 (patch) | |
| tree | 2df103ffc973c9728a866d27ab3ea325f178658e /ci/compile-tests/README.md | |
| parent | 2d94aa0aabf0aa7087f8833e1c61d95a034e2d13 (diff) | |
add Coq compile test for a delayed require
Diffstat (limited to 'ci/compile-tests/README.md')
| -rw-r--r-- | ci/compile-tests/README.md | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/ci/compile-tests/README.md b/ci/compile-tests/README.md new file mode 100644 index 00000000..3b0364e2 --- /dev/null +++ b/ci/compile-tests/README.md @@ -0,0 +1,18 @@ +This directory contains tests for the parallel background +compilation feature for Coq. The test check that +- files get compiled in the right order, +- after changes, precisely those files that need recompilation + are compiled +- files are locked and registered in the right require commands. + + +Tests currently missing: +- unlock checks for ancestors of failed jobs in different cases +- a job depending on a failed dependee, where the dependee has + been finished before +- coq-par-create-file-job detects a dependency cycle +- coq-par-create-file-job finds a job in state waiting-dep +- coq-par-kickoff-queue-maybe is done when the queue dependee is + in state waiting-queue +- coq-par-create-file-job finds a failed job +- all tests in all quick and all vos variants |