Stream: Nix toolbox devs & users

Topic: ✔ Using coq-nix-toolbox with partial CI


view this post on Zulip 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

view this post on Zulip Cyril Cohen (Sep 06 2022 at 10:21):

Strange... either of --argstr job ... and --arg config ... should have worked... I will take a look.

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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 ...)

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Sep 06 2022 at 11:33):

And given that I've no experience on the mathcomp derivation either...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Notification Bot (Sep 19 2022 at 09:29):

Kenji Maillard has marked this topic as resolved.


Last updated: Dec 05 2023 at 04:01 UTC