Conversation
Note that Docker CI no longer works for Rocq 9.1 because there is no compatible rerease of Paramcoq.
.nix/config.nix
Outdated
| bundles = | ||
| let rocq-constraints = { | ||
| "9.0" = { | ||
| coqPackages.paramcoq.override.version = "v1.1.3+coq9.0"; | ||
| }; | ||
| "9.1" = { | ||
| coqPackages.paramcoq.override.version = | ||
| "937537d416bc5f7b81937d4223d7783d0e687239"; | ||
| }; | ||
| }; | ||
| mc-constraints = { | ||
| "master" = { | ||
| coqPackages.mathcomp-zify.override.version = "master"; | ||
| }; | ||
| }; | ||
| matrix = { | ||
| ## The combinations of Rocq and MathComp we test | ||
| "8.19" = ["2.3.0"]; | ||
| "8.20" = ["2.3.0" "2.4.0" "2.5.0"]; | ||
| "9.0" = ["2.4.0" "2.5.0" "master"]; | ||
| "9.1" = ["2.4.0" "2.5.0" "master"]; | ||
| }; in | ||
| attrsets.concatMapAttrs (rocq: mcs: listToAttrs (map (mc: { | ||
| name = "${rocq}-${mc}"; | ||
| value = { | ||
| coqPackages.coq.override.version = rocq; | ||
| coqPackages.mathcomp.override.version = mc; | ||
| } // (attrByPath [rocq] {} rocq-constraints) | ||
| // (attrByPath [mc] {} mc-constraints); | ||
| }) mcs)) matrix; |
There was a problem hiding this comment.
@proux01 Here is my attempt to refactor "bundles", but it looks like I don't understand the semantics of //...
There was a problem hiding this comment.
I'm still unsure if what I wrote is very idiomatic and easy to understand. Any suggestions?
pi8027
force-pushed
the
ci
branch
3 times, most recently
from
1d066b1 to
9637497
Compare
|
The Nix CI does not seem to correctly handle the dependency from stablesort to MathComp, and MathComp gets compiled twice for each bundle. Also, I probably need only |
|
The issues I observed:
By the way, the dependency from |
|
The bundles "9.1-*" are not working. If I understand correctly, they attempt to build the "coq-9.1.0" package in the environment where "rocq-9.0.1" is already installed and then fail. |
|
@pi8027 please ignore the dependencies from |
looks like you are right |
| stablesort: | ||
| needs: | ||
| - coq | ||
| - paramcoq |
There was a problem hiding this comment.
Is it normal that mathcomp-ssreflect and paramcoq do not appear here? I thought needs should list all the dependencies.
| inherit version; | ||
| propagatedBuildInputs = [ mathcomp.ssreflect paramcoq mathcomp-zify equations ]; | ||
| propagatedBuildInputs = [ mathcomp-ssreflect paramcoq mathcomp-zify equations ]; | ||
| } |
There was a problem hiding this comment.
I think I recovered the dependency from stablesort to mathcomp-ssreflect by replacing . with - here. What is the difference?
pi8027
force-pushed
the
ci
branch
2 times, most recently
from
d2b195a to
92350e3
Compare
.nix/config.nix
Outdated
| rocqPackages = | ||
| (if compareVersions "9.0.0" rocq <= 0 || rocq == "master" then | ||
| { rocq-core.override.version = rocq; } else {}) | ||
| // rocq-bundles.${rocq}.rocqPackages or {} | ||
| // mc-bundles.${mc}.rocqPackages or {}; |
There was a problem hiding this comment.
Apparently, coqPackages.coq.override.version was not enough to avoid installing different versions of Coq and Rocq, and I had to add this. This is perhaps a bug of the coq compatibility package in Nix.
.nix/config.nix
Outdated
| paramcoq.job = true; | ||
| equations.job = true; } | ||
| // rocq-bundles.${rocq}.coqPackages or {} | ||
| // mc-bundles.${mc}.coqPackages or {}; }; |
There was a problem hiding this comment.
One pitfall I had was that // did not merge attribute sets recursively. For example,
{ a.b = 1; } // { a.c = 2; }evaluates to { a.c = 2; }, not { a.b = 1; a.c = 2; }.
While I think this behavior is reasonable, I need to merge rocqPackages and coqPackages separately here. Is there a more concise way of doing this?
So should I replace |
|
I replaced |
|
I'm reverting the change since it looks pretty broken. |
3 participants
No description provided.