-
Notifications
You must be signed in to change notification settings - Fork 20
Add a nix flake setup #15
Add a nix flake setup #15
Conversation
.github/workflows/nix.yml
Outdated
- master | ||
- main | ||
jobs: | ||
tests: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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).
I feel weird for being the one to object to this PR, but: who will update the |
@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 |
@tydeu True, it is most convenient if there is a nix user which can run |
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. |
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 |
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 |
@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) |
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. |
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
Outdated
nixpkgs.url = "github:nixos/nixpkgs/nixos-21.05"; | ||
lean = { | ||
url = "github:leanprover/lean4"; | ||
inputs.nixpkgs.follows = "nixpkgs"; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You should remove this follows
btw to avoid unnecessary binary cache misses
@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 I think that adding |
c27104a
to
c2d3d7c
Compare
@tydeu It's fixed now. |
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.