The Nix CI is broken for Lean v4.22.0

Stream: lean4 dev

[Leni Aniva]

Is there any plans to fix it? When I ran nix build .#packages.x86_64-linux.cacheRoots, I got

evaluation warning: The Nix-based build is deprecated
error:
       … while calling the 'derivationStrict' builtin
         at <nix/derivation-internal.nix>:37:12:
           36|
           37|   strict = derivationStrict drvAttrs;
             |            ^
           38|

       … while evaluating derivation 'cacheRoots'
         whose name attribute is located at /nix/store/5w65kvkmrdqv006ci2f5p80s0yghld1i-source/pkgs/stdenv/generic/make-derivation.nix:438:13

       … while evaluating attribute 'buildCommand' of derivation 'cacheRoots'
         at /nix/store/5w65kvkmrdqv006ci2f5p80s0yghld1i-source/pkgs/build-support/trivial-builders/default.nix:80:17:
           79|         enableParallelBuilding = true;
           80|         inherit buildCommand name;
             |                 ^
           81|         passAsFile = [ "buildCommand" ] ++ (derivationArgs.passAsFile or [ ]);

       (stack trace truncated; use '--show-trace' to show the full, detailed trace)

       error: attribute 'result' missing
       at /nix/store/iq0dbcl0rzdkasrcxwbgk3gp1sr21cpq-source/nix/buildLeanPackage.nix:209:119:
          208|     startSet = map (m: { key = m; }) (concatMap expandGlob roots);
          209|     operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.result.imports) else [];
             |                                                                                                                       ^
          210|   }));

[Leni Aniva]

The fix is pretty easy. it's just a one-line change

[Leni Aniva]

https://github.com/leanprover/lean4/pull/9905

[Leni Aniva]

The entire Nix build got deleted. Now lean4-nix is on its own.

[Alex Keizer]

Leni Aniva said:

The entire Nix build got deleted. Now lean4-nix is on its own.

I rely on nix develop when hacking on the Lean core, does this mean that's now gone or are you just talking about a CI build being deleted?

[Leni Aniva]

Alex Keizer said:

Leni Aniva said:

The entire Nix build got deleted. Now lean4-nix is on its own.

I rely on nix develop when hacking on the Lean core, does this mean that's now gone or are you just talking about a CI build being deleted?

I'm just talking about the CI build. The dev shells will still work

[Alex Keizer]

Thanks for clarifying!

[Eric Wieser]

The dev shells will still work

Even without lean4#9905?

[Leni Aniva]

Eric Wieser said:

The dev shells will still work

Even without lean4#9905?

it should be because #9905 is just about building Lean itself (including stage 0), which doesn't affect operations of the dev shell.