Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-4895 has successfully built against this PR. (2024-08-01 15:03:57) View Log
• ✅ Mathlib branch lean-pr-testing-4895 has successfully built against this PR. (2024-08-01 17:21:35) View Log
• ✅ Mathlib branch lean-pr-testing-4895 has successfully built against this PR. (2024-08-02 10:57:15) View Log

Are all Nix components going to be removed eventually? I can take over and create a repository for the Nix build paths

I expect that in the long run we certainly keep a nix shell with the build dependencies alive.

We maybe keep using Nix for our own CI uses, but certainly nothing that we’d want other people to import/depend upon.

So if you are motivated to maintain nix-related things in a separate repository, that would be great!

I expect that in the long run we certainly keep a nix shell with the build dependencies alive.

We maybe keep using Nix for our own CI uses, but certainly nothing that we’d want other people to import/depend upon.

So if you are motivated to maintain nix-related things in a separate repository, that would be great!

does it mean the downstream nix repo should not depend on any nix file in this repo? I was hoping to reuse as much internal machinery as possible including the (most importantly) buildLeanPackage

It's up to you if course. But it may be easier to copy all that machinery and start taking ownership in the new repository, and adjust it to your needs.

I got one working. I'll try to support every major Lean version: https://github.com/lenianiva/lean4-nix