Hello, I'm trying to use the coq-nix-toolbox on metacoq. This is working extremely well when the CI goes through entirely and pushes all 4 components (template-coq, pcuic, safechecker and erasure) that are part of metacoq, but now I would like to go a bit further and reuse the artifacts of a CI build that fails at some point. To be more concrete, I opened a slightly toy example of a PR on metacoq, and the CI is able to build the first 2 components (template-coq and pcuic) but fails in the 3rd one were my changes happen (no changes were made in the sources of the first 2 components). From what I read in the CI log, the artifacts for the first 2 packages were built and pushed to cachix
Post job cleanup.
Cachix: push
/Users/runner/work/_actions/cachix/cachix-action/v10/dist/main/push-paths.sh /Users/runner/.nix-profile/bin/cachix metacoq
compressing and pushing /nix/store/17kl8msjmzl7630l4nsqsbh0jnhbldc6-coq8.14-metacoq-pcuic-dev (81.33 MiB)
compressing and pushing /nix/store/xcp7gf2077nfmwfhc5avp4bi4ngvmgqn-coq8.14-metacoq-template-coq-dev (71.68 MiB)
All done.
Now I would like to get a hand on these artifacts and start patching my code without having to rebuild them locally.
Just running nix-shell
in my branch (without any specific overlay) does recover a version of template-coq and pcuic from cachix but also starts building safechecker, fails to compile it and does not provide me with an environment were I can start patching things. I tried to play with the --argstr job ...
and --arg override ...
but I couldn't find a magic invocation to help in that case. The closest I could find to a success is nix-shell --arg config '{ attribute = "metacoq-safechecker"; }'
that does not build the safechecker component, but does not provide template-coq and pcuic in the nixEnv either. Moreover, trying to run nix-shell --arg config '{ attribute = "metacoq-safechecker"; }' --run cachedMake
yields
The compilation result is not in cache.
Either it is not in cache (yet) or your must check your cachix configuration.
Is there a way to make this kind of build from a partial CI possible ? ping @Théo Zimmermann @Cyril Cohen that might already have a clue about the nix code for metacoq
Strange... either of --argstr job ...
and --arg config ...
should have worked... I will take a look.
How come that in the CI all the metacoq sub-packages are built in the same CI job instead of being split across multiple ones? Could that be related?
BTW, there is a bug with the search NixOS tool here: https://search.nixos.org/packages?channel=unstable&show=coqPackages.metacoq&from=0&size=50&sort=relevance&type=packages&query=metacoq
The source of the metacoq package points to the Coq build support source instead...
I think that's due to the organisation of the metacoq nix derivation. I followed Cyril's advice to mimick mathcomp's organisation, but I must say that I have trouble to understand what name I should use to refer to the sub-components of metacoq (for instance when using --argstr job ...
)
Yes, I was looking at the source right now and I have some trouble following it as well.
And given that I've no experience on the mathcomp derivation either...
What I can say, however, is that in the case of mathcomp, their CI does have a separate CI job for each sub-package.
This might be because the main-job
that is defined for the CI is mathcomp-ssreflect. See https://github.com/math-comp/math-comp/blob/ea0fb35771d762fee04622a4bf0cafe041022cc2/.nix/config.nix#L44
Something else to note is that they define a shell-attribute
: https://github.com/math-comp/math-comp/blob/ea0fb35771d762fee04622a4bf0cafe041022cc2/.nix/config.nix#L14
I would recommend this in your case as well and in the case of any monorepo (we also do it for hydra-battles: https://github.com/coq-community/hydra-battles/blob/9af8a2b52393813fcee4d8c323426d2bf81d9f84/.nix/config.nix#L14).
This means that typing just nix-shell
should give you an environment where you only have the metacoq dependencies and nothing else.
I will look into this. Currently I mostly kept the default configuration generated by coq-nix-toolbox for the CI with a single default bundle
I don't think I can be of more help than that. If you manage to have a configuration which generates separate CI jobs for each sub-package, you should have more chances for the rest of the stuff to work.
Théo Zimmermann said:
BTW, there is a bug with the search NixOS tool here: https://search.nixos.org/packages?channel=unstable&show=coqPackages.metacoq&from=0&size=50&sort=relevance&type=packages&query=metacoq
The source of the metacoq package points to the Coq build support source instead...
Actually there is exactly the same issue with mathcomp
One thing that I don't understand is that if I load a recent enough version of nixpkgs in nix repl
(through :l <nixpkgs>
) then I can find coqPackages.metacoq
and coqPackages.metacoq.pcuic
(and the same for template-coq, safechecker, and erasure), I can also find coqPackages.mathcomp.algebra
and coqPackages.mathcomp-algebra
however I cannot find the attribute coqPackages.metacoq-pcuic
and I don't see a difference between metacoq's derivation and mathcomp's derivation that could explain the behaviour...
So my main question (probably rather for @Cyril Cohen) is how does mathcomp "magically" generate the attributes for the sub-packages ?
The difference is here: https://github.com/NixOS/nixpkgs/blob/master/pkgs/top-level/coq-packages.nix#L68-L75
I just tried to patch nixpkgs locally and that seems to make the --argstr job metacoq-pcuic
command work correctly. I made a PR on nixpkgs to fix that. Thank you very much for the insights @Cyril Cohen @Théo Zimmermann
Kenji Maillard has marked this topic as resolved.
Last updated: Dec 05 2023 at 04:01 UTC