What happened to `lean-all` in Nix flakes?

Stream: lean4

[Leni Aniva]

I have a Lean project that is dependent on Lean's Nix flake and uses the lean-all output as a library dependency:

      leanPkgs = lean.packages.${system};
      projectEnv = {
        LEAN_ROOT =leanPkgs.lean-all;
      }

in Lean v4.12.0, this attribute doesn't exist anymore and got moved to .deprecated. If lean-all is deprecated, how can a downstream lean package link against the lean shared library? Should sharedLib be an output attribute then?

[Joachim Breitner]

The whole nix setup is deprecated in core. I think what needs to happen is that someone steps up to maintain a nice nix setup, in its own repository.

[Leni Aniva]

Joachim Breitner said:

The whole nix setup is deprecated in core. I think what needs to happen is that someone steps up to maintain a nice nix setup, in its own repository.

I can take over this part. Should I create a repo with all the Nix build paths? Or will there be a repo in leanprover-community for the Nix components?

[Jon Eugster]

usually you can ask one of the maintainers to transfer your personal github repo to leanprover-community if it is something that's relevant to the community, so you could get started in your own repo

[Leni Aniva]

I wrote a flake for this and tested it on my own project. Seems like its working: https://github.com/lenianiva/lean4-nix