Stream: MetaCoq

Topic: Nix CI broken?


view this post on Zulip Jason Gross (Mar 01 2023 at 00:25):

I'm seeing
Error: Action failed with error: Error: Unable to locate executable file: cachix. Please verify either the file path exists or the file can be found within a directory specified by the PATH environment variable. Also check the file mode to verify the file is executable.

view this post on Zulip Cyril Cohen (Mar 01 2023 at 14:27):

Yes the nix-install-action needs an upgrade. The issue is fixed in the toolbox.
One needs to run

nix-shell --arg do-nothing true --run "updateNixToolBox & genNixActions"

view this post on Zulip Jason Gross (Mar 02 2023 at 06:22):

Should be fixed by https://github.com/MetaCoq/metacoq/pull/866, but it seems that GH actions is ignoring my changes for pull_request_target actions?

view this post on Zulip Théo Zimmermann (Mar 02 2023 at 09:11):

Yes, it's normal.

view this post on Zulip Théo Zimmermann (Mar 02 2023 at 09:12):

pull_request_target is using the workflow defined in the base branch for security reasons (because it has access to secret variables from the repository). This is why the pull_request event is triggered in addition when there is a change in the workflow (to allow checking how the change to the workflow behave, but without access to the secret variables).

view this post on Zulip Jason Gross (Mar 30 2023 at 06:31):

Why are all the nix CI builds failing with

COQC theories/Typed/Erasure.v
File "./theories/Typed/Erasure.v", line 575, characters 0-15:
Warning: Trying to mask the absolute name "normalization_in"!
[masking-absolute-name,deprecated]
COQC theories/Typed/ErasureCorrectness.v
COQC theories/Typed/Extraction.v
File "./theories/Typed/Extraction.v", line 16, characters 0-58:
Error: Cannot find a physical path bound to logical path
TemplateToPCUIC with prefix MetaCoq.TemplatePCUIC.

make[2]: *** [Makefile.erasure:793: theories/Typed/Extraction.vo] Error 1
make[2]: *** Waiting for unfinished jobs....
make[1]: *** [Makefile.erasure:409: all] Error 2
make[1]: Leaving directory '/build/source/erasure'
make: *** [Makefile:11: theory] Error 2
error: builder for '/nix/store/b1597i39fn0vs8qcksi0ws54ph1ngmrc-coq8.16-metacoq-erasure-dev.drv' failed with exit code 2;
       last 10 log lines:
       > COQC theories/Typed/Extraction.v
       > File "./theories/Typed/Extraction.v", line 16, characters 0-58:
       > Error: Cannot find a physical path bound to logical path
       > TemplateToPCUIC with prefix MetaCoq.TemplatePCUIC.
       >
       > make[2]: *** [Makefile.erasure:793: theories/Typed/Extraction.vo] Error 1
       > make[2]: *** Waiting for unfinished jobs....
       > make[1]: *** [Makefile.erasure:409: all] Error 2
       > make[1]: Leaving directory '/build/source/erasure'
       > make: *** [Makefile:11: theory] Error 2

even though coq-8.16 succeeds?

view this post on Zulip Matthieu Sozeau (Mar 30 2023 at 08:15):

@Kenji Maillard

view this post on Zulip Kenji Maillard (Mar 30 2023 at 17:23):

I'm not sure of what could be happening exactly (and I don't have much time to investigate right now) but it seems that the coq-nix-toolbox version was not updated in a long time (I pushed a newer version on this PR but It did not get merged yet)

view this post on Zulip Jason Gross (Mar 30 2023 at 21:18):

@Kenji Maillard That PR is about master, I'm talking about PRs on the coq-8.16 branch. The coq-nix-toolbox version has been updated, but even, e.g., #883 which just adds Set Polymorphic Inductive Cumulativity. in one place is failing with

COQC theories/Typed/Extraction.v
File "./theories/Typed/Extraction.v", line 16, characters 0-58:
Error: Cannot find a physical path bound to logical path
TemplateToPCUIC with prefix MetaCoq.TemplatePCUIC.

Presumably this is because the nix CI jobs are in the wrong order (template-pcuic comes after erasure), and presumably this isn't caught because the nix jobs don't run on the head of coq-8.16... Ah, and maybe this doesn't work on https://github.com/MetaCoq/metacoq/pull/877 because PRs use the base branch version of the action, rather than the PR version, and maybe once https://github.com/MetaCoq/metacoq/pull/877 is merged the CI will work again?

view this post on Zulip Jason Gross (Mar 30 2023 at 21:18):

Also, it it deliberate that nix doesn't run on the coq-8.16 branch?

view this post on Zulip Jason Gross (Mar 30 2023 at 21:37):

Yeah, I think we just need someone to merge https://github.com/MetaCoq/metacoq/pull/877

view this post on Zulip Jason Gross (Mar 31 2023 at 18:31):

Could someone merge #877? It reorders the jobs on nix CI, and I don't think there's any way to test it without merging it, so we don't expect the CI to pass on the PR.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2023 at 21:13):

Done, in order not to lose time.

view this post on Zulip Jason Gross (Apr 01 2023 at 02:10):

Thank you. Unfortunately, that doesn't seem to fix the issue. I'm baffled as to why NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" --argstr job "metacoq-template-pcuic" is literally a no-op at https://github.com/MetaCoq/metacoq/actions/runs/4579266410/jobs/8087116554?pr=879#step:14:1. Can someone who understands the nix setup explain what's going on here?

view this post on Zulip Jason Gross (Apr 02 2023 at 19:51):

New hypothesis: maybe the nix cache is invalid? Does https://github.com/NixOS/nixpkgs/blob/master/pkgs/top-level/coq-packages.nix have to be updated with new packages or something? How is the nix CI supposed to work? (cc @nicolas tabareau @Kenji Maillard ? )

view this post on Zulip Jason Gross (Apr 02 2023 at 19:55):

Does the list of packages at https://github.com/NixOS/nixpkgs/blob/a5f21729595f01a2de196ed9fb9cc0d18e0b8c88/pkgs/development/coq-modules/metacoq/default.nix#L31 need to be updated? Or overridden somehow?

view this post on Zulip Jason Gross (Apr 02 2023 at 19:56):

It does look like the packages not listed there aren't getting built at all...

view this post on Zulip Jason Gross (Apr 02 2023 at 19:58):

Ah, maybe updating .nix/coq-overlays/metacoq/default.nix will fix things? I've made https://github.com/MetaCoq/metacoq/pull/891, fingers crossed

view this post on Zulip Kenji Maillard (Apr 02 2023 at 20:20):

Jason Gross said:

Does the list of packages at https://github.com/NixOS/nixpkgs/blob/a5f21729595f01a2de196ed9fb9cc0d18e0b8c88/pkgs/development/coq-modules/metacoq/default.nix#L31 need to be updated? Or overridden somehow?

I don't understand much about how nix packages are working, but I think this file should be updated as the global default for releases. For the local tweaks while developing, I think the overlay you modified is indeed the way to go (but the coq-nix-toolbox repo is probably the best place for informations on that question)

view this post on Zulip Jason Gross (Apr 02 2023 at 22:19):

Success! https://github.com/MetaCoq/metacoq/pull/891 has passed CI, and can be merged. (And if someone could merge it shortly, I'd appreciate that, and then my other PRs should be mostly ready for review)

view this post on Zulip Yannick Forster (Apr 03 2023 at 04:18):

Done!

view this post on Zulip Jason Gross (Apr 03 2023 at 06:40):

Thank you!


Last updated: Jun 13 2024 at 03:02 UTC