compile-tests/003-require-error fails sporadically with 8.19-rc1

[hendriktews]

compile-tests/003-require-error fails sporadically with 8.19-rc1

[hendriktews]

The coqdep warning on a missing module has changed such that PG does not recognize the coqdep error any more. coq-coqdep-error-regexp needs to be adapted.

[hendriktews]

Because of the unrecognized coqdep error on Require X c, PG proceeds as if this line did not require any compilation. In the failing runs, compilation of b.v (caused by the first require command) finishes first, such that the first two require commands are sent to coqtop. coqtop produces an error because of the missing X or c, such that PG aborts all background compilation, which kill compilation of c and removes c.vo. cct-file-newer "c.vo" then fails because c.vo does not exist.
In the passing runs, coqdep on the third require line finishes first, such that compilation of c.v is started and completes before the first or second require is processed by coqtop. Then c.vo exists and the test succeeds.

[hendriktews]

What is really missing is a test that coqdep errors on missing modules are reliably recognized.