Nix builds

Stream: lean4

[Anders Christiansen Sørby]

Are there any pressing issues with the nix integration? I'm hoping to some day add type checking and dependent types to nix. I wonder if this is something that can be solved by enabling lean to generate nix derivations.

[Sebastian Ullrich]

Pressing issues of what kind?
Dependent types for Nix sounds like a substantial project :) . Note that there is already an ongoing project developing a gradually-typed language for use with Nix, which I think is a good approach: https://github.com/tweag/nickel

[Anders Christiansen Sørby]

Something that could need collaborators or help. I have some nix experience and if there is anything that needs to be done wrt nix I may be able to help.
I've heard about Nickel and DHall, but I wonder if this is enough. Dependent types adds additional soundness options, but also a lot of complexity. The big problem with nix currently is that it is very hard to debug. I guess Nickel and Flakes solves some of this, but maybe not all.

[Anders Christiansen Sørby]

And how does the nix build relate to Lake? Does it use Lake to build Lean?

[Sebastian Ullrich]

The Nix setup is far older than Lake :) . It uses lean directly, nothing else. Mostly it is written to support my day-to-day workflows; for wider adoption Nix would first need a nicer installation experience (e.g. ship a statically built Nix executable with user-local store, elan-like) and any Windows support at all.

[Anders Christiansen Sørby]

Hm, why do you need a local store? Nix is deterministic so the store is like a hash-space kind of like IPFS (there is an integration underway). Windows support is unlikely unless someone really wants it. I like that nix is not yet-another-build-tool, but more a general framework for any deterministic build. Although it is somewhat opinionated I think this will be less relevant in the long run. I expect there to be made a sort of nix standard spec which allows all sorts of packaging tools to be binary compatible. So nix has the potential to be extremely general to the point that all software could be distributed decentralized with it.
The Lake PackageConfig could be compiled into a nix .drv expression which nix could build using lean tools. Then it could recursively build all the remaining components as their own derivations. Mostly like the nix build is already. What is not so nice is to maintain large and complicated nix expressions.

[Mac]

@Anders Christiansen Sørby While that probably would be useful for Unix users, Windows support is key for any general purpose language. Thus, Nix's lack of support for it means it cannot be the de-facto build system of Lean.

[Sebastian Ullrich]

Anders Christiansen Sørby said:

Hm, why do you need a local store?

Because installing a package manager should not (and cannot, on e.g. university machines) require root.

The Lake PackageConfig could be compiled into a nix .drv expression which nix could build using lean tools

Yes, this would be an interesting project. It should be more or less directly mappable to a buildLeanPackage call as long as it doesn't use custom rules, which most likely few packages will. Haskell shows that Nix can be quite successful as a build system even without Windows support as long as it can consume standard package formats.

[Anders Christiansen Sørby]

This should be possible to fix though. Nix is completely isolated from the rest of the system and has all it's own dependencies. The store can be moved anywhere by changing NIX_STORE env var. Root is only needed for a multi-user install. University machines could have it pre-installed as well.
Nix is more of a wrapper than a build system since it always relies on other build systems wrapped inside it's hermetic environment. I think there is no better system for multi system support.
So to have windows support only a few things needs to be fixed. Cygwin provides a unix like system to build on windows. There has been support for this previously, but it is hard to maintain with little interest. https://discourse.nixos.org/t/dropping-cygwin-support/3425 Also WSL works fine for nix already which might explain why there is little intrest to work on the Cygwin version.
Is it really easier to maintain yet another language specific build system with tons of non-reproducible dependencies? It is strange to me that this hasn't been the norm before to have reproducible builds.

[Mac]

@Anders Christiansen Sørby What do you mean by "tons of non-reproducible dependencies"? I would say the goal is for Lean builds to reproducible and have very few (and, in most cases, ideally none) external dependencies. So I would hope that most builds are reproducible.

[Sebastian Ullrich]

@Anders Christiansen Sørby Believe me, I have already thought very hard about all these questions :) . At Lean Together in January I mentioned that I would love to see Nix as Lean's package manager & version manager & build system & cloud cache at some point in the future. But due to a lack of time on my side and the experimental nature of the used/desired Nix features (flakes are still very much unstable, content-adressed store would be crucial if we get the module system), I'm happy to see Lake provide a more focused solution. But I'm far from giving up on Nix yet. Ideally, installing a (perhaps Lean-flavored) user-local Nix should be no harder than installing elan. nix-portable already comes close.

The store can be moved anywhere by changing NIX_STORE env var.

Which breaks remote caching (substitution). This can be avoided on Linux using user mount namespaces (see also nix-portable) and I believe I even have a solution for Windows (before even having a working Nix on Windows): any Windows user can map a network drive to a local directory, which is then scoped to the user. So we could map N: to $HOME\AppDataLocal\Nix or whatever and regain installation-independent paths (however, realpath seems to be able to see through the mapping, so it's a leaky abstraction). Ironically, macOS is the one platform I do not have a solution for here, not Windows.

Potentially there is a simpler solution where any derivation output that does not even reference /nix/store can be substituted into any store path, but that would need quite some work both on the Nix side and on the individual derivations of interest I believe.

University machines could have it pre-installed as well.

That could be a big ask depending on the university!

Cygwin provides a unix like system to build on windows. There has been support for this previously, but it is hard to maintain with little interest.

Yes, this is the option I'm currently exploring when I find some spare time. In the short term, it sounds much more realistic than the work on a native Nix for Windows with its on stdenv. However, there is some trouble with segfaults in Boost coroutines or something and I'm not completely convinced yet that the result will be fast enough for practical use, at least without some Windows-specific hacks to avoid some of Cygwin's overhead. If anyone else is interested in exploring that route, help would be very much welcome.

[Sebastian Ullrich]

TL;DR, there's three work items I have in mind here

• a Nix function that consumes leanpkg.toml/package.lean and translates it to a buildLeanPackage call
• a pleasant Nix wrapper that takes care of installation of Nix and uses the former function where appropriate
• whatever the shortest route to Windows support is

[Anders Christiansen Sørby]

Mac said:

Anders Christiansen Sørby What do you mean by "tons of non-reproducible dependencies"?

What I mean is that they are not content addressed bottom up which means that a lot of input and breaking changes are not explicitly given as input. So IMO Nix reproducibility is mostly two things:

• A build environment which disallows undeterministic behavior like network access.
• Content addressed dependencies which ensure that you will always get the same binaries for the same build.
  This is even better in Flakes where strict & pure mode is default.

[Anders Christiansen Sørby]

Languages keep making new build systems, but we need something universal and portable. Python has a ton of build tools and it still is a complete mess. Also all of these tools fail to address the version of the compiler and tools which also has a big impact. Then you have stuff like npm and nvm for node or rvm for ruby. This could all be solved universially with nix.

[Anders Christiansen Sørby]

If you have those two properties in any build system you are sort of already compatible with nix.
Disclaimer: I use NixOS for everything and love it.

[Anders Christiansen Sørby]

There are some nice options to root permissions here: https://nixos.wiki/wiki/Nix_Installation_Guide

[Sebastian Ullrich]

Yes, that is basically what nix-portable does. But again, not an option on macOS.

[Anders Christiansen Sørby]

I thought nix had excellent macOS support? I've never used it, but shouldn't it be easy to use non-root nix there as well?

[Sebastian Ullrich]

Haha no, macOS has been a trash fire ever since Apple started clamping down on write access to /. But what can you do without user namespaces or ptrace?

[Julian Berman]

I have a couple of friends who say they're quite successful using nix-darwin I believe? -- https://github.com/LnL7/nix-darwin (but I haven't myself gotten around to getting back to it, I have enough sustained worry from trying nix too early on in its development that I've still put it off)

[Mac]

Anders Christiansen Sørby said:

Languages keep making new build systems, but we need something universal and portable. ... Then you have stuff like npm and nvm for node or rvm for ruby.

I suspect the reason why each language keeps inventing its own "build system" (while copying ideas from others) is that each language has very different notions of what its "build system" needs to do. In fact, a lot of projects in interpreted languages don't even do any building. Thus, I would talk more generally about their "management systems", which can often be split into some major components:

• A toolchain/version manager: nvm for Node, phpenv for PHP, rvm for Ruby, venv for Python, rustup for Rust, stack for Haskell, elan for Lean
• A package manager : npm/yarn for Node, composer for PHP, gem for Ruby, pip/poetry for Python, cargo for Rust, cabal/stack for Haskell, leanpkg/lake for Lean, apt for Linux, brew for MacOS, winget/choco/scoop for Windows, pacman for Arch Linux / Windows MSYS2
• A script manager: npm/yarn for Node, rake for Ruby, stack for Haskell, lake for Lean
• A build system: webpack/gulp for Node/JavaScript, rake for Ruby, setuptools for Python, cargo for Rust, cabal/stackfor Haskell, leanpkg/lake for Lean, cmake for C/C++, make/shake/bazel/nix (hopefully lake eventually) for general builds
• An interactive environment: node for Node, irb for Ruby, ipython/jupyter for Python, ghci for Haskell, VSCode/Emacs/etc. + the LSP server for Lean

As you can see, some languages have some of these components and others do not (though newer or long lived languages tend to acquire many of them). There is also substantial overlap in some cases an not in others. In many cases, there are good reasons for this.

For example, languages like C and C++ tends to overlap with the system's package manager because they install and use binaries/libraries that are system-specific and may, in turn, be used by the system directly, but interpreted languages often do not because their packages are specific to their language toolchain instead of the ABI of the OS. Purely compiled languages (e.g., Rust) also don't have scripting systems or interactive environments because there is no such concept. Conversely, having such things is a major boon to interpreted languages like Python and Lean.

Furthermore, in Lean, there is a strong overlap between the said interactive environment and management system. It is entirely reasonable for the LSP server to potentially ask the system to fetch a remote resource, build a target, extract configuration options and vice versa. Thus the absence of a sandboxed environment (e.g., like bazel's) along nondeterminism in the system is perfectly reasonable in some cases. On the other hand, when simply building a native library or binary for Lean, such things may be desired (which is why such features are so popular in systems designed to do just that). The ability to support both these use cases is why having a Lean-specific system is useful. Such flexibility is also why most other languages have system, because they have there own requirements on the system.

On the other hand, if you simply want to inject Lean into a larger multi-layered project, a more general build system (like Nix) may be more desirable for the overarching project. Thus, that is why creating bridges between the two is still something we would like to do.

[Mac]

One other thing to consider is that, for Windows users and developers who prefer GUIs over CLIs, you will also want visual interface support for the system, which Nix may also lack.

[Anders Christiansen Sørby]

This shouldn't be a problem with using nix. Non-determinism can always be solved by separating the build into pinned inputs and outputs from builds. All of these tools solve very similar problems. I think with all the overlaps it makes sense to have a unified tool. Nix makes essentially zero assumptions about the structure of an underlying build system.

[Mac]

@Anders Christiansen Sørby Sure, any sufficiently general system can be adapted, with effort, to fit a given task. The question is simply whether there is the time and desire to do so. If want to get Nix functioning as general purpose build system for Lean, feel free to try.

Personally, when it comes to languages, I would much prefer that all the tools written for the language are, to the greatest possible extent, written in said language, which is why I proposed and built Lake. For these same reasons, nix would thus never be the build tool of choice for someone like me. However, I could certainly see adapting it's approach and the lessons it learned to build systems like Lake in languages like Lean.

[Anders Christiansen Sørby]

Actually I agree. Tools for a language should be written in that language, and nix should be able to support that. The nix language is not very nice IMO, but it mostly is a script to generate content addressed .drv files. This can be done by any other language as well. The drv files are then executed by the nix-daemon. I think nix should evolve into a system where you can use your language of choice which implements the nix spec.

[Daniel Fabian]

@Anders Christiansen Sørby also, for context, lake stems from the idea to have something like fake (F# make) for lean. The notion of having a core dependency resolving mechanism couple with easy-to-extend written in the same language helper tasks is meant to invite outside contributions.

The lake community is fairly small and making it easier for the people interested in lean to contribute is an important goal if we want long-term survival of lake.

When we were discussing whether or not writing a build system was a good idea at all, at least the following points were quite important:

• cross platform; whilst academia is maybe a bit more unix-oriented than the rest of the industry, you most likely still have well over 50% of users use windows. This one disqualifies nix almost entirely.
• few dependencies; we could have used fake for instance. But then we'd need .net core just to build and that felt wrong on quite a few levels. As it stands, lean comes with fairly minimal dependencies.
• extendable; this meant, it would ideally be written in lean or allow for extensions to be written using lean
• cloud build / caching; since in lean a lot of time goes into compilation, having support for efficient rebuilds becomes much more important. And in fact, with mathlib, you really want to cache builds and even avoid building at all on a fresh machine.
• installable without admin access: for universities we don't expect people to have admin access in general which e.g. makes WSL2 problematic.

Nix would have ticked a few of the boxes, but not others.

Finally, at least for the time being, we have relatively few packages that are big as opposed to a multitude of small packages like npm. So at least for now, build scripts vs. versioned packages are more important. This obviously may change in future and maybe at some point spitting out a .drv may be a fine option. But that is not something that will happen in a few months.

In the mean time nix could possibly come up with a solid windows story and or a solid mac story. And then we could reconsider some of the choices we made so far.

That said, nix is quite old getting close to 20 years and we still don't have a solid cross-platform story or content-addressable storage. Whilst I love nix and nixos, it is a complex beast (building a whole linux distro in a single build script is no small feat) and it doesn't have too much industry support. If some of the big tech companies took a big bet on nix and poured in resources, some of those many year old issues could be addressed much more quickly. As it stands, nix is unfortunately really good at the things it's doing with a community that's focused around nixos and cloud deployment, but not very strong on the cross-platform story. Part of it comes down to nix driving backend services where lack of reproducibility is much more painful than desktops. Another reason, I believe, is that cross-platform support is genuinely hard if you start with nothing and build the whole tool chain from scratch, so there's a lot of work.

Personally, I wouldn't expect a great cross-platform story for years to come, unfortunately. And that's not a timeframe we would want to target with a build system for lean, if that makes sense.

[Henrik Böving]

Are there any plans to have a tool similar to doc-gen from mathlib integrated with lake? Similar to how e.g. rustdoc is integrated with Cargo in the Rust eco system.

[Daniel Fabian]

@Henrik Böving the idea around the design is that any kind of tool like that would ideally be integrated using just a few lines of lean code to define a new task. You'd write a wrapper that wraps the doc-gen and then lake could drive it.

I don't know if @Mac has it on his radar at the moment, but that's exactly the kind of thing, I think the community could easily provide and upstream if not.

[Anders Christiansen Sørby]

@Daniel Fabian What I'm advocating is really just satisfying two properties:

• Content addersed builds and dependencies.
• Deterministic builds.
  Supporting this in Lake shouldn't be too difficult and it would make nix support trivial. Most of the complexity in nix comes from working around that other build systems doesn't support these properties.

[Daniel Fabian]

yeah, that makes sense. And I think we kind of plan doing it. @Mac has been following the Build systems à la carte paper. The features we wanted IIRC would be equivalent to cloud shake from the paper.

[Christian Pehle]

I think an important feature not typically covered by build systems is the "workspace" and "hermiticity / reproducibility" concept present in blaze, Bazel, Buck, Pants, Please, gn. Workspaces give you the ability to have multiple projects share the same build infrastructure and hermiticity/reproducibility enforces that you can't call arbitrary shell scripts, system installed binaries, link to system libraries, that have not been declared explicitly. Language specific package managers and build systems often throw up their hands in the air as soon system library dependencies or FFI are involved and packages then resort to brittle (shell) scripts. Pip, cabal, opam all have that issue.

[One An]

hello, I'm a bit stuck on installing lean 4. I followed all the steps but when I checked to see if the eval command was working, it wasn't and I got this error message "command 'lean4.displayGoal' not found." Is there a fix to this?

[One An]

oh wait should i have asked in the new members stream?

[Sebastian Ullrich]

Fittingly, the main author of Shake has recently posted three blog posts reflecting on Shake: https://neilmitchell.blogspot.com/ (start with the third one from the top)

[Mac]

Daniel Fabian said:

Henrik Böving the idea around the design is that any kind of tool like that would ideally be integrated using just a few lines of lean code to define a new task. You'd write a wrapper that wraps the doc-gen and then lake could drive it.

I don't know if Mac has it on his radar at the moment, but that's exactly the kind of thing, I think the community could easily provide and upstream if not.

There are two different these would be conceptually done this in Lake. Either it could be implemented as a "script" (a concept aped from npm) where you can specify some arbitrary function of type (args : List String) -> IO Unit indexed by a String key than can be executed by Lake via lake run <key> -- [<args>...]. Alternatively you could treat documentation generation as proper build and defined a custom build target for it (though support for running these separately from the package build has not yet been added to Lake).

[Mac]

@Sebastian Ullrich I found the post of "Forward Build Systems" interesting, especially so, since I have a counter-intuition about it. Linking/Loading would be the first thing I would think of when talking about compiling a C program to a binary. I guess my intuition is naturally backwards (i.e., I think of a result and how to get to it -- not first of a source and then how to reach a given destination).

Though, now that I think about it, the forward/backward approach in build systems has strong parallels between the forward and backward proof styles (represented by tactic and term proofs respectively in Lean). I wonder if their would be some way to adapt how tactics and goals work to a forward build system. Actually, I wonder if one wrote a build target through a by if it would already result in a forward build system?

[Mac]

I
Christian Pehle said:

I think an important feature not typically covered by build systems is the "workspace" and "hermiticity / reproducibility" concept present in blaze, Bazel, Buck, Pants, Please, gn. Workspaces give you the ability to have multiple projects share the same build infrastructure and hermiticity/reproducibility enforces that you can't call arbitrary shell scripts, system installed binaries, link to system libraries, that have not been declared explicitly. Language specific package managers and build systems often throw up their hands in the air as soon system library dependencies or FFI are involved and packages then resort to brittle (shell) scripts. Pip, cabal, opam all have that issue.

The concept of "workspaces" is on my todo list. For the "hermiticity/reproducibility", one of the great things about writing a build system in a functional language is that such things could potentially be resolved by providing a more restrict monad to perform builds in, which I hope Lake will eventually support more fully.

[Mac]

Anders Christiansen Sørby said:

Daniel Fabian What I'm advocating is really just satisfying two properties:

• Content addressed builds and dependencies.
• Deterministic builds.

Supporting this in Lake shouldn't be too difficult and it would make nix support trivial. Most of the complexity in nix comes from working around that other build systems doesn't support these properties.

As far as I am aware, Lake does support content addressed builds and dependencies. Once #659 l lands in production Lean, a Lake basic build will be fully content addressed and deterministic (as the toolchain will be precisely determined by the commit hash of Lean). Only builds that rely on external resources (i.e., libraries/external binaries) will not be. Those however, could still be made content-addressable by converting such resources into targets as well.

[Anders Christiansen Sørby]

The zig cc builds look nice, but are they content addressed on the hash of the compiler as well as all input variables and configuration?
I made a PR where I've added a nix flake to the lake repo btw https://github.com/leanprover/lake/pull/15 .
This way lake can be loaded with nix run github:leanprover/lean.

[Anders Christiansen Sørby]

@Sebastian Ullrich I'm wondering how to use the buildLeanPackage function for including FFI bindings to c-libraries (compiled/source/shared/static). How would I link arbitrary libraries to a Lean module? It seems for now you need to put a c src file in the same directory and with the same name as the lean module to be able to compile it using the normal setup. Is it possible to link to an arbitrary c-library with this setup or do I need to make modifications?

[Sebastian Ullrich]

If you compile the C code into a static archive independently from the Lean setup, you should be able to pass it to buildLeanPackage's linkFlags parameter

[Anders Christiansen Sørby]

That was my plan. Are the linkFlags which are sent to leanc the same as gcc link flags?

[Sebastian Ullrich]

Yes, leanc is just a simple wrapper around ccache + clang!

[Anders Christiansen Sørby]

nix flake check fails on master because lean-packages does not only contain derivations which is the flakes convention. I think it would be a good idea to follow these flake standards. This is unstable and standardized features though. Do you think it would be worthwhile to fix this setup so that nix flake check runs successfully?

[Sebastian Ullrich]

We have many nested derivations such mods, I don't see how to restructure that other than making the root a fake derivation. Nixpkgs has many of these as well, so I'm not sure how this restriction is supposed to work out in practice.

[Sebastian Ullrich]

Some exciting development on the "wrap foreign package managers in Nix" front btw
https://github.com/NixOS/rfcs/pull/92#issuecomment-939203270
https://github.com/DavHau/dream2nix

[Anders Christiansen Sørby]

The nix build buildLeanPackage is broken on the newest lean. I get this error

> clang-13: error: no such file or directory: '/nix/store/491141g8sk8rhgs3vxf68nhwr2bg54xm-Blake3-c/Blake3.c'

[Sebastian Ullrich]

$ nix flake update
warning: updating lock file '/home/sebastian/lean/lean/lean-blake3/flake.lock':
• Updated input 'lean':
    'github:leanprover/lean4/a741a3dfd422143a445127af67fa8c5f1f59a892' (2021-10-22)
  → 'github:leanprover/lean4/9fc0cd0555d517b473aee7460dd150a9cabab797' (2021-10-26)
$ nix build .#tests
...
lean: symbol lookup error: /nix/store/32pxmag2l6rv73sky9pafp0yfadyfgyw-Blake3.so/Blake3.so: undefined symbol: blake3_version

[Anders Christiansen Sørby]

It was my changes which caused it. I'd added a -v flag to lean

[Anders Christiansen Sørby]

Which library contains lean_register_external_class and where do I find it in nix?

[Henrik Böving]

According to nm it seems to be in ~/.elan/toolchains/leanprover--lean4---nightly-2021-10-22/lib/lean/libleanshared.so

λ nm lib/lean/libleanshared.so | grep lean_register_external_class
0000000002836750 T lean_register_external_class

on elan based installations, no idea about nix though

[Sebastian Ullrich]

There is a leanshared attribute

[Anders Christiansen Sørby]

Ok, that fixed an issue, but I'm still getting:

> could not find native implementation of external declaration 'Blake3.internalVersion' (symbols 'l_Blake3_internalVersion___boxed' or 'l_Blake3_internalVersion')

Where exactly does the Lean interpreter look for native symbols when building lean source?

[Sebastian Ullrich]

       RTLD_DEFAULT
              Find  the  first  occurrence  of the desired symbol using the default shared object search order.
              The search will include global symbols in the executable and its dependencies, as well as symbols
              in shared objects that were dynamically loaded with the RTLD_GLOBAL flag.

This includes lean and its dependencies as well as any LD_PRELOAD libraries, but not --plugin libraries

[Anders Christiansen Sørby]

That is strange because I have included all the dependencies in LD_PRELOAD.
I guess this code does the lookup?

```c
void * lookup_symbol_in_cur_exe(char const * sym) {
#ifdef LEAN_WINDOWS
HMODULE hmods[128]; // 128 modules should be enough for everyone
DWORD bytes_needed;
lean_always_assert(EnumProcessModules(GetCurrentProcess(), hmods, sizeof(hmods), &bytes_needed));
for (int i = 0; i < bytes_needed / sizeof(HMODULE); i++) {
void * addr = reinterpret_cast<void *>(GetProcAddress(hmods[i], sym));
if (addr) {
return addr;
}
}
return nullptr;
#else
return dlsym(RTLD_DEFAULT, sym);
#endif
}

[Sebastian Ullrich]

A link would be sufficient :) ...

[Anders Christiansen Sørby]

I tried adding the lean generated Blake3.so to the LD_PRELOAD and I've now upgraded my linking error into a segfault. What am I doing wrong?

[Sebastian Ullrich]

That might be progress...? Do you have a stack trace?

[Sebastian Ullrich]

You might be interested in https://github.com/leanprover/lean4/pull/751 btw

[Anders Christiansen Sørby]

How do I produce a stack trace from this?

> bash: line 7:     7 Segmentation fault      (core dumped) lean -o $out/$oleanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags

[Anders Christiansen Sørby]

Is there a way to run the compilation from inside gdb or something?

[Sebastian Ullrich]

You should be able to run gdb + that command in nix develop as in https://leanprover.github.io/lean4/doc/make/nix.html#other-fun-stuff-to-do-with-nix, thought you might need to drop the -o/-c output parameters

[Anders Christiansen Sørby]

gdb debugging is not so easy. To use LD_PRELOAD I need to have all the dependencies of lean loaded in that path. This might be what is causing the issue. libleanshared.so is compiled with GLIBC_2.33 which is available on nixpkgs unstable.

[Sebastian Ullrich]

Yeah, LD_PRELOAD is pretty evil all in all. You could try leanprover/lean4#752 instead.

[Sebastian Ullrich]

But that shouldn't cause a segfault

[Anders Christiansen Sørby]

It is good for it's purpose which is to override arbitrary library functions, but it is bad for dealing with entire libraries with lots of dependencies.

[Anders Christiansen Sørby]

I tried to use your --load-dynlib setup, but I still get a segfault. Maybe it has something to do with my C shim idk. Any tips on debugging?

[Sebastian Ullrich]

Do you have a stack trace now?

[Anders Christiansen Sørby]

#0  0x00007ffff53e8baa in raise () from /nix/store/2jfn3d7vyj7h0h6lmh510rz31db68l1i-glibc-2.33-50/lib/libc.so.6
#1  0x00007ffff53d3523 in abort () from /nix/store/2jfn3d7vyj7h0h6lmh510rz31db68l1i-glibc-2.33-50/lib/libc.so.6
#2  0x00007ffff5cf13c9 in __gnu_cxx::__verbose_terminate_handler() [clone .cold] () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#3  0x00007ffff7b1ac26 in __cxxabiv1::__terminate(void (*)()) () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#4  0x00007ffff7b1ac91 in std::terminate() () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#5  0x00007ffff7b1ade4 in __cxa_throw () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#6  0x00007ffff79f343e in load_library(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >) () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#7  0x00007ffff79f46e4 in lean_main () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#8  0x00007ffff53d4780 in __libc_start_main () from /nix/store/2jfn3d7vyj7h0h6lmh510rz31db68l1i-glibc-2.33-50/lib/libc.so.6
#9  0x000000000040106a in _start () at ../sysdeps/x86_64/start.S:120

from gdb

[Sebastian Ullrich]

Hmm, that looks like a regular abort from an uncaught exception to me, not a segfault

[Anders Christiansen Sørby]

Maybe I didn't reproduce it properly
I used this command --load-dynlib=/nix/store/4m6n7rzgnqal7cfcb1lq9vy9m9v4p5wq-libleanblake3.so src/Blake3.lean

[Anders Christiansen Sørby]

Oh, my bad. I wrote the wrong path

[Sebastian Ullrich]

From your master I get

$ nix develop /nix/store/ih1ibncr3wi47rl47756wxk1kd7akj05-Tests.HashString.drv
> leanPath=Tests/HashString.lean gdb --args lean -o $out/$oleanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags $leanLoadDynlibFlags
GNU gdb (GDB) 10.2
...
Reading symbols from lean...
(gdb) r
Starting program: /nix/store/2wjddx5f2b3ivh19napvk408br1y8ggs-lean/bin/lean -o /home/sebastian/lean/lean/lean-blake3/outputs/out/Tests/HashString.olean -c /home/sebastian/lean/lean/lean-blake3/outputs/c/Tests/HashString.c Tests/HashString.lean --load-dynlib=/nix/store/ls84fmli14gfjhw7j6wb0d4bylkc269k-Blake3.so/Blake3.so --load-dynlib=/nix/store/dblpwlsrvyh9cp55kx9wkaq8wf73m0zl-libblake3.so/libblake3.so --load-dynlib=/nix/store/kysihyv6mdi58z2yrn7gia4cqp16l3ni-libleanblake3.so/libleanblake3.so --load-dynlib=/nix/store/nzki9k7ragvdjmg8x3zlncfnzdx56s6v-Lean.so/Lean.so --load-dynlib=/nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
...
Program received signal SIGSEGV, Segmentation fault.
0x00007ffff5dade10 in l_String_isEmpty () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
(gdb) bt
#0  0x00007ffff5dade10 in l_String_isEmpty () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#1  0x00007ffff5da59e3 in l_instReprString___boxed () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#2  0x00007ffff7b001f6 in lean_apply_2 () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#3  0x00007ffff5e62f4c in l_Lean_instEval__1___rarg___boxed () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
...
#59 0x00007ffff64dd119 in lean_run_frontend () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#60 0x00007ffff79f54e9 in lean::run_new_frontend(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, lean::options const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, lean::name const&) () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#61 0x00007ffff79f7700 in lean_main () from /nix/store/di5rqi13gq56w4sai26qpin4i3ikwfhv-leanshared/libleanshared.so
#62 0x00007ffff53d6780 in __libc_start_main () from /nix/store/2jfn3d7vyj7h0h6lmh510rz31db68l1i-glibc-2.33-50/lib/libc.so.6
#63 0x000000000040106a in _start () at ../sysdeps/x86_64/start.S:120

[Sebastian Ullrich]

Looking at the shared libs, it is worrying that the seem to statically link against Lean:

$ ldd /nix/store/ls84fmli14gfjhw7j6wb0d4bylkc269k-Blake3.so/Blake3.so
    linux-vdso.so.1 (0x00007fff8553d000)
    libgmp.so.10 => /nix/store/fnd1kz8wzv3bj7nwm07yn828vwh0ayfp-gmp-6.2.1/lib/libgmp.so.10 (0x00007fe599b60000)
    libdl.so.2 => /nix/store/2jfn3d7vyj7h0h6lmh510rz31db68l1i-glibc-2.33-50/lib/libdl.so.2 (0x00007fe599b5b000)
    libpthread.so.0 => /nix/store/2jfn3d7vyj7h0h6lmh510rz31db68l1i-glibc-2.33-50/lib/libpthread.so.0 (0x00007fe599b3b000)
    libc.so.6 => /nix/store/2jfn3d7vyj7h0h6lmh510rz31db68l1i-glibc-2.33-50/lib/libc.so.6 (0x00007fe599976000)
    /nix/store/2jfn3d7vyj7h0h6lmh510rz31db68l1i-glibc-2.33-50/lib64/ld-linux-x86-64.so.2 (0x00007fe599e2b000)
$ nm /nix/store/ls84fmli14gfjhw7j6wb0d4bylkc269k-Blake3.so/Blake3.so | grep l_String_isEmpty  # not the culprit symbol, just an example
00000000001165d0 T l_String_isEmpty
00000000001165e0 T l_String_isEmpty___boxed

Duplicate data symbols can lead to issues like this one. This might be an issue with the current buildLeanPackage.

[Sebastian Ullrich]

Specifically, sharedLib should probably use a dynamic analogue to allStaticLibDeps

[Anders Christiansen Sørby]

I didn't know I could use nix develop like that. Really neat.
So I should remove the static links from the Blake3.so lib build?

[Sebastian Ullrich]

Ah, I see you've already tried to link Blake3.so against libleanshared.so. But it doesn't seem to be working.

[Anders Christiansen Sørby]

What I find strange about this stack trace is that none of the calls are from any of the imported libraries. Might this be a problem from within the lean ir system itself?

[Sebastian Ullrich]

It would be great if debugging segfaults was that straightforward. But the bad object is probably from a prior callchain in Blake3.so.

[Sebastian Ullrich]

It would be possible to check that with a debug build of Lean and the rr reverse debugger, but Blake3.so not linking against libleanshared.so is definitely a/the problem.

[Anders Christiansen Sørby]

I would guess it has something to do with the blake3_version call not returning a valid pointer to the version string.

[Anders Christiansen Sørby]

Hm, I tried to replace the call with a string litteral, but no change so hypothesis invalidated i guess?

[Anders Christiansen Sørby]

If I comment out the eval the build works fine. Is eval run by the IR interpreter?

#eval Blake3.version
#eval (hash "hello".toByteArray)

[Sebastian Ullrich]

It is

[Anders Christiansen Sørby]

So it might work nicer if these calls were from inside a main function?

[Sebastian Ullrich]

Depending on how it's linked yes

[Anders Christiansen Sørby]

Moving it inside main gives this

tests> /nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/wd0xrfazq2imw3xlh96p0aqf4dp6bvh1-Blake3-cc/Blake3.o: in function `l_Blake3_internalVersion___boxed':
tests> /nix/store/2pr0x2fydifarj2x6fb6xg1gl2mnxkdh-Blake3-c/Blake3.c:211: undefined reference to `lean_blake3_version'
tests> /nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/wd0xrfazq2imw3xlh96p0aqf4dp6bvh1-Blake3-cc/Blake3.o: in function `l_Blake3_initHasher___boxed':
tests> /nix/store/2pr0x2fydifarj2x6fb6xg1gl2mnxkdh-Blake3-c/Blake3.c:236: undefined reference to `lean_blake3_initialize'
tests> /nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/wd0xrfazq2imw3xlh96p0aqf4dp6bvh1-Blake3-cc/Blake3.o: in function `l_Blake3_hasherUpdate___boxed':
tests> /nix/store/2pr0x2fydifarj2x6fb6xg1gl2mnxkdh-Blake3-c/Blake3.c:246: undefined reference to `lean_blake3_hasher_update'
tests> /nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/wd0xrfazq2imw3xlh96p0aqf4dp6bvh1-Blake3-cc/Blake3.o: in function `l_Blake3_hasherFinalize___boxed':
tests> /nix/store/2pr0x2fydifarj2x6fb6xg1gl2mnxkdh-Blake3-c/Blake3.c:256: undefined reference to `lean_blake3_hasher_finalize'
tests> /nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/wd0xrfazq2imw3xlh96p0aqf4dp6bvh1-Blake3-cc/Blake3.o: in function `l_Blake3_hash':
tests> /nix/store/2pr0x2fydifarj2x6fb6xg1gl2mnxkdh-Blake3-c/Blake3.c:332: undefined reference to `lean_blake3_hasher_update'
tests> /nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/2pr0x2fydifarj2x6fb6xg1gl2mnxkdh-Blake3-c/Blake3.c:334: undefined reference to `lean_blake3_hasher_finalize'
tests> /nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/wd0xrfazq2imw3xlh96p0aqf4dp6bvh1-Blake3-cc/Blake3.o: in function `_init_l_Blake3_version___closed__1':
tests> /nix/store/2pr0x2fydifarj2x6fb6xg1gl2mnxkdh-Blake3-c/Blake3.c:220: undefined reference to `lean_blake3_version'
tests> /nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/wd0xrfazq2imw3xlh96p0aqf4dp6bvh1-Blake3-cc/Blake3.o: in function `_init_l_Blake3_hash___closed__1':
tests> /nix/store/2pr0x2fydifarj2x6fb6xg1gl2mnxkdh-Blake3-c/Blake3.c:274: undefined reference to `lean_blake3_initialize'

[Anders Christiansen Sørby]

I guess --load-dynlib is not enough for this case?

[Sebastian Ullrich]

It's not, --load-dynlib does not affect compilation at all

[Anders Christiansen Sørby]

Ok, I tried adding both as staticLibDeps and got this:

tests> /nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/8wr1184878xvqqs76kplgljidfi38m1z-libleanblake3.a/libleanblake3.a(blake3-shim.o): in function `lean_blake3_initialize':
tests> blake3-shim.c:(.text+0xd7): undefined reference to `blake3_hasher_init'
tests> /nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/8wr1184878xvqqs76kplgljidfi38m1z-libleanblake3.a/libleanblake3.a(blake3-shim.o): in function `lean_blake3_hasher_update':
tests> blake3-shim.c:(.text+0x211): undefined reference to `blake3_hasher_update'
tests> /nix/store/fp2h123793bxln4cjxy0mz08sf4nx2m3-binutils-2.35.1/bin/ld: /nix/store/8wr1184878xvqqs76kplgljidfi38m1z-libleanblake3.a/libleanblake3.a(blake3-shim.o): in function `lean_blake3_hasher_finalize':
tests> blake3-shim.c:(.text+0x3ef): undefined reference to `blake3_hasher_finalize'

[Sebastian Ullrich]

I can't help you without more information, but clearly you're not linking against the library with these symbols

[Anders Christiansen Sørby]

Ok, I'll try some more.

[Anders Christiansen Sørby]

I got it working inside main with proper linking! Though not inside #eval yet.

[Anders Christiansen Sørby]

So I made my edits on the nix build into a PR https://github.com/leanprover/lean4/pull/763
This adds a way to automatically and recursively link against native shared libs

[Anders Christiansen Sørby]

I wanted to use lake in the beginning, but for me it was very much not plug and play compared to using nix. (I'm using NixOS).
@Mac No doubt lake & lean is content addressed for some things like the git hashes. But this is also dependent on the actual lean binary command and the libraries it was using at the time. So the output should ideally also be hashed. For now lake is more like Cargo or pip which are very sensitive to what kind of input and config given to the tool. Also nix disallows internet access during build which ensures that it is always an input -> output build. Not that lake isn't a good tool. If possible I would want to ba able to generate drv files from something lake like and push that to the nix build daemon.
@Gabriel Ebner The nix build _can_ cache between systems and architectures. If not you need to split up the derivation steps or there is some irrelevant input that does not affect the output. Since everything is cached on hash in hash out I think only the last step needs to be done for each architecture (olean -> o).

[Mario Carneiro]

Anders Christiansen Sørby said:

Gabriel Ebner The nix build _can_ cache between systems and architectures. If not you need to split up the derivation steps or there is some irrelevant input that does not affect the output. Since everything is cached on hash in hash out I think only the last step needs to be done for each architecture (olean -> o).

Forgive my ignorance, but if I understand Nix right, if the olean was generated using build data from a linux x86 then you can't use it on a mac because the build inputs are different, even if the output would be (pinky promise) bit-identical if actually carried out.

A separate issue is that the output is most likely not bit identical in lean 4, unlike lean 3 where the data to store is mostly platform agnostic (I don't think this was on purpose, but it turned out to be true and really useful). In lean 4 there are memory mapping tricks being done that make the olean files at least endian-dependent and probably also contain local file paths and things of that nature

[Gabriel Ebner]

Luckily all architectures that we care about are 64-bit and little-endian (amd64, aarch64, riscv). As long as we keep all the OS-dependent stuff to C files, we should be fine.

[Sebastian Ullrich]

Except for wasm32, that is :)

[Gabriel Ebner]

Even if we wanted to support obscure 32-bit architectures (like wasm), I think it would be easier to write a 64-bit-to-32-bit olean converter than to compile mathlib twice.

[Mario Carneiro]

maybe I need to dust off the olean parser after all...

[Gabriel Ebner]

Feel free to be inspired by https://github.com/gebner/oleanparser

[Mario Carneiro]

I see you are two steps ahead of me. Would this work for parsing a non-native olean file?

[Gabriel Ebner]

Yes, it can parse 64-bit little-endian oleans on any platform.

[Sebastian Ullrich]

Depending on how important this use case will be, I think it would make sense to make Lean a native .olean cross compiler

[Gabriel Ebner]

If we want to support multiple platforms, it would be great to have endianness and bitsize included in the header.

[Mario Carneiro]

it would be great if olean was, like, an actual format and not "whatever lean happens to produce today"

[Mario Carneiro]

I would love to be able to target an external verifier on oleans directly

[Gabriel Ebner]

Since oleans are mmapd, they need to have the same object layout as lean. This means that the format shouldn't be stable (we want to be able to change Lean's object layout if we need to). But we could put in a version number and have documentation for the current format.

[Mario Carneiro]

(this goal is not mutually exclusive with having efficient mmap style import, there are plenty of binary formats with ABI compatibility in the linux space)

[Mario Carneiro]

and like you say, a version number can be used to paper over abi breaks

[Sebastian Ullrich]

Note that all data types used in environment extensions also become part of the olean ABI

[Mario Carneiro]

you can leave space for extensions

[Mario Carneiro]

as long as Expr can be read, that's probably good enough for a verifier

[Mario Carneiro]

I guess that extensions using extern are not self-describing? Is it possible to know the type layout of such things or do you just have to be prepared for anything?

[Gabriel Ebner]

You also want Name and Expr.Data and Environment, etc. The Lean 4 oleans are really just serialized VM objects.

[Mario Carneiro]

Do externs have type tags that could at least in principle be used to look them up in a schema?

[Gabriel Ebner]

You can read the schema for the relevant part of the olean file here:
https://github.com/leanprover/lean4/blob/f01a124f187793cdf09788b0cc102eba156b1c60/src/Lean/Environment.lean#L500-L505

[Gabriel Ebner]

/- Content of a .olean file.
   We use `compact.cpp` to generate the image of this object in disk. -/
structure ModuleData where
  imports    : Array Import
  constants  : Array ConstantInfo
  entries    : Array (Name × Array EnvExtensionEntry)

[Gabriel Ebner]

As you can see, there's names for the extensions ^^

[Mario Carneiro]

That sounds like enough to make it work, although a consistent naming scheme for the extensions has to be coordinated somehow

[Mario Carneiro]

are closures or other code precompiled in oleans?

[Sebastian Ullrich]

Closures cannot be serialized if you mean that

[Sebastian Ullrich]

As to the actual topic title...
Gabriel Ebner said:

one could simply tell Nix "yeah, this derivation for macOS will definitely be realised into this store path produced by the Linux derivation, just trust me on that"

I don't think such an option would ever make it past Eelco. He's already super unhappy about the cargo-vendor stuff (i.e., that we use a fixed-output derivation for the automatically generated vendor directory, instead of checksums for the individual upstream tarballs). Intentional impurity seems even less likely to be accepted.

If we were to seriously invest in Nix infrastructure and e.g. shipped a custom Nix wrapper, maintaining a (hopefully small and backwards-compatible) fork of Nix would be inevitable I think. But for this hack specifically... all we should need is access to the sqlite DB, it should be doable in a hacky script completely outside of Nix.

[Sebastian Ullrich]

I'm mostly thinking of small enhancements like https://github.com/NixOS/nix/pull/5324 that might not be as important to upstream as to our use case

[Anders Christiansen Sørby]

@Mario Carneiro If the build depends on system when it is not actually relevant I would call that a bug. For me nix is more of an ideal that has yet to mature properly. I only see benefits from hermetic and content addressed builds. The problem is that the current tooling does not really satisfy these properties. This could be made much more ergonomic and integrated than what nix currently supports, but what nix is already doing is really impressive.
I've started toying with translating hnix to a Nix.lean which could support interoperability.

[Sebastian Ullrich]

How should Nix know/verify that two different binaries for two different platforms using slightly different build scripts are semantically equivalent? You are asking for something that Nix cannot provide within its guarantees. Thus the "trust me, Nix" part of the hack.

[Anders Christiansen Sørby]

Well if the build scripts are really different then yes, but why should they be when they are supposed to produce the same output?

[Sebastian Ullrich]

I mean the scripts generating the Lean binary. Please see for yourself how many platform-specific branches we have in our CMake files.

[Anders Christiansen Sørby]

This may be really hard and a lot of work, but there should be a way to decompose all the steps of the build in a cachable and minimal inputs way.

[Anders Christiansen Sørby]

But that should only be relevant for the generate native code step. Building mathlib should only need to check the last step if that is even necessary.
If this is possible I'm going to try doing it.

[Mac]

Anders Christiansen Sørby said:

But this is also dependent on the actual lean binary command and the libraries it was using at the time. So the output should ideally also be hashed. For now lake is more like Cargo or pip which are very sensitive to what kind of input and config given to the tool. Also nix disallows internet access during build which ensures that it is always an input -> output build. Not that lake isn't a good tool. If possible I would want to ba able to generate drv files from something lake like and push that to the nix build daemon.

@Sebastian Ullrich has been working very hard on making Lean self-contained. Very soon the githash for Lean should be enough to uniquely determine the Lean binary and the libraries it was using at the time. Thus the whole chain of lean + .lean -> .olean / .c -> .o -> .a / .so / .exe should be content addressed and hash.

As to your second concern (internet access), I don't think a build system (especially one for Lean) should be concerned with malicious use (after all, building a Lean file already allows for arbitrary code execution which could potentially cheat even Nix by mucking with its store if it so desired). I think Lake trusting that the build steps work as advertised (i.e., the traces produced do uniquely determine the input -> output) is fine. In fact, a good bit of discussion here is about the problems with not being able to do this with Nix. If you want to prove that such an invariant is truly maintained, well, you can use Lean to do so! :big_smile:

[Mac]

Hmm, that makes me wonder if Lake could eventually have 0 trust mode that requires proof of input -> output content hash correspondence.

[Mario Carneiro]

a formal statement of that claim is almost certainly false because of hash collision

[Anders Christiansen Sørby]

Proofs need to know the internal structure of functions and types to work so that will definitely fail with external programs like cc, but in theory if everything is written in lean you could design a proof that ensures that a given input will produce output land inside the hash collision equivalence class or something like that.

[Anders Christiansen Sørby]

No internet access is really nice to avoid abusive use like embedded crypto miners and so on which is increasingly becoming a problem. Nix builds are sandboxed which means they have no way of interacting with the outside world except what they have been given as input.
If git hashes was enough then every git project ever could be called content addressed.
The point is that having a truly plug and play dev environment is what nix tries to and mostly succeed to achieve.
The compiler and all dependencies that were used to build a particular lean binary is not given by a git hash. This is something nix can ensure since all input is hashed.
Now nix has its problems no doubt, but in the end I think this is how all software should be built. :smile:

[Mac]

Anders Christiansen Sørby said:

If git hashes was enough then every git project ever could be called content addressed.

Every Git project is content addressed (at least source wise). That is what Git is, a content addressed VCS. The problem that things like Nix try to resolve, though, is that most project builds are not content addressed for two reasons: 1) they use inputs outside the project itself (like system compilers) which are not content addressed 2) many build systems do not produce content addresses of their outputs.

For Lean projects, the Git hash of Lean uniquely determines the Lean toolchain being used (which now includes the C compiler to build Lean outputs), thus the Git hash works as a content address for the Lean input to Lean project build. That is, Lean Git Hash + Hash of Lean source file uniquely determines (is a content address for) the olean output of the source.

[Mac]

Anders Christiansen Sørby said:

The compiler and all dependencies that were used to build a particular lean binary is not given by a git hash. This is something nix can ensure since all input is hashed.

I am a bit confused by this statement. Hashes are not reversible, so it is not possible to derive the compiler and all dependencies from any hash. The point of a content addressed hash is simply to uniquely determine the content of said object, which the Git hash is sufficient for the Lean toolchain obtained from elan. When building from source, though, you are right, you need something more.

[Anders Christiansen Sørby]

Yes, git is content addressed, and I weren't saying otherwise. But content addressing is more than uniquely determining something although that can be seen as sufficient in some cases.
The thing is, as I have tried, when downloading and trying to build a project with lake a lot of things can go wrong. Especially if you are using something not standard like NixOS. I it good to hear that lean is now bundled with all dependencies, but the git hash still does not tell you anything about which configuration flags were used or if it was liked against some library or a fork of something else. In the trivial case it is fine, but as soon as things get more complicated and customized it is not. I have struggled so many times with build issues relating to some undocumented env parameter or system setup needing to be present. What nix does is demanding that _all_ input is accounted for and that the actual build process can not be affected by changing returns from a web service or similar. This is a restriction that conflicts with the design of most builders, but ensures that the build is always deterministic.

The thing about content addresses outside of hashing is that you can actually look it up as an address. That is why an actual content address of the lean binary is a hash of the actual binary not the git hash that produced it. There are always some details that are not accounted for when you don't .

A build is a function and that can be content addressed as an AST of whatever build expression is used + a Merkle tree. It only makes sense to call a particular build content addressed when it is fully deterministic. In lake you can do arbitrary IO which essentially means there is no guarantees. Also system architecture has a lot to say. The same git hash does not produce the same output on different architectures.

My dream scenario would be to have something like lean as a frontend for nix providing end-to-end type checking where possible.

[Mac]

Anders Christiansen Sørby said:

A build is a function and that can be content addressed as an AST of whatever build expression is used + a Merkle tree. It only makes sense to call a particular build content addressed when it is fully deterministic.

I understand that you like Nix's approach. My point is that what you described here is merely one form of content addressed builds -- in particular, Nix's approach -- however a build system does not need to do exactly this to be considered content addressed.

All content addressed storage requires is that content can be fetched by its content address and that addresses are equal if and only if their content is equal (for the content relevant to the store). I can use the Git hash of Lean to uniquely to fetch a particular Lean toolchain (which is more than the shingle binary, by the way) and the same hash will map to the same toolchain if and only if they match. Therefore, it is a valid content address of the toolchain.

You are right that this does not account for the platform in question. However, Lean oleans are platform agnostic, so the platform should not be considered an input to them (even if it is an input to the compiler that built Lean). This is one problem Nix has (as far as I understand), which is that traces are a Merkel tree of all transitive inputs, even when the direct hash of an intermediate output may be sufficient. Hence why Nix building mathlib is a problem.

[Mac]

(If one did want to take the platform into account, mixing Lean's Git hash with the platform descriptor would give a cross-platform trace.)

[Anders Christiansen Sørby]

I'm clearly biased as a nix fan, but that is not without a reason. Plug and play dev setups and no config builds are super nice.
But what you are describing of mixing more and more hashes of relevant input to correctly input address a lean lake build is just doing what nix already is doing.
I'm not so sure nix would have a problem caching mathlib correctly. I might set it up to see what happens.

[Mac]

Anders Christiansen Sørby said:

I'm clearly biased as a nix fan, but that is not without a reason. Plug and play dev setups and no config builds are super nice.

If all you want is a plug and play dev setup VSCode + elan + lake already provide that. I feel like you clearly want something more than just plug and play.

Anders Christiansen Sørby said:

But what you are describing of mixing more and more hashes of relevant input to correctly input address a lean lake build is just doing what nix already is doing.

Yes, but my point was that which hashes you choose to mix is important. Many times you don't want to mix all the hashes of all possible inputs (which, as I understand it, is what Nix does) because the output is more generic than its inputs. Lean is a good example of this, as the oleans it produces are more generic than the compiler which produces them (i.e., they are cross-platform while the Lean binary is not).

[Sebastian Ullrich]

So this should obviously be replaced with a little program that uses the Nix API directly in any serious solution, but it is possible to use the content-addressed store to "build" .oleans for foreign platforms

# build on Linux, note derivation hash
$ nix --store $PWD/store-linux --extra-experimental-features 'ca-derivations' build .#Init.Prelude.out -vvvv 2> >(grep -E '^(error:|drv output)') --json
drv output 'sha256:5510cbd31d1e34ce34cfa48dbb2aa9ab4bff7034155f25a072f658ba94611294!out' is required, but there is no substituter that can provide it
drv output 'sha256:41a2bddf2e70c43558ed8e8c559cb116b67861a9183c8b2976febe663e671ae6!out' is required, but there is no substituter that can provide it
drv output 'sha256:41a2bddf2e70c43558ed8e8c559cb116b67861a9183c8b2976febe663e671ae6!c' is required, but there is no substituter that can provide it
[{"drvPath":"/nix/store/dj4ngv0s1k544qwxmdzjg7shwcq5qfjm-Init.Prelude.drv","outputs":{"out":"/nix/store/x8s1mk4yfixj3zmj5glnazxalpjzw7gn-Init.Prelude"}}]

# try to build for macOS, note derivation hash
$ nix --store $PWD/store-linux --extra-experimental-features 'ca-derivations' build .#packages.x86_64-darwin.Init.Prelude.out -vvvv 2> >(grep -E '^(error:|drv output)') --json
drv output 'sha256:e1b18fc3fb3c4327a0dd8ed462056fd49172bd8b403b37032bb66d4d1a71a260!out' is required, but there is no substituter that can provide it
error: a 'x86_64-darwin' with features {} is required to build '/nix/store/rc7737ppa23biwj7hjazn5a2z4rs5wsk-ccache-links.drv', but I am a 'x86_64-linux' with features {benchmark, big-parallel, ca-derivations, kvm, nixos-test}

# map macOS hash to build result of Linux hash
$ nix shell nixpkgs#sqlite -c sqlite3 store-linux/nix/var/nix/db/db.sqlite 'insert into Realisations (drvPath, outputName, outputPath, signatures) select "sha256:e1b18fc3fb3c4327a0dd8ed462056fd49172bd8b403b37032bb66d4d1a71a260" as drvPath, outputName, outputPath, signatures from Realisations as r where r.drvPath = "sha256:41a2bddf2e70c43558ed8e8c559cb116b67861a9183c8b2976febe663e671ae6";'

# macOS now builds successfully!
$ nix --store $PWD/store-linux --extra-experimental-features 'ca-derivations' build .#packages.x86_64-darwin.Init.Prelude.out -vvvv 2> >(grep -E '^(error:|drv output)') --json
[{"drvPath":"/nix/store/dsxn7yibv6mqws8annkprln97f2ydbva-Init.Prelude.drv","outputs":{"out":"/nix/store/x8s1mk4yfixj3zmj5glnazxalpjzw7gn-Init.Prelude"}}]

# while we're at it, demonstrate that content addressing indeed works
$ echo "-- $(date)" >> src/Init/Prelude.lean
$ nix --store $PWD/store-linux --extra-experimental-features 'ca-derivations' build .#Init.Prelude.out -vvvv 2> >(grep -E '^(error:|drv output)') --json
drv output 'sha256:bc7911ecd77d575bf6a42d4640f077fd799bdc166942f3246425f135cb8eb00f!out' is required, but there is no substituter that can provide it
drv output 'sha256:ec7bbeea22c8a967cc097eb9ca48b36d7be1ca87a40e02ddd694712732b945c4!out' is required, but there is no substituter that can provide it
drv output 'sha256:ec7bbeea22c8a967cc097eb9ca48b36d7be1ca87a40e02ddd694712732b945c4!c' is required, but there is no substituter that can provide it
[{"drvPath":"/nix/store/3pnpr0gjyby1mgwpzi9llhfifzvsa7ph-Init.Prelude.drv","outputs":{"out":"/nix/store/x8s1mk4yfixj3zmj5glnazxalpjzw7gn-Init.Prelude"}}]

[Sebastian Ullrich]

Is it hacky? Absolutely. But otherwise this is no different from implicitly assuming that Lean generates identical oleans for different platforms (which we know is not true in the presence of arbitrary metaprograms anyway).

[Anders Christiansen Sørby]

I have some questions about the LSP implementation when using nix. What I have been doing so far is just to hook up the correct lean to PATH with nix develop and run lean --server however I also want to put my lean files in a src or testdirectory. Is there some config / flag to fix this?
Also I get this error that I should open the directory as a workspace (in neovim with coc.nvim and in VSCode).
What could this mean?

[cognivore]

:eyes:

[cognivore]

I'm trying to run a workflow verbatim (as suggested in #lean4 > ✔ Easily test lean4 patch), but it fails with nix stack overflow: https://github.com/cognivore/lean4/actions/runs/3753931115/jobs/6377674941

[cognivore]

Currently, I'm trying to reproduce the commands locally by entering nix shell and will tinker to understand what's going on. In the meantime, I'll have Github build the exact copy of lean4's main branch under my user.

If someone understands what's going on or have seen an error like this before, however, please do share your knowledge! It will be highly appreciated :bow:

[cognivore]

(Reproduced at home with my branch)

Thu Dec 22 00:46:34:143384200 cognivore@conflagrate ~/github/lean4-float-fork (cognivore/deopaque-ofscientific)
λ nix shell
error: builder for '/nix/store/x05m7zq51f7bfzajl464lsxj2y35b5sr-Lean.Data.FuzzyMatching.drv' failed with exit code 1;
       last 1 log lines:
       > deep recursion was detected at 'whnf' (potential solution: increase stack space in your system)
       For full logs, run 'nix log /nix/store/x05m7zq51f7bfzajl464lsxj2y35b5sr-Lean.Data.FuzzyMatching.drv'.
error: 1 dependencies of derivation '/nix/store/qy9pr2jfb3lgflicyv72vf4k3gf6yigp-Lean-depRoot.drv' failed to build
error: 1 dependencies of derivation '/nix/store/7kqdnr2fvkvxx63r2vw8jngzkx60sxd0-Lean.Data.FuzzyMatching-cc.drv' failed to build
error: 1 dependencies of derivation '/nix/store/9yj80f2jrccxwbxbwgwn9n3r4yffyvv1-Lean.Server.Completion-depRoot.drv' failed to build
error: 1 dependencies of derivation '/nix/store/5na9mfb04v33fvf783ks5haa14kmmm3v-Lean.Server.Watchdog-depRoot.drv' failed to build
error: 1 dependencies of derivation '/nix/store/lf07py4slm4371x8pks996kvvc5i3y65-lean-stage1.drv' failed to build

[cognivore]

Carbon copy works!, so I wrote a bug in the patch.

Now the question is how to learn why is it a bug! When you get a log like this, how do you learn how exactly does the build fail?

[cognivore]

I would like to have a dev shell without building lean and then manually reproduce the build steps from lean-all.

[Mauricio Collares]

Try running nix develop instead of nix shell. Running the build steps manually can typically be done by running genericBuild inside the resulting shell, and that can typically be broken into phases depending on the concrete use case.

[cognivore]

Ok, thank you!

[Sebastian Ullrich]

So just to make clear, you do not have to use Nix if you don't want to! Your first link doesn't work for me, so I'm missing a bit of context (edit: found it).