Kenji Maillard (Sep 06 2022 at 08:31): Kenji Maillard (Sep 06 2022 at 08:31):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
Cyril Cohen (Sep 06 2022 at 10:21):Strange... either of --argstr job ... and --arg config ... should have worked... I will take a look.
Théo Zimmermann (Sep 06 2022 at 11:24):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?
Théo Zimmermann (Sep 06 2022 at 11:31):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...
Kenji Maillard (Sep 06 2022 at 11:32):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 ...)
Théo Zimmermann (Sep 06 2022 at 11:33):Yes, I was looking at the source right now and I have some trouble following it as well.
Théo Zimmermann (Sep 06 2022 at 11:33):And given that I've no experience on the mathcomp derivation either...
Théo Zimmermann (Sep 06 2022 at 11:35):What I can say, however, is that in the case of mathcomp, their CI does have a separate CI job for each sub-package.
Théo Zimmermann (Sep 06 2022 at 11:36):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
Théo Zimmermann (Sep 06 2022 at 11:38):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).
Théo Zimmermann (Sep 06 2022 at 11:38):This means that typing just nix-shell should give you an environment where you only have the metacoq dependencies and nothing else.
Kenji Maillard (Sep 06 2022 at 11:39):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
Théo Zimmermann (Sep 06 2022 at 11:40):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.
Kenji Maillard (Sep 06 2022 at 11:44):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
Kenji Maillard (Sep 06 2022 at 13:13):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...
Kenji Maillard (Sep 06 2022 at 13:14):So my main question (probably rather for @Cyril Cohen) is how does mathcomp "magically" generate the attributes for the sub-packages ?
Cyril Cohen (Sep 06 2022 at 13:45):The difference is here: https://github.com/NixOS/nixpkgs/blob/master/pkgs/top-level/coq-packages.nix#L68-L75
Kenji Maillard (Sep 06 2022 at 14:14):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
Notification Bot (Sep 19 2022 at 09:29):Kenji Maillard has marked this topic as resolved.
Last updated: Jun 10 2023 at 23:01 UTC