@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:
_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.
What are the advantages of testing a release build? Is there a risk of not catching something by doing a developer build?
A release build is like using -O 2 etc...
developer build has more warnings, and builds faster
"release" build enables all the optimizations, so it is clear to me, for CI main jobs that's what we should use
test-suite, doc, etc... are more subtle
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
Ok, current code is that way.
almost
:)
I'm also thinking of dropping the doc install targets, in the sense that they are a simple cp -a
for now
tho newer dune should be able to handle those fine, I think
but in the makefile, I'm not sure they are useful
How would a packager do (though I don't know if anyone packages Coq's documentation at the moment)? Replicate the cp
commands?
Yes, like deploy ci job does
I mean, we can add the targets, but they are a simple copy
stdlib docs should be handled in coq.theory tho
so we are really only talking about Sphinx, after the PR make refman
will put the docs in _build/default/doc/refman-html
so maybe indeed we can just install them with coq-doc
but that will require bumping the minimum dune version
I'm fine with any solution, as long as we properly document it.
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.
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
@Gaëtan Gilbert but there are not tested anywhere
so what's the point
shouldn't we test them then?
what's the point of testing a directory copy?
We deploy directly from the doc build dir
you may be right
Last updated: Oct 13 2024 at 01:02 UTC