nix: buildLeanPackage vs. lakefile

Stream: lean4

[Joachim Breitner]

I have a little tool with a working lakefile.lean, depending on mathlib and other projects, and using stuff like extern_lib:
<https://github.com/nomeata/loogle/blob/fcc3a0bc01a9dad20fee2d078f0188014d250908/lakefile.lean>

Since I may want to deploy that at some time in the future, I’d like to nix’ify the build. I made a feeble attempt at using buildLeanPackage like this:

{
  inputs.nixpkgs.url = github:NixOS/nixpkgs;
  inputs.lean.url = "github:leanprover/lean4";
  outputs = { self, lean, nixpkgs }:
    let
      system = "x86_64-linux";
      pkgs = nixpkgs.legacyPackages.${system};
      leanPkgs = lean.packages.${system};
      lakePkg = leanPkgs.buildLeanPackage {
        name = "Loogle";
        src = ./.;
      };
    in
    {
      packages.${system} = lakePkg;
    };
}

But

nix build .#executable

says

error: attribute 'Mathlib.Tactic.Find' missing

       at /nix/store/m3n7ham5k637bjy1m9q599bskh2iq9jy-source/nix/buildLeanPackage.nix:199:83:

It seems that buidLeanPackage does not build on lake or at least lakefile.lean, but is an alternative to it? In particular, should I call buildLeanPackage for each dependency of my little project (e.g. mathlib)?
(Like in https://github.com/stites/templates/blob/492ffebb29b479d3ee85fa24beb214ecb227fbb0/lean4/flake.nix#L66-L88)

[Sebastian Ullrich]

Yes, they are separate, the Nix builder is older than Lake. I got it far enough to auto-translate mathlib's dependency tree https://github.com/kha/nale, but it isn't clear to me whether there is sufficient reason to continue working on that or whether a different approach should be used.

[Sebastian Ullrich]

Doing one derivation per package certainly is a no-go for mathlib, except you could cheat and make it a FOD that downloads the cache

[MangoIV]

I'm currently also searching to use nix with to import mathlib and saw this conversation.
I would like to give some input on the topic "but it isn't clear to me whether there is sufficient reason to continue working on that or whether a different approach should be used", basically as a "lessons learnt" from Haskell's build sytem story.

I'm sure this is known but there's a very big mistake that cabal did some 20 years ago, it introduced the Setup.hs file, which reverses the responsibility of the build from the build system (cabal) to the package, which can do anything at install-time.
This makes it so that the build systems gives up control and at the same time ties the ecosystem not only to legacy features of its library but also to itself. This is now causing a lot of issues, that the cabal stanza is basically "complete" and we do not really need any Setup.hs files anymore but now we're stuck with them, we cannot build any sufficiently large Haskell package without at least using Cabal the library.

If I were to choose, I would never make the choice of delegating building to the package, but always keep the control in the build system, I would probably do something like generating a lowlevel stanza which can easily be interpreted but also easily be used to create a build plan to invoke the compiler with. I guess this is similar to what you did in an adhoc way in nale but I think that the lower level stanza should be specified, such that it can also be generated by a third party (e.g. if we specify dependencies within nix instead of a lakefile)

I hope this makes a tiny bit of sense :D

[Sebastian Ullrich]

Thanks for the perspective, but that ship has thoroughly sailed with Lake, hasn't it? I included support for custom Nix overrides inside the package source in Nale as the next-best compromise I could think of.

[MangoIV]

but that ship has thoroughly sailed with Lake, hasn't it?

I feared that would be the answer

On another note, is there any usage example of how nale might be used? I see there's a lakeRepo2flake thing which I tried to use as such, but it didn't work. (no outputs are generated)

image.png

[Joachim Breitner]

I’m bindly playing around with it as well.
https://github.com/nomeata/loogle/blob/537ebbc4b8f115e6fea7f9ea3ffeab6528fcd5d5/flake.nix
and then

nix build ./#loogle --extra-substituters https://lean4.cachix.org/ --extra-trusted-public-keys lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=

but I get

~/projekte/programming/loogle $ nix log /nix/store/mvjzqimxs2q2j58nj4vpkqygkqk6vvy8-lake-export-json.drv
PANIC at Option.get! Init.Data.Option.BasicAux:16:14: value is none
backtrace:
/nix/store/9k6hadmqsqdlhakkkqka9mihy20jia38-leanshared/libleanshared.so(lean_panic_fn+0xa3)[0x7ffff79908e3]
/nix/store/b985sk3vpzpr9icps2y5jvirr038jzck-lakeexport/bin/lakeexport(_lean_main+0x368)[0x4668a8]
/nix/store/b985sk3vpzpr9icps2y5jvirr038jzck-lakeexport/bin/lakeexport[0x4680f4]
/nix/store/d2bpliayddadf6lx6l1i04w265gqw8n6-glibc-2.34-210/lib/libc.so.6(+0x29237)[0x7ffff44b1237]
/nix/store/d2bpliayddadf6lx6l1i04w265gqw8n6-glibc-2.34-210/lib/libc.so.6(__libc_start_main+0x85)[0x7ffff44b12f5]
/nix/store/b985sk3vpzpr9icps2y5jvirr038jzck-lakeexport/bin/lakeexport(_start+0x21)[0x45e411]
error: /nix/store/m961q6p1nfm7ncjw63b9k1jrwmld4l18-byffgzrmq4irvfpm0mf21y5ssr07lqks-source/lakefile.lean:21:13: error: invalid field 'nativeLibDir', the environment does not contain 'Lake.Pac>
  pkg
has type
  Package
error: /nix/store/m961q6p1nfm7ncjw63b9k1jrwmld4l18-byffgzrmq4irvfpm0mf21y5ssr07lqks-source/lakefile.lean:24:42: error: invalid field 'nativeLibDir', the environment does not contain 'Lake.Pac>
  pkg
has type
  Package
error: /nix/store/m961q6p1nfm7ncjw63b9k1jrwmld4l18-byffgzrmq4irvfpm0mf21y5ssr07lqks-source/lakefile.lean: package configuration has errors

Presumably lakeRepo2flake uses an older version of lake that doesn’t provide nativeLibDir yet?

[Joachim Breitner]

Looks like it’s not using the lake from the lean4 repo yet:

inputs.lake.url = github:leanprover/lake/lean4-master;

[Sebastian Ullrich]

Indeed, this would need adjustments

[Sebastian Ullrich]

@MangoIV Sorry, I missed your message. The intended way to use it was via a Nix plugin that provides a custom file scheme for auto-translating Lake packages to flakes, plugged into a custom version of Nix wrapped in a custom version of nix-portable: https://github.com/Kha/nale/blob/master/script/bench#L10. Very much experimental, yes.

[MangoIV]

:flushed: What’s wrong with the usual approach of generating nix files from the lean code and then using IFD?

Thank you though, I’ll have a look

[Joachim Breitner]

A nix plugin! Very fancy :-)

But won’t this make it harder to use this on CI platforms (like garnix) where you get a “stock” nix?

[Joachim Breitner]

(deleted)

[MangoIV]

@Joachim Breitner from what I gathered this is intended to be installed with a stock nix.

[MangoIV]

I e you use a stock nix to build the custom nix and then use that to build the lake file?

[Joachim Breitner]

But you won’t be able to use that easily on platforms that “provide nix”, and do the evaluation for you. Isn’t one of the promises of nix (esp. flake) that everyone can just nix run etc, them? If you have to install a custom nix, that would prevent that, woudn’t it? (but maybe I misunderstand how plugins work)

[MangoIV]

Yeah. That’s why I was a bit surprised, too, I’d rather I were able to use the usual interface. Mind that this isn’t the case with the current nix code either, try e g nix flake show, the outputs generated by buildLeanPackage don’t follow the schema.

[Joachim Breitner]

I made some progress, after commenting out all Widget related code from mathlib it is now building things.

[Joachim Breitner]

But I wonder if the use-case “deploying applications built with lean”, where per-module-incremental compilation isn’t that important, is better served by a buildRustPackage-like (or was it go?) approach (vender dependencies, then build it all at once) that treats lake as a much darker box. The audience for the tool is probably rather small, so less moving parts means less maintenance. Although at least per-package-granularity would be nice… hmm.

[MangoIV]

@Joachim Breitner there’s a very strong case for finer grained derivations, namely build caching. Given how large mathlib is I think it would be good to build things at least somewhat incremental. This is also an annoyance I have with buildRustPackage…
In my opinion nix should be a way to improve UI.

I think an approach similar to what Haskell.nix does would be really nice. Of course one would have to be careful to not make the same mistakes they did. (E g slow IFD, common compiler rebuilds, inconsistent use of modules)

[Joachim Breitner]

Absolutely!

[Joachim Breitner]

I have always wondered if a little help from the corresponding packaging tool (here lake) could go a long way for nix integration - because reimplementing too big chunks of the packaging tool logic in nix probably doesn't scale well. But I'm not sure what kind of help exactly would be needed.

[MangoIV]

I'm not sure whether this is entirely on topic with lean4 anymore but I have made up my mind about this a couple of times and I think a correct solution would be as follows

• provide an extensible project configuration stanza with common fields and custom fields similar to what dream2nix does
• provide a package-set provisioning system (read something like stackage) and a resolver (read something like the cabal resolver) tightly builtin to nix
• write small amounts of glue between a compiler and nix that plug into the realization of the build plan.
• write automatic converters from existing build plans (e.g. cabal stanzas) to that configuration stanza
• successively include the configuration stanza generation in the ecosystems s.t. they can be easily invoked and provided by a package

This would offer several improvements:

• avoid code duplication across ecosystems (resolving and package set provisioning are implemented by every package manager), this improves both the usability (more development hours because we don't have to reimplement everything) and the reusability (ecosystems will have an easy start integrating into the nix ecosystem)
• a readable and agreed upon package format that allows developers to build and understand packages and their dependencies without understanding the build tool
• trivial adoption

[Joachim Breitner]

Bold vision! I'm too pessimistic to hope that language ecosystems will use anything common, though, rather then reimplementing the wheel. And I'm not sure a common resolver is actually viable, things differ too much (versioning, flags, subcomponents, dependency algebra)

[MangoIV]

I agree it's very ambitious, but I think this could yield an actual improvement.

things differ too much (versioning, flags, subcomponents, dependency algebra)

the question is: should they? There's no fundamental difference, it's merely a choice of implementation.

[Joachim Breitner]

They shouldn't maybe, but the psychological forces are too strong, I'd say. Or would you really think that, say, the lean ecosystem would have refrained from building their own build system, package manager, doc generation, package repository - even assuming a general purpose offering would exist?

[MangoIV]

r would you really think that, say, the lean ecosystem would have refrained from building their own build system, package manager, doc generation, package repository - even assuming a general purpose offering would exist?

Well, this is also partly due to the state of the nix ecosystem and community, "outsiders" or non-nix users probably don't trust that nix can achieve what they want and they fear that this will make adoption for beginners harder (where, currently, if you're not a nix user, the latter is definitely true)

also, on:

little help from the packaging tool

that's kinda what I was trying to get at with the "intermediate representation" where lake should spit out a plan that nix can realize somewhat easily, similar to how haskell.nix generates a json plan. This would also allow specifying or overwriting custom plans from the nix side. (e.g. mathlib.src = inputs.mathlib;)

[Joachim Breitner]

So you’d imagine a nix-based build system that's used by various ecosystems? That I find even less plausible (sadly!). nix is great, but not Der Weisheits letzter Schluss, and fans of guuix and bazel and buck would certainly also good support.

The intermediate representation approach is more plausible, which then can be consumed by nix/bazel/buck etc. It could do for build systems what LSP did for editor, if a nice, narrow and general division of labor between langauge-specific build systems and nix-like systems can be found.

[MangoIV]

that's used by various ecosystems

well, I just want it to be easy for an ecosystem to adopt nix, such that it doesn't become a giant overhead that makes communities reject nix at the moment for their ecosystems

nix is great, but not Der Weisheits letzter Schluss, and fans of guuix and bazel and buck would certainly also good support.

sure, but this is not about commitment on one ecosystem but, much the opposite, making it easier to adopt nix with your ecosystem.

The intermediate representation approach is more plausible, which then can be consumed by nix/bazel/buck etc. It could do for build systems what LSP did for editor, if a nice, narrow and general division of labor between language-specific build systems and nix-like systems can be found.

yes, this is definitely more approachable and would be good enough in most cases.

[Sebastian Ullrich]

Just to clarify, the goal of Nale was to build existing Lake packages with as little setup (including of Nix) as possible. But using it as a library as part of a standard flake using standard Nix should also be feasible.

[Mauricio Collares]

The implementation of https://github.com/NixOS/rfcs/blob/master/rfcs/0092-plan-dynamism.md is moving along at a steady pace. Do dynamic derivations help here?

[MangoIV]

they will presumably make the situation around IFD a lot easier, so if we're able to get lake to spit out a format that nix can realize, this will definitely help.

[Joachim Breitner]

But using it as a library as part of a standard flake using standard Nix should also be feasible.

It’s been building mathlib for a while here already, so let’s see :-)

[Joachim Breitner]

Some success!

~/projekte/programming/loogle $ nix build ./#mathlib4 --offline
~/projekte/programming/loogle $ ls -l result/Mathlib.olean
lrwxrwxrwx 1 root root 67 Jan  1  1970 result/Mathlib.olean -> /nix/store/a32m5lhdxyi6813fmvflix66zz2w1yb3-Mathlib/./Mathlib.olean

Unfortunately, trying to build a package that depends on mathlib says

error: attribute 'Aesop' missing

       at /nix/store/146ps5dfp8n0pfmw397nzs0wv0apppnz-source/nix/buildLeanPackage.nix:199:83:

          198|              else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}";
          199|     in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap;
             |                                                                                   ^
          200|   makeEmacsWrapper = name: emacs: lean: writeShellScriptBin name ''
(use '--show-trace' to show detailed location information)

whether I pass the aesop4 flake in depFlakes or not. Odd.

Seems to be related to lean_exe, because as a lean_lib the target builds. Later more.

[Joachim Breitner]

Hmm, can't make sense of it. Building a module as a library via lakeRepo2flake, it works. Building the same .lean file as an executable via lakeRepo2flake works as well. Under the hood this uses buildLeanPackage, but I failed to call buildLeanPackage in a way that even the library builds. Tricky nix stuff…

[Joachim Breitner]

Ah, I have to use .modRoot. Ok, I can build the libray with plain buildLeanPackage now, so let’s see why .executable doesn’t work.

[Joachim Breitner]

Some more sleuthing: It seems that buildLeanPackage gets confused in allStaticLibDeps if some of the dependency flakes have extra libraries (such as AesopTest), where it then will complain about a missing Aesop. I made some progress by removing all these extra lean_libs of the dependencies, it’s building 5000 c files now. That’s what I get for writing a tool that imports mathlib :-)

[Mac Malone]

MangoIV said:

Well, this is also partly due to the state of the nix ecosystem and community, "outsiders" or non-nix users probably don't trust that nix can achieve what they want and they fear that this will make adoption for beginners harder

Unfortunately, trust is not the biggest issue here. Nix simply cannot achieve what any general purpose language wants because it does not support Windows.

[Joachim Breitner]

After a few hours of compiling, success:

~/projekte/programming/loogle $ nix run ./#loogle -- Std.Data.List.Lemmas '(List.replicate (_ + _) _ = _)'
Found 2 definitions mentioning List.replicate, HAdd.hAdd and Eq.
Of these, 1 match your patterns.

List.replicate_succ

And the binary is actually small, despite linking in all of mathlib.a. Probably link time optimization!

But I should try to make buildLeanPackage to pass only the used .o files from dependencies to the linker, no point in compiling all of mathlib if the executable only uses 4 packages.

[Sebastian Ullrich]

Ah, I probably did that so the linker cmdline size doesn't explode, but for mathlib dependents that's indeed not optimal

[Joachim Breitner]

I’m not sure I can make that change without a bigger refactoring: If I see it right, then module dependencies are in modDepsMap only for modules of the current package, so calculating the list of transitive objects isn’t quite possible yet. I’ll go with the current code for now, there are other hurdles before I can deploy loogle :-)

[Joachim Breitner]

I am currently patching mathlib to not pull in ProofWidgets, which requires some npm stuff to be run before. Such stuff is probably out of scope for buildLeanPackage for now.

Hmm, and it seems I can’t easily (without recompiling everything) patch from nix (e.g. with pkgs.applyPatches), as it changes the name of the input paths.

[Scott Morrison]

No npm should be required for ProofWidgets, if you can just use the downloadable release. (In particular, normal users of Mathlib are not expected to have npm available!)

[Joachim Breitner]

I’m trying to deploy a lean application that uses mathlib as a library with nix, where you want to build from source. So unfortunately I don’t get to claim “normal users” benefits :-)

[Scott Morrison]

But you can't just pretend the ProofWidgets zip is a "source" file? I guess I haven't drunk enough of the nix kool-aid. :-)

[Joachim Breitner]

There might be a way, but then I’d also have to figure out how to inject that into the nix-lean-buildsystem. It’s a mess. For now just patching Widgets out is a quicker way to get loogle online :-)

[Joachim Breitner]

Next hurdle taken: Replace the Alloy setup for FFI with just a plain .c file, and figured out how to build that even though the c library depends on a system library (libseccomp), both using lake and nix:

~/projekte/programming/loogle $ nix run .#loogle --  --module  Std.Data.List.Lemmas '(List.replicate (include_str "test") = _)'
Bad system call (Speicherabzug geschrieben)

Now ready to create a service, then a nixos configuration, then deploy it.

[Joachim Breitner]

Almost there, just uploading 4GB of oleans to Hetzner:

$ nixos-rebuild switch --use-substitutes --target-host root@loogle.nomeata.de --flake .#loogle --fast
…

[Joachim Breitner]

And it’s live… I think the time spend on getting this to run in nix was well worth it that I can now deploy it as simply as that.