libgmp dependency

Stream: general

[Scott Morrison]

I know on macOS you have to install libgmp before Lean will work. Does anyone know if there is a similar requirement on linux? (There doesn't appear to be on Windows.)

[Reid Barton]

The toolchains installed by elan contain static binaries, which I find a bit surprising, but should mean you don't need libgmp. However all the machines I have lean on also have libgmp installed anyways, so no definitive proof.

[Sebastian Ullrich]

Yes, on Linux it's definitely a static binary. I'm not even sure why it's not on macOS

[Scott Morrison]

@Sebastian Ullrich, is the libgmp dependency on OS X something that could be fixed? (In elan?) I don't really know about these static/dynamic library issues. Given a pointer to something to look I could try to sort it out.

[Scott Morrison]

Helping out students, I see how valuable it would be to get a "no command line necessary" install procedure, and I think libgmp is one of the last obstacles. (On OS X one currently needs brew install coreutils to get greadlink, but there are various ways to get around this: https://stackoverflow.com/questions/1055671/how-can-i-get-the-behavior-of-gnus-readlink-f-on-a-mac)

[Scott Morrison]

For reference, the error message my students have been getting (on OS X) is:

[Scott Morrison]

dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
  Referenced from: /Users/ZZZ/.elan/toolchains/nightly-2019-01-13/bin/lean
  Reason: image not found

[Scott Morrison]

(this is of course fixable with brew install gmp, but the point is to avoid this if possible)

[Keeley Hoek]

I have not taken the time to try to fully understand the build system, nor have I ever used CMake for anything, so I can't point exactly to where the distinction between the operating systems is made given default settings, but I did try a mac build (on your machine scott) forcing the static option on. However, I get a whole bunch of

ld: library not found for -lcrt0.o
clang: error: linker command failed with exit code 1

which looked like a solvable problem (the crt0 has to by lying around somewhere!, I thought). But alas, there is this:
https://stackoverflow.com/questions/3801011/ld-library-not-found-for-lcrt0-o-on-osx-10-6-with-gcc-clang-static-flag
Apparently, apple refuses to provide statically linked libSystem.dylib, so you'd have to build it yourself...

This is all to say that you can't just be lazy and pass -static and compile with gcc or clang to fix the problem.

[Keeley Hoek]

On the other hand, I manually patched out the references to the dynamic library libgmp.dylib in the generated CMakeFiles and compiled, and everything worked fine... Here's a link to the zip for macos that was built:

[Keeley Hoek]

https://github.com/khoek/klean/releases/download/macos-static/lean-3.4.2-darwin.zip

I'd be really good to know if it works (i.e. doesn't need libgmp.dylib)---I'm pretty sure it doesn't but I don't actually have a mac.
(If this works, it's obviously unsatisfactory, but it's proof the build system could probably be fixed/improved easily by someone who understood it.)

[Keeley Hoek]

On the other hand, I'm pretty sure the dynamic loader would look in the directory where the executable is for missing shared libraries, so if elan just popped a copy of libgmp.10.dylib in the bin directory of an extracted release I think we'd be okay too?

[Scott Morrison]

re: the last point, cp /usr/local/opt/gmp/lib/libgmp.10.dylib /Users/scott/.elan/bin/ doesn't help

[Scott Morrison]

and yes, your statically linked binary really works, (when normal lean doesn't, complaining

dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
  Referenced from: /Users/scott/.elan/toolchains/stable/bin/lean
  Reason: image not found
Abort trap: 6

[Keeley Hoek]

Your last snipped confused me, presumably you hid /usr/local/opt/gmp/lib/libgmp.10.dylib before test-invoking bin/lean?

[Schrodinger ZHU Yifan]

How does lean import gmp symbols? I don't see any dependency from binary distributions?

schrodinger@Yifans-MacBook-Air hasher % otool -L $(which lean)
/Users/schrodinger/.elan/bin/lean:
        /usr/lib/libcurl.4.dylib (compatibility version 7.0.0, current version 9.0.0)
        /usr/lib/libiconv.2.dylib (compatibility version 7.0.0, current version 7.0.0)
        /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)

[Sebastian Ullrich]

We are in the process of replacing GMP with a custom implementation lifted from Z3. If you're on Apple Silicon, that's already the case.

[Schrodinger ZHU Yifan]

Is it mpn? I wonder if we can have API to access the buffer of mpn and its length. (mpz has mpz_limbs_read and mpz_size)

[Ioannis Konstantoulas]

Sebastian Ullrich said:

We are in the process of replacing GMP with a custom implementation lifted from Z3. If you're on Apple Silicon, that's already the case.

What is the reason/reasons for this change?

[Schrodinger ZHU Yifan]

license？

[Ioannis Konstantoulas]

Schrodinger ZHU Yifan said:

license？

Oh, I see! If the license is a burden and there is no significant performance hit, why not.

[Alex J. Best]

Schrodinger ZHU Yifan said:

license？

Can someone confirm / say more about this and what sort of license is desired for Lean if that is the case?

[Ioannis Konstantoulas]

Alex J. Best said:

Schrodinger ZHU Yifan said:

license？

Can someone confirm / say more about this and what sort of license is desired for Lean if that is the case?

I guess Apache license; generally, corporate-sponsored open source projects prefer permissive licenses like Apache over copyleft like GPL.

[Ioannis Konstantoulas]

I generally use GPL 3.0 for my projects, but I will use Apache if/when I upload Lean code, to make things easier for the rest of the community.

[Alex J. Best]

Sure, I'm wondering if the devs considered switching to MPIR instead of gmp, it was forked from GMP for essentially this purpose, its not really maintained these days but it always maintained backwards compatibility so would be a drop in replacement.
If the performance hit is small of course not depending on an external library is better but its something to consider

[Ioannis Konstantoulas]

For further information, can someone link to the code of the new library (e.g. the one that works on Apple stuff)? Is it written in C? I'd like to poke around a bit.

[Mauricio Collares]

It's code extracted from Z3, as far as I understand it. I don't think it is packaged as a library.

[Mauricio Collares]

See, e.g., https://github.com/leanprover/lean4/blob/89b65c8f1d6fa7700d73f1bc12db0b140c728e32/src/runtime/mpz.cpp

[Scott Morrison]

@Ioannis Konstantoulas, I've been meaning to write some tests for these functions: if you're at all interesting in writing tests as part of poking around, that would be amazing. :-)

[Ioannis Konstantoulas]

Scott Morrison said:

Ioannis Konstantoulas, I've been meaning to write some tests for these functions: if you're at all interesting in writing tests as part of poking around, that would be amazing. :-)

Oh no no, I am an amateur and will create more trouble than help :laughing: . I am trying to learn Lean well enough to be able to help on simple matters, but I am still far from ready. I do not even understand how the github collaboration process works: what is CI, how to make correct PRs, etc.

[Ioannis Konstantoulas]

I also don't know any real C++; I am comfortable with some parts of C, but not any specialized work, especially as subtle as bignum.

[Schrodinger ZHU Yifan]

@Scott Morrison do you know how hashable interface is implemented for MPN/MPZ