Add a nix flake setup

[Anderssorby]

This adds a nix flake setup to lake and a corresponding CI. Eventually I would hope that Lake and nix flake will be somewhat interoperable in the sense that they both support content addressed and deterministic builds.

[tydeu]

Also, name the job Ubuntu as that is the machine it is running on (and building for). It is doing both a build and a check, so tests is a bit of a misnomer.

[tydeu]

Please name it just Ubuntu, not Build and Check Ubuntu to make it consistent with the other CIs. Also, I don't think GItHub even allows job names that are arbitrary strings (or, at least, that would be my best guess as to why the job doesn't register).

[Kha]

I feel weird for being the one to object to this PR, but: who will update the lean input when leanpkg.toml's lean_version is updated? As Mac is a Windows user, this looks like a recipe for frequently-broken CI.

[tydeu]

@Anderssorby, @Kha makes a good point, how can this be feasibly maintained if I am (or another maintainer is) not using Nix? Is there a way for one to manually update the Lean version for Nix (e.g.., by editing a file) when one updates the version in leanpkg.toml?

[Anderssorby]

@tydeu True, it is most convenient if there is a nix user which can run nix flake update occasionally. I guess it is possible to manually update the revision in flake.lock, but you also need to update the NAR hash which you need nix to know, but as long as you have some contributors which can do this update it shouldn't be a big problem. You want to support unix right? So you need to test it occasionally in that environment anyway. You could also disable the nix CI if it gets annoying. I'm planning on using this in my experiments with Lean and Yatima going forwards.

[tydeu]

@Anderssorby

You want to support unix right? So you need to test it occasionally in that environment anyway.

As Lake is written in Lean, the Unix support comes largely as a by-product from Lean itself. Lean is cross-platform, so I can develop the project on my Windows machine and have it still work on Linux and MacOS. The problem here is that in order to support the Nix build, I also need to have a local Nix installation, which I do not have (and the same may be true for other future contributors and/or maintainers). This is not the case for the other builds. For instance,, there is a MacOS build for Lake in the CI, but I have never tested that locally on a Mac (and may never do so).

Also, it should be noted that, as it stands for now, I am the sole maintainer of Lake, there is no one else.

[tydeu]

Also, it concerns me that you need to have Nix installed in order to update a build configuration. This strikes me as a major flaw with Nix. While I understand that you may need Nix in order to compute the integrity hash, such a hash should not be required to perform builds. For example, in npm, the package-lock.json (which contains integrity hashes) is a useful but unnecessary component for building.

[Kha]

You seem to be talking about two different things at once - requiring a lock file, and requiring the build tool for updating/generating it. Nix doesn't do the first one either (but we of course want Lean packages to be locked against Lean), and the second is just as true for npm or any other tool that uses a (non-standardized) integrity hash, I would assume

[Kha]

@Anderssorby If you want to use Lake via Nix, someone should just improve Nix' submodules support so we can extend leanprover/lean4#683 with Nix support :) (likely after it is merged)

[tydeu]

Nix doesn't do the first one either (but we of course want Lean packages to be locked against Lean),

Ah, my mistake, I misunderstood. In that case, I could just delete the lockfile when a change makes it outdated and wait until some other contributor decides to regenerate it and add it back. Obviously, this is sub-optimal solution, but I think it is still a sufficient one.

[Kha]

Yes, that would work since going forward we will not make incompatible changes to Lean without immediately repairing Lake, so it's never wrong to fall back to the newest Lean in absence of a lock file. So I would probably suggest to commit only the flake.nix (and secondary files) and leave out flake.lock and the CI setup, since there is no maintainer to maintain them as you pointed out.

[Kha]

You should remove this follows btw to avoid unnecessary binary cache misses

[tydeu]

@Kha Is there any harm in keeping the CI setup? It can serve as a nice test that such a build does indeed work and it doesn't need the lockfile, right?

[Anderssorby]

@Kha @tydeu I've removed the flake.lock and nix CI. I'm also looking into ways to use lake from within nix.

[tydeu]

@Anderssorby I think that adding flake.lock to the .gitignore resulted its deletion not being committed.

[Anderssorby]

@tydeu It's fixed now.