Zulip Chat Archive

Stream: lean4

Topic: using nix


view this post on Zulip Edward Ayers (Jan 05 2021 at 15:14):

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'

view this post on Zulip Edward Ayers (Jan 05 2021 at 15:20):

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

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 15:22):

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)

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 15:24):

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...

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 15:28):

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).

view this post on Zulip Edward Ayers (Jan 05 2021 at 15:34):

Nice I added the config and it's downloading woop

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 15:39):

Changed executable, thanks for giving it a try!

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 15:48):

And now it seems to actually work

view this post on Zulip Simon Hudon (Jan 05 2021 at 16:46):

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)

view this post on Zulip Reid Barton (Jan 05 2021 at 16:47):

that's what lean does!

view this post on Zulip Reid Barton (Jan 05 2021 at 16:47):

unlike lean 3

view this post on Zulip Simon Hudon (Jan 05 2021 at 16:47):

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

view this post on Zulip Simon Hudon (Jan 05 2021 at 16:48):

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

view this post on Zulip Reid Barton (Jan 05 2021 at 16:48):

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

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 16:48):

You're missing a main function

view this post on Zulip Simon Hudon (Jan 05 2021 at 16:50):

You're right that fixes it

view this post on Zulip Simon Hudon (Jan 05 2021 at 16:50):

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

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 16:58):

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.

view this post on Zulip Simon Hudon (Jan 05 2021 at 17:00):

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

view this post on Zulip Sebastian Ullrich (Jan 05 2021 at 17:05):

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

view this post on Zulip Zygimantas Straznickas (Jan 06 2021 at 19:31):

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?

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 19:35):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 19:37):

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.

view this post on Zulip Zygimantas Straznickas (Jan 06 2021 at 19:39):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 19:40):

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.

view this post on Zulip Zygimantas Straznickas (Jan 06 2021 at 19:52):

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?

view this post on Zulip Zygimantas Straznickas (Jan 06 2021 at 19:54):

(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)

view this post on Zulip Simon Hudon (Jan 06 2021 at 19:56):

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

view this post on Zulip Zygimantas Straznickas (Jan 06 2021 at 20:05):

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

view this post on Zulip Simon Hudon (Jan 06 2021 at 20:09):

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.

view this post on Zulip Simon Hudon (Jan 06 2021 at 20:10):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 20:12):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 20:12):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 20:13):

So flakePkgs.lean-dev should work, I think

view this post on Zulip Simon Hudon (Jan 06 2021 at 20:13):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 20:13):

In the Nix store?

view this post on Zulip Simon Hudon (Jan 06 2021 at 20:13):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 20:16):

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.

view this post on Zulip Simon Hudon (Jan 06 2021 at 20:20):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 20:22):

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

view this post on Zulip Simon Hudon (Jan 06 2021 at 20:25):

Thanks!

view this post on Zulip Simon Hudon (Jan 06 2021 at 20:25):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 20:25):

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

view this post on Zulip Zygimantas Straznickas (Jan 06 2021 at 20:40):

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

view this post on Zulip Reid Barton (Jan 06 2021 at 20:42):

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

view this post on Zulip Simon Hudon (Jan 06 2021 at 20:44):

@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?

view this post on Zulip Sebastian Ullrich (Jan 06 2021 at 20:47):

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

view this post on Zulip Zygimantas Straznickas (Jan 06 2021 at 21:06):

@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.

view this post on Zulip Zygimantas Straznickas (Jan 06 2021 at 21:09):

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.

view this post on Zulip Simon Hudon (Jan 06 2021 at 21:13):

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

view this post on Zulip Sebastian Ullrich (Jan 07 2021 at 15:33):

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

view this post on Zulip Zygimantas Straznickas (Jan 08 2021 at 02:48):

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.

view this post on Zulip Adam Topaz (Jan 08 2021 at 15:01):

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/)?

view this post on Zulip Adam Topaz (Jan 08 2021 at 15:04):

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

view this post on Zulip Adam Topaz (Jan 08 2021 at 15:41):

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).

view this post on Zulip Sebastian Ullrich (Jan 08 2021 at 16:13):

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

view this post on Zulip Adam Topaz (Jan 08 2021 at 16:17):

I see. Thanks.

view this post on Zulip Sebastian Ullrich (Jan 09 2021 at 22:10):

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

view this post on Zulip Sebastian Ullrich (Jan 10 2021 at 17:54):

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

view this post on Zulip Cyril Cohen (Jan 26 2021 at 16:09):

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?

view this post on Zulip Sebastian Ullrich (Jan 26 2021 at 16:15):

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.

view this post on Zulip Sebastian Ullrich (Jan 26 2021 at 16:33):

@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.

view this post on Zulip Cyril Cohen (Jan 26 2021 at 16:42):

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

view this post on Zulip Sebastian Ullrich (Jan 26 2021 at 17:02):

I updated our pinned Nix version just to be safe

view this post on Zulip Sebastian Ullrich (Jan 26 2021 at 17:03):

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

view this post on Zulip Zygimantas Straznickas (Feb 27 2021 at 03:30):

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

view this post on Zulip Zygimantas Straznickas (Feb 27 2021 at 03:30):

@Sebastian Ullrich

view this post on Zulip Zygimantas Straznickas (Feb 27 2021 at 04:37):

nvm, this somehow broke go-to-definition

view this post on Zulip Zygimantas Straznickas (Feb 27 2021 at 04:37):

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

view this post on Zulip Wojciech Nawrocki (Feb 27 2021 at 05:42):

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.

view this post on Zulip Zygimantas Straznickas (Feb 27 2021 at 05:52):

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

view this post on Zulip Sebastian Ullrich (Feb 27 2021 at 12:39):

Looks good to me at first glance!

view this post on Zulip Sebastian Ullrich (Feb 27 2021 at 12:54):

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

view this post on Zulip Zygimantas Straznickas (Feb 27 2021 at 17:48):

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

view this post on Zulip Zygimantas Straznickas (Feb 27 2021 at 17:50):

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.

view this post on Zulip Sebastian Ullrich (Apr 21 2021 at 11:11):

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?

view this post on Zulip Sebastian Ullrich (Apr 21 2021 at 11:12):

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:

view this post on Zulip Daniel Fabian (Apr 21 2021 at 11:14):

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

view this post on Zulip Sebastian Ullrich (Apr 21 2021 at 12:06):

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.

view this post on Zulip Sebastian Ullrich (Apr 21 2021 at 12:14):

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 ....

view this post on Zulip Daniel Fabian (Apr 21 2021 at 14:10):

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

view this post on Zulip Sebastian Ullrich (Apr 21 2021 at 15:01):

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.

view this post on Zulip Daniel Fabian (Apr 21 2021 at 16:03):

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.

view this post on Zulip Sebastian Ullrich (Apr 21 2021 at 16:46):

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

view this post on Zulip Sebastian Ullrich (Apr 21 2021 at 16:48):

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

view this post on Zulip Sebastian Ullrich (May 13 2021 at 16:27):

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 :) .

view this post on Zulip Ryan Lahfa (May 13 2021 at 17:43):

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?

view this post on Zulip Ryan Lahfa (May 13 2021 at 17:44):

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

view this post on Zulip Sam Stites (May 13 2021 at 18:10):

(deleted)

view this post on Zulip Sam Stites (May 13 2021 at 18:14):

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

view this post on Zulip Sebastian Ullrich (May 13 2021 at 18:20):

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...

view this post on Zulip Sebastian Ullrich (May 13 2021 at 18:20):

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

view this post on Zulip Sebastian Ullrich (May 13 2021 at 18:26):

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.


Last updated: May 18 2021 at 23:14 UTC