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.
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"
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?
Yes, it's normal.
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).
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?
@Kenji Maillard
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)
@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?
Also, it it deliberate that nix doesn't run on the coq-8.16 branch?
Yeah, I think we just need someone to merge https://github.com/MetaCoq/metacoq/pull/877
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.
Done, in order not to lose time.
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?
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 ? )
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?
It does look like the packages not listed there aren't getting built at all...
Ah, maybe updating .nix/coq-overlays/metacoq/default.nix will fix things? I've made https://github.com/MetaCoq/metacoq/pull/891, fingers crossed
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)
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)
Done!
Thank you!
Last updated: Oct 13 2024 at 01:02 UTC