Stream: Coq devs & plugin devs

Topic: CI policy after full Dune switch

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:

• build Coq in release mode vs developer mode?
• output as artifact _install_ci or _build

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.

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?

Emilio Jesús Gallego Arias (Apr 29 2022 at 14:43):

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

Emilio Jesús Gallego Arias (Apr 29 2022 at 14:43):

developer build has more warnings, and builds faster

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

Emilio Jesús Gallego Arias (Apr 29 2022 at 14:43):

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

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

Emilio Jesús Gallego Arias (Apr 29 2022 at 14:56):

Ok, current code is that way.

Emilio Jesús Gallego Arias (Apr 29 2022 at 14:56):

almost

Emilio Jesús Gallego Arias (Apr 29 2022 at 14:56):

:)

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

Emilio Jesús Gallego Arias (Apr 29 2022 at 14:57):

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

Emilio Jesús Gallego Arias (Apr 29 2022 at 14:58):

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

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?

Emilio Jesús Gallego Arias (Apr 29 2022 at 15:08):

Yes, like deploy ci job does

Emilio Jesús Gallego Arias (Apr 29 2022 at 15:08):

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

Emilio Jesús Gallego Arias (Apr 29 2022 at 15:09):

stdlib docs should be handled in coq.theory tho

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

Emilio Jesús Gallego Arias (Apr 29 2022 at 15:10):

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

Emilio Jesús Gallego Arias (Apr 29 2022 at 15:10):

but that will require bumping the minimum dune version

Théo Zimmermann (Apr 29 2022 at 15:16):

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

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.

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

Emilio Jesús Gallego Arias (Apr 29 2022 at 15:30):

@Gaëtan Gilbert but there are not tested anywhere

Emilio Jesús Gallego Arias (Apr 29 2022 at 15:30):

so what's the point

Gaëtan Gilbert (Apr 29 2022 at 15:35):

shouldn't we test them then?

Emilio Jesús Gallego Arias (Apr 29 2022 at 15:36):

what's the point of testing a directory copy?

Emilio Jesús Gallego Arias (Apr 29 2022 at 15:36):

We deploy directly from the doc build dir

Gaëtan Gilbert (Apr 29 2022 at 15:46):

you may be right

Last updated: Apr 19 2024 at 08:01 UTC