Stream: Coq devs & plugin devs

Topic: Test-suite on windows


view this post on Zulip Ali Caglayan (May 18 2022 at 12:53):

We don't run the test-suite on windows. Why not?

view this post on Zulip Ali Caglayan (May 18 2022 at 12:53):

I would assume the bash scripts look scary, but shouldn't cygwin handle those fine?

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 12:54):

probably it broke at some point

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 12:57):

https://github.com/coq/coq/pull/12071

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 12:57):

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.

view this post on Zulip Ali Caglayan (May 18 2022 at 13:01):

I'll experiment with windows jobs on the new test-suite then, I suspect it will time out since cygwin is quite slow.

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2022 at 13:02):

IIRC the reason was that we replaced the azure job which was running the test-suite by the coq-platform job

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2022 at 13:02):

and that job is supposed to pass --with-test to opam but still it doesn't

view this post on Zulip Ali Caglayan (May 18 2022 at 13:03):

Do we even have --with-test set up for the Coq opam file?

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2022 at 13:04):

See https://github.com/coq/coq/pull/12425/files#diff-34a36af65fe6793c9d83dce66c4e0517913b0818b07c14a80102d6395aeb4a4f

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2022 at 13:04):

So that was an oversight

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2022 at 13:08):

But Gaetan is correct, that commit was the bug

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2022 at 13:09):

So it is a mix of the commit plus the removal of the "azure-build.sh" script

view this post on Zulip Ali Caglayan (May 18 2022 at 13:11):

OK I created an issue so we don't forget https://github.com/coq/coq/issues/16036

view this post on Zulip Michael Soegtrop (May 19 2022 at 08:00):

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.

view this post on Zulip Michael Soegtrop (May 19 2022 at 08:01):

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