We don't run the test-suite on windows. Why not?
I would assume the bash scripts look scary, but shouldn't cygwin handle those fine?
probably it broke at some point
https://github.com/coq/coq/pull/12071
3rd commit says
+ dune is rebuilding Coq to run the test-suite, this needs move
investigation.
+ the test suite seems to take long and it times-out on Win.
I'll experiment with windows jobs on the new test-suite then, I suspect it will time out since cygwin is quite slow.
IIRC the reason was that we replaced the azure job which was running the test-suite by the coq-platform job
and that job is supposed to pass --with-test to opam but still it doesn't
Do we even have --with-test set up for the Coq opam file?
So that was an oversight
But Gaetan is correct, that commit was the bug
So it is a mix of the commit plus the removal of the "azure-build.sh" script
OK I created an issue so we don't forget https://github.com/coq/coq/issues/16036
Note that Coq Platform doesn't have a way to pass the --with-test
option to opam, but setting the corresponding opam environment variable OPAMWITHTEST
should work.
I would think that just building Coq with tests should not time out, since we can build the complete platform in CI without tests.
Last updated: Dec 07 2023 at 17:01 UTC