using nix

Stream: lean4

[Edward Ayers]

Hi I just wanted to report my experience using nix.
I followed this link https://leanprover.github.io/lean4/doc/setup.html#nix-setup

curl -L https://nixos.org/nix/install | sh
nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix
nix flake new my-first-lean4-package -t github:leanprover/lean4
cd my-first-lean4-package
nix build

It took about 30 mins to build.
The build procedure seems to be building a load of CXX code.
I got loads of warnings, I am not sure if I should be concerned.

warning: --- Invalid path signature ------------------------------------------------------------------ nix
substituter 'https://lean4.cachix.org' does not have a valid signature for path '/nix/store/bjnk91prlnvzhsvbk2sbsp5f1484bkbh-Lean.ReducibilityAttrs'

[Edward Ayers]

This fails for me: what am I missing?

[nix-shell:~/mylean4pkg]$ nix build .#executable
error: --- Error --------------------- nix
flake output attribute 'packages.x86_64-linux.executable' is not a derivation

[Sebastian Ullrich]

Edward Ayers said:

I got loads of warnings, I am not sure if I should be concerned.

This is definitely the reason it built from source. Did you also do the /etc/nix/nix.conf steps? (Perhaps "recommended" is not strong enough there)

[Sebastian Ullrich]

It's probably the biggest weakness in the current setup. It looks like Nix will soon allow setting these options per project ("flake"), but that hasn't landed on master yet. And it will probably require using an unstable Nix daemon (and not just a client like opening that nix-shell does), so not exactly easier to set up either...

[Sebastian Ullrich]

Edward Ayers said:

This fails for me: what am I missing?

[nix-shell:~/mylean4pkg]$ nix build .#executable
error: --- Error --------------------- nix
flake output attribute 'packages.x86_64-linux.executable' is not a derivation

Oh, I guess I didn't actually test that step... executable actually is a function right now that takes the filename to produce since I wanted the Leanpkg package to produce a leanpkg executable. Looks like there is in fact a lib.toLower function, so maybe I should just use that one (as a default).

[Edward Ayers]

Nice I added the config and it's downloading woop

[Sebastian Ullrich]

Changed executable, thanks for giving it a try!

[Sebastian Ullrich]

And now it seems to actually work

[Simon Hudon]

When I try to execute the resulting binary I get the --help output of Lean:

[nix-shell:~/my-first-lean4-package/result/bin]$ ./mypackage
Expected exactly one file name
Lean (version 4.0.0, Release)
Miscellaneous:
  --help -h          display this message
  --version -v       display version number
  --githash          display the git commit hash number used to build this binary
  --run              executes the 'main' definition
  --o=oname -o        create olean file
  --c=fname -c       name of the C output file
  --stdin            take input from stdin
  --root=dir         set package root directory from which the module name of the input file is calculated
                     (default: current working directory)
  --trust=num -t     trust level (default: max) 0 means do not trust any macro,
                     and type check all imported modules
  --quiet -q         do not print verbose messages
  --memory=num -M    maximum amount of memory that should be used by Lean
                     (in megabytes)
  --timeout=num -T   maximum number of memory allocations per task
                     this is a deterministic way of interrupting long running tasks
  --threads=num -j   number of threads used to process lean files
  --tstack=num -s    thread stack size in Kb
  --plugin=file      load and initialize shared library for registering linters etc.
  --deps             just print dependencies of a Lean input
  --json             print JSON-formatted structured error messages
  --server           start lean in server mode
  --worker           start lean in server-worker mode
  --profile          display elaboration/type checking time for each definition/theorem
  --stats            display environment statistics
  -D name=value      set a configuration option (see set_option command)

[Reid Barton]

that's what lean does!

[Reid Barton]

unlike lean 3

[Simon Hudon]

But I compile a .lean file that does #eval "hello world"

[Simon Hudon]

[nix-shell:~/my-first-lean4-package]$ cat MyPackage.lean
#eval "Hello, world!"

[Reid Barton]

oh I see, I don't know anything about Nix, but it looks like you managed to produce a Lean executable instead

[Sebastian Ullrich]

You're missing a main function

[Simon Hudon]

You're right that fixes it

[Simon Hudon]

I don't understand what the behavior of the compiler is supposed to be when it tries to produce a binary but doesn't find a main function

[Sebastian Ullrich]

Well, there's another main function in leancpp.so :) . This is just a hack in the Nix setup so I don't have to "switch" between C++ and Lean multiple times.

[Simon Hudon]

Oh! Does the binary always have the whole Lean prover compiled in with the rest of its functions?

[Sebastian Ullrich]

Hopefully your binary is not in fact as big as lean after adding a main function

[Zygimantas Straznickas]

Hi,
does the nix configuration currently support linking lean packages against static library dependencies? E.g. if I have a package

@[extern "test_impl"]
def test (n: UInt32) : UInt32 := n

and a static library exporting a symbol test_impl, can I just pass it as a dep to leanPkgs.buildLeanPackage?

[Sebastian Ullrich]

Not yet because no-one has tried that even without Nix so far! We should probably add an argument injected here: https://github.com/leanprover/lean4/blob/master/nix/buildLeanPackage.nix#L136

[Sebastian Ullrich]

I'm not sure what the proper Nix way here is though. For example, if a Lean library declares an external dependency, any executable depending on the library should inherit the dependency.

[Zygimantas Straznickas]

thanks, I’ll take a look later tonight. I also tried to write a custom deriver by reverse-engineering what the compiler does, and also got stuck in the linking stage, probably because of the same issue

[Sebastian Ullrich]

It doesn't help that there is no real Nix infrastructure for C, probably because they assume you're already using some other build system like CMake that will take care of assembling the linker flags etc.

[Zygimantas Straznickas]

Are you guys open to PRs in infrastructure code like this, or should I just post stuff here if I find something I believe is useful?

[Zygimantas Straznickas]

(btw, here's one small patch I'm using to make the lean binary available when in the nix shell:

diff --git a/shell.nix b/shell.nix
index a0ecd9eeae..18cd9ea056 100644
--- a/shell.nix
+++ b/shell.nix
@@ -16,6 +16,6 @@ in { pkgs ? flakePkgs.nixpkgs, llvmPackages ? null }:
     CTEST_OUTPUT_ON_FAILURE = 1;
   };
   nix = pkgs.mkShell {
-    buildInputs = [ flakePkgs.nix ];
+    buildInputs = [ flakePkgs.nix flakePkgs.lean ];
   };
 }

this, together with https://marketplace.visualstudio.com/items?itemName=arrterian.nix-env-selector , makes it easier to run my own version of vscode with a modified lean4 extension)

[Simon Hudon]

@Zygimantas Straznickas Can you elaborate on what this does? If I wanted to use it with emacs, can I use the same thing?

[Zygimantas Straznickas]

IIUC it does some magic symlinking to , effectively, add /nix/store/randomchanginghash-lean/bin to PATH within the nix shell so lean can be used from the terminal as lean. I assume this will also work with emacs if you start it from a nix shell or use something like https://github.com/nix-community/nix-direnv.

(this addresses the problem of having a way to refer to the lean binary. I'm not sure how the emacs mode works, this might not even be a problem in the first place :) )

Though I'm still stuck at making VSCode+ext+lean_server to recognize custom lean package dependencies defined through nix: e.g., in MyPackage2 it succeeds at import Lean.<...>, but errors out on import MyPackage1, even though nix build successfully builds MyPackage2

[Simon Hudon]

Thanks for the pointer! That's actually the issue I'm trying to solve now. I'm going to do some reading and play around a bit with this.

[Simon Hudon]

I hope your project works out. It sounds like the kind of stuff I'd like to use

[Sebastian Ullrich]

Right, for the editor you'll want to have .#lean-dev (output of a flake using the template) in the path, which is a lean wrapper that does the automatic compilation and importing of package-local depdencencies

[Sebastian Ullrich]

The bare lean, as you've observed, only knows its stdlib

[Sebastian Ullrich]

So flakePkgs.lean-dev should work, I think

[Simon Hudon]

Thanks for pointing it out. How do I find out what the path of .#lean-dev is?

[Sebastian Ullrich]

In the Nix store?

[Simon Hudon]

I'm not familiar enough with Nix to know what that means

[Sebastian Ullrich]

Then I don't know what your question is :) . If you do not want to go the nix-env-selector way, you can create a link to the executable using nix build .#lean-dev -o ./lean-dev. But that way you'll have to remember updating that link when the package's Lean version has changed yourself.

[Simon Hudon]

Basically, at the point where I am with setting up emacs, I need to set up the PATH environment variables and the lean4-rootdir Emacs variable so that lean4 (the binary) and its libraries can be found by the language server

[Sebastian Ullrich]

Yes, that should get you there. With the mentioned caveat.

[Simon Hudon]

Thanks!

[Simon Hudon]

Where can I find out how nix-env-selector works?

[Sebastian Ullrich]

(Note that the lean-dev setup might change soon)

[Zygimantas Straznickas]

aha, lean-dev works, thanks! IDE setup complete :check:

[Reid Barton]

I can't help reading .#foo as an emacs backup file and I want to delete it :trash_can:

[Simon Hudon]

@Zygimantas Straznickas Super! Would you mind walking me through what you did? In particular, how do you install the version of Lean where you patched shell.nix?

[Sebastian Ullrich]

@Reid Barton I had to specifically patch the sh highlighter used in the docs to not interpret # without leading whitespace as a comment... :grimacing:

[Zygimantas Straznickas]

@Simon Hudon

Sure, so,
1) since you want to patch shell.nix, you'll probably want to clone the lean4 code somewhere on your machine
2) update shell.nix to expose lean-dev: in line 19, add flakePkgs.lean-dev to the array
3) enter the nix shell: nix-shell <lean4_dir> -A nix
4) type lean into the shell and confirm that you get lean's help output
5) type which lean into the shell and confirm the first line starts with /nix/store/

(I don't fully understand how nix and flakes interplay, so sometimes I get a problem with nix complaining about mismatching dependency hashes, and fix it by a dumb sledgehammer approach of deleting all of my flake.lock files and rebuilding everything. I should really learn more about what that problem actually means :) )

6) Now we're in emacs territory so I haven't tested that but my guess would be to either
6.1) Just start your global emacs from the nix shell command line and see if lean support works out of the box, without specifying a custom lean4-executable-name or lean4-rootdir
6.2) If that doesn't work, emacs doesn't inherit PATH and does something smarter, and I don't know anything about that :) The same applies if you want to start emacs from a desktop shortcut, or if you run an emacs daemon.

[Zygimantas Straznickas]

btw, for context, one reason I'm going through all this trouble for VSCode is that I'm using WSL, and I can't use the nix-built vscode version because that would try to open a graphical app in WSL and fail. Instead, Microsoft has this convenient bridge that connects my Windows VSCode with a backend running in WSL.

[Simon Hudon]

Thank you so much for the detailed instructions! I need to run but I'll test them later tonight

[Sebastian Ullrich]

FYI, I just looked up the closures sizes of Lean itself/+ Emacs/+ VS Code using Nix, meaning the cumulative size of all dependencies down to glibc. In other words, what you would have to download if those exact versions are not already in your Nix store.

$ nix path-info -Sh .#lean
/nix/store/s1cmjry080s7ilv3h8axj9rl4jra7jl8-lean       1.5G
$ nix path-info -Sh .#emacs-package
/nix/store/bj514l0pag981zbs75xflc11i2c797q2-emacs-package      2.6G
$ nix path-info -Sh .#vscode-package
/nix/store/cknca6rnm2z2p6j4q593p3fdk80dgf0m-vscode-package     2.2G

A full 1.0GB of that is clang, which ideally we would only download when someone actually wants to compile a Lean package into a binary. /cc @Makarius Wenzel

[Zygimantas Straznickas]

Alright, I now have static libraries linking successfully. My next goal: set up nix so that initialize test_symbol : IO.Ref (String) ← IO.mkRef "Asdf"defined in external package A would be visible in external package B.

[Adam Topaz]

I'm trying to set up nix on my machine. For the /etc/nix/nix.conf step that @Sebastian Ullrich mentioned above, is it necessary to put the config file in /etc or can I use a non-privileged folder (e.g. some file in $HOME/.nix-profile/)?

[Adam Topaz]

Actually it seems that $HOME/.config/nix/nix.conf might work?

[Adam Topaz]

There's another silly issue that I came across, just in case someone else has this issue: I had a problem where the backspace key in the nix-shell would create a space instead of deleting the character. Has anyone else come across this?

This seems like a terminal specific issue, since setting $TERMto be e.g. xterm before running nix-shell fixes the problem (whereas my default $TERM is rxvt-unicode-256color).

[Sebastian Ullrich]

Adam Topaz said:

I'm trying to set up nix on my machine. For the /etc/nix/nix.conf step that Sebastian Ullrich mentioned above, is it necessary to put the config file in /etc or can I use a non-privileged folder (e.g. some file in $HOME/.nix-profile/)?

If you're using a multi-user installation of Nix (the default), your Nix daemon will run as root and as such accept privileged options like trusted-substituters only from privileged locations

[Adam Topaz]

I see. Thanks.

[Sebastian Ullrich]

Sebastian Ullrich said:

A full 1.0GB of that is clang, which ideally we would only download when someone actually wants to compile a Lean package into a binary. /cc Makarius Wenzel

This is now the case with https://github.com/leanprover/lean4/pull/256:

$ nix path-info -Sh .
/nix/store/zyzyfm2c8n1rj7mh8f8x2kn32668q389-lean     362.6M

[Sebastian Ullrich]

Sebastian Ullrich said:

Well, there's another main function in leancpp.so :) . This is just a hack in the Nix setup so I don't have to "switch" between C++ and Lean multiple times.

fixed

[Cyril Cohen]

I had to deactivate flakes this week cf https://discourse.nixos.org/t/nix-shell-assertion-request-expectedetag-res-etag-failed/11119/9
Is it still possible for me to run lean4 on nix?

[Sebastian Ullrich]

I didn't encounter this issue inside the Lean-Nix shell yet (only outside with my system Nix that is on another version), but now that a fixed version of Nix should be on Hydra, I can update the shell. Assuming that this issue is client-side, not daemon-side.

[Sebastian Ullrich]

@Cyril Cohen Re-reading your question, are you using a Lean shell as in https://leanprover.github.io/lean4/doc/setup.html#nix-setup? You do not have to enable flakes system-wide to use the Lean Nix setup.

[Cyril Cohen]

Oh thanks, since I had flakes until yesterday, I did not even notice you had a compatibiliy layer with legacy shells. Thanks

[Sebastian Ullrich]

I updated our pinned Nix version just to be safe

[Sebastian Ullrich]

The good news is that I hope to simplify the setup on Linux soon :) https://twitter.com/derKha/status/1354013281812410369

Looks like we could drastically simplify the Lean 4 Nix setup now :eyes: https://twitter.com/derKha/status/1354013281812410369/photo/1

- Sebastian Ullrich (@derKha)

[Zygimantas Straznickas]

Alright, I finally implemented building static libraries/plugins on Nix (in my fork of Lean4). Not sure if the change is PR-ready, it's not the most elegant -- but at least it works :)

The change: https://github.com/zygi/lean4/commit/9fb8aad8f5d38b3383c0698c1b857f744e8f1465
Example of the ergonomics it provides:
https://github.com/zygi/leannixstatic1
https://github.com/zygi/leannixstatic2

[Zygimantas Straznickas]

@Sebastian Ullrich

[Zygimantas Straznickas]

nvm, this somehow broke go-to-definition

[Zygimantas Straznickas]

or did go-to-definition ever work with nix?

[Wojciech Nawrocki]

It should work, yes, with the caveats that for go-to-def into Lean sources LEAN_SRC_PATH needs to be set (but I think emacs/vscode-dev both set it). And for go-to-def into imported packages leanpkg print-paths needs to report sensible paths which for leanpkg.toml it should. I'm not sure what the story is with flake.nix.

[Zygimantas Straznickas]

Thanks! It works within the same file so it must be the leanpkg thing

[Sebastian Ullrich]

Looks good to me at first glance!

[Sebastian Ullrich]

Would be interesting to check if -fpic actually has a performance impact using clang https://stackoverflow.com/a/51611087/161659

[Zygimantas Straznickas]

sg, will try to beautify it a little bit and do a PR

[Zygimantas Straznickas]

also, added support for Nix go-to-definition. Instead of leanpkg print-paths, Nix will build a combined-dependency-source-dir and pass it in LEAN_SRC_PATH.

[Sebastian Ullrich]

I have to say I'm very much satisfied with Nix local and remote caching when working on Lean. Both no-op rebuilds after switching branches and automatically fetching the latest CI build after a pull just feel great. However, I acknowledge that for users of Lean 4 there are a few issues with this approach:

• Fetching Lean from the binary cache should be much faster (~2min) than building it from scratch, but that's still awfully slow compared to downloading a single ~100MB nightly build archive. This is both because the "build plan" has to be computed first by parsing the header of every .lean file (via import-from-derivation, which is not exactly fast) and then all ~400 .olean files are downloaded individually.
• Even with the very generously sized free Cachix cache, commits are cached only for about a month, while there is no time limit with our binary releases on GitHub. Per-commit caching is very useful for developers, but less so for users, for which nightly releases should usually be sufficient.
• There is no direct way to map leanpkg.toml lean_version specifiers such as "leanprover/lean4:nightly-2021-04-20" to cache entries.
• The cache has to be configured as a trusted substituter.

Thus, if we want the Nix setup to be at least as fast and convenient as, and potentially also more compatible with, the elan setup, it seems like for users of Lean it should fetch it from the GitHub releases, not from Cachix. Downloading and Nix-patching binary releases is nothing unheard of in nixpkgs, so I feel we would be in good company.

Specifically, what I'm imagining is that we have CI generate and commit a new configuration file, say releases.json on a branch releases in leanprover/lean4-nightly with the following content:

{
  "releases": {
    "nightly-2021-04-21": {
      "x86_64-linux": {
        "url": "https://github.com/leanprover/lean4-nightly/releases/download/nightly-2021-04-21/lean-4.0.0-nightly-2021-04-21-linux.tar.gz",
        "sha256": "..."
      }, ...
    }, ...
  },
  "latest": "nightly-2021-04-21"
}

With this and a corresponding (static) flake.nix that implements the downloading and patching, we could add that branch as an input to any flake and either access a version directly with something like releases.${system}.latest, or parse a leanpkg.toml and use the version from there. The only limitation in the latter case is that the locked flake input must be at least as recent as the lean_version in leanpkg.toml, so Nix users might sometimes need to do an extra nix flake update when someone else has updated the Lean version.

It's not quite clear to me yet where our custom Nix functions such as buildLeanPackage should come from in this setup, but if we want to keep them version-specific, we should probably include them in the binary releases (negligible storage overhead) and import-from-derivation them from in there, i.e. it would look something like releases.${system}.latest.buildLeanPackage.

Ok, that's all I can think of so far. Thoughts?

[Sebastian Ullrich]

Note that the same configuration file could be used by elan so it can stop having to parse the GitHub release page's HTML :upside_down:

[Daniel Fabian]

presumably you could build a binary using nix too for users?

[Sebastian Ullrich]

Yes, you could have Nix build a big tarball as well and put it in the binary cache if you meant that. But the build plan would still have to be computed in order to compute the hash of the tarball, so this would not solve any of the above issues.

[Sebastian Ullrich]

Ideally it should be possible to work on a leanpkg.toml-based package using the Nix setup without any flake.nix being present. This could either be done using a temporary flake (Eelco Dolstra has some experiments in that direction I think) or perhaps using an old-style nix-build -E ....

[Daniel Fabian]

I mean more like a nix way of creating the nightly builds. But maybe that's already a solved problem anyway.

[Sebastian Ullrich]

Putting a Nix build result directly in a tarball and publishing it usually doesn't make sense because it will contain many broken references to the libc and other dependencies elsewhere in the Nix store. In fact the nightlies are already built inside a nix-shell (but using cmake) and we patch the build results in the end to work on generic Linux/macOS machines. So I think the only two ways of distribution are 1) using a "proper" binary cache that automatically fetches dependencies, as we do right now, and 2) downloading a generic-Linux/macOS binary and patching it on the fly for Nix, as proposed above.

[Daniel Fabian]

did you consider the FHS wrapper to make it more generic? (Though I have to admit, I don't know if it's used in this way). At least you might not have to patch in the end.

[Sebastian Ullrich]

Binary patching is very much established in the Nix ecosystem, it's definitely cleaner than the FHS wrapper :)

[Sebastian Ullrich]

It's just a bit funny that we will un-Nix-patch the release before uploading it and then re-patch it on the (Nix) user's machine, but the first part is basically an implementation detail of how the releases are created

[Sebastian Ullrich]

After mulling over the above issues for a while, let's consider if we could possibly solve them using Nix alone:

• I'm not aware of any currently available way to skip/significantly optimize the "build plan" evaluation, but in theory it is very much possible: Nix already uses an evaluation cache locally that skips this step if the flake contents are unchanged. Doing the same remotely is listed under "Future Improvements" in https://www.tweag.io/blog/2020-06-25-eval-cache/, though I'm not aware of any work or even a GitHub issue on this feature. With it, Nix would download a Lean release's commit (over HTTP, not clone the whole repo), hash its contents, and then immediately skip to downloading binaries from the cache.
  Regarding downloading 400 .olean files, this could trivially be optimized today by adding a new derivation that copies all .olean files of a package into a single directory tree and pushing that to the cache. The biggest downside of doing that is that every commit would take up much more cache space. However, here the Nix setup could also easily improve on the standard setup: using Nix's laziness, there is no need to even download the whole Lean package, or its compiled static library, until users actually import it. These two alone make up 60% of a release's size! The only reason this isn't already the case today is that we try to emulate the standard setup's directory layout, which contains all these dependencies in lib/, so that we can run Lean's test suite with minimal changes. But there is no reason to use this "all-inclusive" derivation in the pure-Nix buildLeanPackage as well.

• There is no magic bullet for fitting more commits in the binary cache, but perhaps there are workarounds. For example, we could use a separate cache for nightly and/or stable builds. That would still not give us unbounded cached releases like GitHub graciously does, but probably a sufficient number. If you really need an old release, maybe building it from source is tolerable since with Nix we can at least guarantee it will be painless and eventually succeed.

• If we auto-generate a flake.nix from a leanpkg.toml, we can certainly map lean_version = "leanprover/lean4:nightly-2021-04-20" to inputs.lean = github:leanprover/lean4-nightly/2021-04-20;. If a project has both files, we could have a tool for keeping them in sync.
• Speaking of tools, I'm now committed to building a custom wrapper around a statically built Nix for Lean, which will resolve the global installation and configuration issues... on Linux (because using a local Nix store depends on mount namespaces)

In summary, while the Nix setup is unlikely to beat the standard setup on time for downloading a Lean release in the near future, we could reasonably already do so on download size for most use cases (which on a slow connection could of course translate into less time as well).

Here's hoping someone interested will actually read this :) .

[Ryan Lahfa]

Sebastian Ullrich said:

After mulling over the above issues for a while, let's consider if we could possibly solve them using Nix alone:

• I'm not aware of any currently available way to skip/significantly optimize the "build plan" evaluation, but in theory it is very much possible: Nix already uses an evaluation cache locally that skips this step if the flake contents are unchanged. Doing the same remotely is listed under "Future Improvements" in https://www.tweag.io/blog/2020-06-25-eval-cache/, though I'm not aware of any work or even a GitHub issue on this feature. With it, Nix would download a Lean release's commit (over HTTP, not clone the whole repo), hash its contents, and then immediately skip to downloading binaries from the cache.
  Regarding downloading 400 .olean files, this could trivially be optimized today by adding a new derivation that copies all .olean files of a package into a single directory tree and pushing that to the cache. The biggest downside of doing that is that every commit would take up much more cache space. However, here the Nix setup could also easily improve on the standard setup: using Nix's laziness, there is no need to even download the whole Lean package, or its compiled static library, until users actually import it. These two alone make up 60% of a release's size! The only reason this isn't already the case today is that we try to emulate the standard setup's directory layout, which contains all these dependencies in lib/, so that we can run Lean's test suite with minimal changes. But there is no reason to use this "all-inclusive" derivation in the pure-Nix buildLeanPackage as well.

• There is no magic bullet for fitting more commits in the binary cache, but perhaps there are workarounds. For example, we could use a separate cache for nightly and/or stable builds. That would still not give us unbounded cached releases like GitHub graciously does, but probably a sufficient number. If you really need an old release, maybe building it from source is tolerable since with Nix we can at least guarantee it will be painless and eventually succeed.

• If we auto-generate a flake.nix from a leanpkg.toml, we can certainly map lean_version = "leanprover/lean4:nightly-2021-04-20" to inputs.lean = github:leanprover/lean4-nightly/2021-04-20;. If a project has both files, we could have a tool for keeping them in sync.
• Speaking of tools, I'm now committed to building a custom wrapper around a statically built Nix for Lean, which will resolve the global installation and configuration issues... on Linux (because using a local Nix store depends on mount namespaces)

In summary, while the Nix setup is unlikely to beat the standard setup on time for downloading a Lean release in the near future, we could reasonably already do so on download size for most use cases (which on a slow connection could of course translate into less time as well).

Here's hoping someone interested will actually read this :) .

If we auto-generate a flake.nix from a leanpkg.toml, we can certainly map lean_version = "leanprover/lean4:nightly-2021-04-20" to inputs.lean = github:leanprover/lean4-nightly/2021-04-20;. If a project has both files, we could have a tool for keeping them in sync.

Actually, leanpkg.toml can work with a Nix setup and read the data directly from the Flakes file, lockfile, etc. Right?

[Ryan Lahfa]

Sebastian Ullrich said:

• Speaking of tools, I'm now committed to building a custom wrapper around a statically built Nix for Lean, which will resolve the global installation and configuration issues... on Linux (because using a local Nix store depends on mount namespaces)

FWIW, there is https://github.com/DavHau/nix-portable

[Sam Stites]

(deleted)

[Sam Stites]

Ryan Lahfa said:

FWIW, there is https://github.com/DavHau/nix-portable

DavHau's mach-nix is also worth checking out as a flake-compatible build tool for python (with a command line wrapper as well): https://github.com/DavHau/mach-nix

[Sebastian Ullrich]

Ryan Lahfa said:

Actually, leanpkg.toml can work with a Nix setup and read the data directly from the Flakes file, lockfile, etc. Right?

You can't really make sense of a flake.nix without a Nix interpreter, so using the restricted leanpkg.toml format as the common ground is way easier. At one point I considered separate flake.nix and leanpkg.toml files with a common lock file, but I really don't want to teach leanpkg how to calculate narHashes...

[Sebastian Ullrich]

You don't have to quote my entire message btw :)

[Sebastian Ullrich]

Ryan Lahfa said:

FWIW, there is https://github.com/DavHau/nix-portable

I know about the project, but it's not clear to me if there are relevant systems for Lean where this would work but not mount namespaces. In particular, even Debian has activated namespaces for non-root users by now afaik. And the big missing platform, macOS, is not supported by nix-portable either.

[Sebastian Ullrich]

Sebastian Ullrich said:

However, here the Nix setup could also easily improve on the standard setup: using Nix's laziness, there is no need to even download the whole Lean package, or its compiled static library, until users actually import it. These two alone make up 60% of a release's size! The only reason this isn't already the case today is that we try to emulate the standard setup's directory layout, which contains all these dependencies in lib/, so that we can run Lean's test suite with minimal changes. But there is no reason to use this "all-inclusive" derivation in the pure-Nix buildLeanPackage as well.

This is now implemented: the (uncompressed) closure size of the lean derivation shrunk from 806 derivations totaling 434MB to just 6 derivations totaling 89MB (a good chunk of which is glibc, which you might already have from a different Lean revision).

$ nix path-info -Sh .#lean-all
/nix/store/9s2bcmdr8035dkfx9vgfh5jxcibqnxaw-lean     434.1M
$ nix path-info -rsSh .#lean
/nix/store/1yvpgm763b3hvg8q4fzpzmflr5674x4j-glibc-2.32-10         29.7M   31.4M
/nix/store/c13jjm75vr23fv15wr1gqvlkkf6s1m7g-libidn2-2.3.0        217.5K    1.8M
/nix/store/gk72n6pafkh603q9syxgj0i3pwp4fqf4-gmp-6.2.1            734.3K   38.1M
/nix/store/isy60my0ijjzh49rscgdb1i2457nf7lp-gcc-9.3.0-lib          6.0M   37.4M
/nix/store/ngc68ngmymx2vmbj6gih07n7z2024ffj-libunistring-0.9.10    1.6M    1.6M
/nix/store/p64iq0dhanyzzf2l0g0bkiw252l40z6c-lean                  51.5M   89.7M

When building a Lean package using Nix, this executable will be used to parse all import paths, which will then be fetched lazily. In other words, if you use prelude, not even the Init .oleans will be downloaded onto your PC.

[Gabriel Ebner]

I really need to check out this nix integration more. Is it a full leanmake replacement, i.e. does the server use it as well? Can you use your own editor? How hard is it e.g. to add nix support to mathlib4?

[Sebastian Ullrich]

I was hoping you would eventually find time to check it out :grinning_face_with_smiling_eyes: . Well, the problem right now is that I don't have to work on it either, except for this super low-hanging fruit.

Is it a full leanmake replacement, i.e. does the server use it as well?

Yes, the server is pointed at a fake leanpkg that on print-paths builds and returns the .olean store paths on the fly. It even works for stage 0, where the "proper" leanpkg doesn't exist yet. The editor can't tell the difference between the two setups.

How hard is it e.g. to add nix support to mathlib4?

Until we can consume leanpkg.tomls directly, it looks like this: https://github.com/Kha/testpkg2/blob/master/flake.nix. The only onerous part is keeping the two Lean versions in leanpkg.toml and flake.lock in sync.