Stream: Coq devs & plugin devs

Topic: CI policy after full Dune switch


view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 14:40):

@Théo Zimmermann @Gaëtan Gilbert @Ali Caglayan , https://github.com/coq/coq/pull/15560 is mostly ready now, except for a few choices to make regarding our CI policy.

In particular, we need to figure out what kind of testing matrix we have for the Coq build. The main parameters we have to choose are:

I guess for the first one, we can just do a developer build with check, maybe for 32+bits too as it is faster. WDYT?

For the artifact I guess it depends on whether we want to test installed Coq or built Coq. Keeping _build is nice for some cases, for example the new test-suite mode really wants to work this way; but maybe it'd be worth just to run it from a zero build? Also the docs may require stuff from _build

Otherwise _build doesn't provide a lot of advantages unless a) depending jobs depend on dune and b) we can expose a cache to the workers.

So I dunno, let me know what you think, I guess I'll be pretty conservative for this update of the PR.

view this post on Zulip Théo Zimmermann (Apr 29 2022 at 14:42):

What are the advantages of testing a release build? Is there a risk of not catching something by doing a developer build?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 14:43):

A release build is like using -O 2 etc...

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 14:43):

developer build has more warnings, and builds faster

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 14:43):

"release" build enables all the optimizations, so it is clear to me, for CI main jobs that's what we should use

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 14:43):

test-suite, doc, etc... are more subtle

view this post on Zulip Théo Zimmermann (Apr 29 2022 at 14:44):

If the release build could bring some performance when building the Coq projects, then yes, it is likely to be what we need. For this one, we could cache the _install_ci. For the rest of the jobs, we would use a developer build and cache _build

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 14:56):

Ok, current code is that way.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 14:56):

almost

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 14:56):

:)

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 14:57):

I'm also thinking of dropping the doc install targets, in the sense that they are a simple cp -a for now

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 14:57):

tho newer dune should be able to handle those fine, I think

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 14:58):

but in the makefile, I'm not sure they are useful

view this post on Zulip Théo Zimmermann (Apr 29 2022 at 15:08):

How would a packager do (though I don't know if anyone packages Coq's documentation at the moment)? Replicate the cp commands?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 15:08):

Yes, like deploy ci job does

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 15:08):

I mean, we can add the targets, but they are a simple copy

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 15:09):

stdlib docs should be handled in coq.theory tho

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 15:10):

so we are really only talking about Sphinx, after the PR make refman will put the docs in _build/default/doc/refman-html

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 15:10):

so maybe indeed we can just install them with coq-doc

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 15:10):

but that will require bumping the minimum dune version

view this post on Zulip Théo Zimmermann (Apr 29 2022 at 15:16):

I'm fine with any solution, as long as we properly document it.

view this post on Zulip Guillaume Melquiond (Apr 29 2022 at 15:23):

Théo Zimmermann said:

I don't know if anyone packages Coq's documentation at the moment

Given this bug report https://github.com/coq/coq/issues/15956, at least Fedora does.

view this post on Zulip Gaëtan Gilbert (Apr 29 2022 at 15:25):

Emilio Jesús Gallego Arias said:

I mean, we can add the targets, but they are a simple copy

I think we should still have the targets even if the implementation looks simple

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 15:30):

@Gaëtan Gilbert but there are not tested anywhere

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 15:30):

so what's the point

view this post on Zulip Gaëtan Gilbert (Apr 29 2022 at 15:35):

shouldn't we test them then?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 15:36):

what's the point of testing a directory copy?

view this post on Zulip Emilio Jesús Gallego Arias (Apr 29 2022 at 15:36):

We deploy directly from the doc build dir

view this post on Zulip Gaëtan Gilbert (Apr 29 2022 at 15:46):

you may be right


Last updated: Feb 06 2023 at 00:03 UTC