feat: Add nix flake

[Anderssorby]

Add a nix flake build to this repo

[arthurpaulino]

Is this necessary? I try to avoid opening namespaces like that. This file compiles just fine without this line

[arthurpaulino]

We're using leanprover/lean4:nightly-2022-08-09 in the lean-toolchain file

[Anderssorby]

There is no tag for that release. You can ofc set it to the explicit git commit hash.

[arthurpaulino]

So we need to get the git commit hash of the Lean 4 version every time we do a toolchain bump?

[Anderssorby]

Yes, idk how lake fetches the data. It is probably possible to tie into that with nix as well.

[lenianiva]

Is there any update to this? The lean-toolchain file has stabilized and we can probably use something like

    lean = {
      url = "github:leanprover/lean4?ref=v4.4.0";
    };

as a flake input

[lenianiva]

Update: Lean's official flake build is deprecated leanprover/lean4#4895

I might create a Lean4 nix repo sometimes later to replace this, but I don't think having the user handle the build themselves is very difficult, e.g.

      lspecLib = leanPkgs.buildLeanPackage {
        name = "LSpec";
        roots = [ "Main" "LSpec" ];
        src = "${lspec}";
      };

      test = leanPkgs.buildLeanPackage {
        name = "Test";
        roots = [ "Test.Main" ];
        deps = [ lspecLib repl ];
        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
          src = ./.;
          filter = path: type:
            !(pkgs.lib.hasInfix "Pantograph" path);
        });
      };