Skip to content

Conversation

@Alizter
Copy link
Collaborator

@Alizter Alizter commented Sep 19, 2025

No description provided.

Signed-off-by: Ali Caglayan <[email protected]>
@Alizter Alizter marked this pull request as ready for review September 19, 2025 20:57
@Alizter
Copy link
Collaborator Author

Alizter commented Sep 19, 2025

Used in CI and local development. Works for me so merging.

@Alizter Alizter merged commit 228f8f3 into HoTT:master Sep 19, 2025
22 checks passed
@Alizter Alizter deleted the push-kzzoywotyzlm branch September 19, 2025 20:57
@jdchristensen
Copy link
Collaborator

@Alizter Did this change the nix job in the CI to build with 9.0 instead of 8.20? If so, I think that's good, so that we get some coverage of 9.0, but it's also good if the PR and the commit message indicate the change.

(Incidentally, it's often very hard to figure out which version of Coq our CI jobs use when looking at their output. Would it be hard to get them to output this clearly, somewhere near the beginning? Or at the start of the building of the Coq-HoTT library?)

@Alizter
Copy link
Collaborator Author

Alizter commented Sep 20, 2025

@jdchristensen This uses 9.0 in the nix job, but I will follow up with a PR overhauling our CI to make it easier to track versions and update various things.

Adding a version dump in the build script sounds like a good idea.

It took me longer than usual because the docker images for 9.0 don't include comparability shims with Coq so coq_makefile has to be conditionally replaced with rocq makefile etc. All very boring and mundane work unfortunately.

@jdchristensen
Copy link
Collaborator

Currently we have opam-build, quick-build and build, and for each of those we build against three versions of Coq. And in addition we have nix building against one version of Coq. I wonder if we should only do some of those builds. E.g. opam-build could build against v1, v2 and v4 of Coq, quick-build could build against v3 and v4, while build could be against v2 and v4, while nix is against v3. (I'm just making this up, but the idea is that we mix and match, rather than doing the full cartesian product of the sets.) OTOH, the builds run in parallel, so it doesn't waste much wall time, just github resources.

I also wondered about doing one build really fast, with more cores, before doing any others. Then when you pushed something faulty, you'd find out very quickly (ideally in < 1 minute), and we wouldn't waste cpu time trying all of the other build variants.

Just some random thoughts, since you are adjusting things.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants