Conversation
pi8027
force-pushed
the
ci
branch
7 times, most recently
from
b88ad80 to
c479551
Compare
pi8027
requested review from
CohenCyril and
proux01
and removed request for
proux01
|
Nix CI is still a bit broken but probably better than before. |
| ## Set this when the package has no rocqPackages version yet | ||
| ## (either in nixpkgs or in .nix/rocq-overlays) | ||
| no-rocq-yet = true; |
There was a problem hiding this comment.
To be removed now that finmap is in rocqPackages
There was a problem hiding this comment.
Removing no-rocq-yet = true; rather seems to break mathcomp-finmap in "Nix CI for bundle master".
.nix/config.nix
Outdated
| "9.0".coqPackages = common-bundles // { | ||
| coq.override.version = "9.0"; | ||
| }; | ||
| "9.1".coqPackages = common-bundles // { | ||
| coq.override.version = "9.1"; | ||
| }; |
There was a problem hiding this comment.
These also need a rocq-core override (c.f., the config.nix file in mathcomp)
.nix/config.nix
Outdated
| mathcomp.override.version = "master"; | ||
| mathcomp-boot.override.version = "master"; |
There was a problem hiding this comment.
We should keep mathcomp here (otherwise only mathcomp-boot = mathcomp.boot will be overriden)
There was a problem hiding this comment.
I reverted the change. But the generated Nix CI lacks many dependencies, and it looks like we build the entire MathComp for nothing: https://github.com/math-comp/finmap/actions/runs/22440228038?pr=151
There was a problem hiding this comment.
If I list mathcomp-boot,..., mathcomp-algebra here, do you think it works better?
There was a problem hiding this comment.
If I list
mathcomp-boot,...,mathcomp-algebrahere, do you think it works better?
I made a separate commit for this change to see what happens.
There was a problem hiding this comment.
Should I also add these lines to rocqPackages?
.nix/config.nix
Outdated
| rocq-elpi.override.elpi-version = "2.0.7"; | ||
| rocq-elpi.override.elpi-version = "3.4.2"; | ||
| hierarchy-builder.override.version = "master"; | ||
| stdlib.override.version = "master"; |
There was a problem hiding this comment.
Perhaps we can remove this line, and the same applies to rocqPackages.stdlib below.
|
And now |
|
(Also, feel free to amend my changes and proceed without me. I just wanted to test #144 properly.) |
|
It looks like I managed to fix Nix CI after making several dumb attempts. Dependencies are still broken, and we probably build a few packages several times in CI (which is wasteful), but this issue should probably be fixed in nixpkgs. We can squash the Nix-related commits, and I think we are good to go. |
|
Yes, dependencies can sometime seem a bit broken. Playing with |
|
Thanks for the suggestion. Shall we squash and merge this PR, and optimise further in another PR when we have more time and energy? |
|
Sure, let's merge |
|
Thanks! |
2 participants
Closes #148