Should we bump nixpkgs version?

Stream: general

[Alissa Tung]

If so, I am willing to file a PR on this. The reason is

• the check phase for ccache on aarch64-darwin is broken, but newer nixpkgs works fine
• in China, Nix binary mirrors won't last so long (as nixpkgs is pinned to 2022)

[Joachim Breitner]

I'd say yes, just try it, and see what breaks :-)

[Alissa Tung]

Seems that build on Darwin is broken., I am not sure how to fix it

ld: warning: directory not found for option '-L/nix/store/w8s745hmd24c605d4fziy4fjakj06dn2-lean-bin-tools/lib/lean'
ld: warning: ignoring file /nix/store/hijjyl9fqynq0vis2bq7a6msyf4b0rb7-Init-lib/libInit.a, building for macOS-arm64 but attempting to link with file built for unknown-unsupported file format ( 0x21 0x3C 0x74 0x68 >
ld: warning: ignoring file /nix/store/2kink7vw6asw0ac64wvsil053frjm10q-Lean-lib/libLean.a, building for macOS-arm64 but attempting to link with file built for unknown-unsupported file format ( 0x21 0x3C 0x74 0x68 >
Undefined symbols for architecture arm64:
  "_initialize_Init", referenced from:

% tree /nix/store/w8s745hmd24c605d4fziy4fjakj06dn2-lean-bin-tools/
/nix/store/w8s745hmd24c605d4fziy4fjakj06dn2-lean-bin-tools/
├── bin
│   ├── leanc
│   └── leanmake
├── include
│   └── lean
│       ├── config.h
│       ├── lean.h
│       ├── lean_gmp.h
│       └── version.h
└── share
    └── lean
        └── lean.mk

cc @Joachim Breitner

[Joachim Breitner]

I am very ignorant about linking in general and OSX in particular. Sebastian said he’s not using the nix integration himself anymore, so I wonder how tenable it is to have it at all, unless we find a volunteer who :heart: nix and linker issues and wants to own this nix stuff. Maybe in a separate repository.

[Scott Morrison]

If that +1 is for "separate repository" then let me add another one. :-)

[Joachim Breitner]

I assume he read me saying „I am very ignorant“, stopped reading and :+1:’ed my message.

[Joachim Breitner]

Although it pains me to see that, especially with the merge queue, the rather slow lean CI runs at least three times (on the branch, in the queue, on the master), and the Nix CI is instantaneous the second and third time (in the happy case), while the other jobs warm up the globe for no good reason. I hope in a decade or two this wasteful recomputation will somehow be a quant thing from the past.

[Jannis Limperg]

Don't worry, Lake and Cache have already reinvented substantial portions of the Nix architecture. In a decade we'll have reinvented the rest as well. :innocent:

[Johan Commelin]

I hope they don't reinvent the Nix language... :see_no_evil:

[Joachim Breitner]

Nix (the language) is to nix (the store, derivations, caching, etc.) like Git (the UX) to Git (the object model).

[Joachim Breitner]

Somehow inventing amazing new concepts rarely correlates with great UX. Good that lean has all these macros then :-)