Add a nix flake build

[Anderssorby]

trafficstars

Adding a nix flake to enable builds and dependency fetching with nix. This has several opinionated choices about structure which can be negotiated.

[Kha]

I would argue that solutions that do not automatically keep the flake.lock<->lean-toolchain versions in sync are strictly worse than no Nix solution.

[Anderssorby]

Well, on NixOS using lake is not an option. Can't we just leave it up to the nix users to keep this up to date? When we eventually unify the two solutions this will no longer be an issue. I think this is an acceptable maintenance for a project in development.

[Anderssorby]

@Kha If you added a commit hash to the lean-toolchain file it would be easy to parse it and keep it in sync with nix.

[Kha]

Well, on NixOS using lake is not an option

Using it in Nix builds may currently not be an option, but lake is only a nix shell nixpkgs#elan away

@Kha If you added a commit hash to the lean-toolchain file it would be easy to parse it and keep it in sync with nix

This is not sufficient for Lean as a flake input since there's also the nar hash. My current plan is to implement a custom fetcher that creates the flake.lock at fetch time (i.e. when we have full network access to retrieve the given release tag).

[Kha]

I'm not sure I've stated this before, but my philosophy is that any Nix/Lean integration should be a net benefit that does not annoy/disadvantage anyone not using it. As long as there good reasons for not using it at least.

[Anderssorby]

should be a net benefit that does not annoy/disadvantage anyone not using it.

I totally agree on this, but this should also extend to lake + elan. Currently using this on NixOS is a pain and it constantly breaks because NixOS uses nonstandard locations, which is why I have uninstalled it. Also I don't see how having a flake file would affect users not using it. I don't expect non nix users to update the flake and that should not be a big issue.

This is not sufficient for Lean as a flake input since there's also the nar hash.

Flake supports specifying the git hash of inputs.

{
  inputs = {
    lean = {
      url = "github:leanprover/lean4/3ad8dcb7ffdc3b01ae326798bf2e3a7e11cd961b";
    };
}

Also my ambition is to unify the two solutions by creating a nix evaluator / transpiler + parser + derivation generator implemented in Lean. https://github.com/Anderssorby/Nix.lean/tree/acs/parser I don't have a lot of experience with this though. Contributions are welcome. This could also be a benefit to the general nix ecosystem

[gebner]

I completely agree with Sebastian that Nix support should not incur any costs on the non-Nix developers. I don't want to maintain and support two build systems. (And since Nix doesn't work on Windows, we'll always have to support the non-Nix build.) Until we have lake2nix, adding Nix support just adds extra development cost without significant benefits. The number of people who only want to use Nix and not lake is very, very small.

I'm not at all enthusiastic about moving the source code into yet another subdirectory and adding a flake-specific direnv file. (The PR also doesn't build with lake, but I assume you plan to fix that.)

In my very personal opinion, the Nix build is an amazingly cool tech demo but completely unsuitable for production use. It doubles the maintenance and development cost on every front: editor support, tooling, documentation, build setup in each project, and even twice the CI time. In return, you get very little. Lake runs everywhere that Nix runs. But you can't use Nix on Windows. Or to link against system libraries on non-NixOS systems. You can't even use the Nix build for packages in nixpkgs because of the prohibition on IFD and lack of recursive Nix.

I don't expect non nix users to update the flake and that should not be a big issue.

We're upgrading the Lean version relatively often, so non-Nix users will have to touch flake.nix as well.

Well, on NixOS using lake is not an option.

On NixOS, lake is very much an option. I'm using it every day. (EDIT: apparently linking has been broken for the last few nightlies... https://github.com/leanprover/lean4/issues/1130)

constantly breaks because NixOS uses nonstandard locations

It will only break if there's an stdenv change (or gmp change, but that's even more rare). Personally, I run into very few issues because I'm regularly deleting ~/.elan to free up space (every nightly is like half a gigabyte).

[Anderssorby]

Getting this PR merged was a long shot. I mostly did this change to enable building mathlib with nix.

We're upgrading the Lean version relatively often, so non-Nix users will have to touch flake.nix as well. Why? Not updating or maintaining the flake.nix will not affect non-nix users. I feel it should be acceptable that maintaining the flake.nix would be the responsibility of only the nix users.

[gebner]

I feel it should be acceptable that maintaining the flake.nix would be the responsibility of only the nix users.

Then I'm okay with this PR as long as it only adds the flake.nix/flake.lock files. No restructuring, no direnv files, and the README should make clear that the nix build is experimental/unstable. (And please be aware that we upgrade the Lean version every few days, so the Nix setup will stop working very quickly if it is not updated.)