cmake woes in source build

Stream: general

[Miguel Raz Guzmán Macedo]

Hello!
I am trying to build a binary distribution of lean from source so that I can call Lean from the Julia programming language.
I am just trying to set this up inside a sandbox linux environment which has GMP 5 and GCC 5, but I keep getting this error:

[ 98%] Linking C executable c_name_test
cd /workspace/srcdir/lean/build/release/tests/shared && /usr/bin/cmake -E cmake_link_script CMakeFiles/c_name_test.dir/link.txt --verbose=false
/opt/x86_64-linux-gnu/bin/../lib/gcc/x86_64-linux-gnu/5.2.0/../../../../x86_64-linux-gnu/bin/ld: warning: libstdc++.so.6, needed by ../../libleanshared.so, not found (try using -rpath or -rpath-link)
../../libleanshared.so: undefined reference to `typeinfo for std::invalid_argument@GLIBCXX_3.4'
../../libleanshared.so: undefined reference to `VTT for std::__cxx11::basic_stringstream<char, std::char_traits<char>, std::allocator<char> >@GLIBCXX_3.4.21'

Any ideas how I can solve this?

[Miguel Raz Guzmán Macedo]

TLDR: libstdc++.so.6 not found, at 98% of the compilation :(((

[Alex J. Best]

Which version of lean are you trying to make?

[Miguel Raz Guzmán Macedo]

version 3.15.0 of the leanprover-community

[Reid Barton]

From the pathnames it looks like you have some kind of custom setup that we won't guess.

[Reid Barton]

I mean most Linux users probably have g++ installed at /usr/bin/g++ and not under /opt.

[Reid Barton]

I guess maybe that's what "sandbox" means.

[Reid Barton]

Anyways, I think your g++ installation is just broken.

[Miguel Raz Guzmán Macedo]

Don't know what you mean by broken, but myself and others have used this succesfully to build many projects.

[Miguel Raz Guzmán Macedo]

Could be it's not linked to properly, sure.

[Reid Barton]

In any case, it doesn't look like a Lean-related error

[Ryan Lahfa]

@Miguel Raz Guzmán Macedo can you try ldd ../../libleanshared.so ?

[Ryan Lahfa]

or wherever is the libleanshared

[Ryan Lahfa]

and post the output

[Ryan Lahfa]

ah, at linktime, I guess it's not working

[Ryan Lahfa]

are you even sure you have libstdc++6 ?

[Miguel Raz Guzmán Macedo]

yup, lemme try. the libleanshared.so is produces after a make, and even a make bin_lean, but lemme see.

[Ryan Lahfa]

like if you do ldd on some C++-linked executable, can you see it being linked to libstdc++ ?

[Ryan Lahfa]

honestly, though, if I were you and wanted to build a very specific version of Lean in a sandbox

[Ryan Lahfa]

I'd just use Nix or Guile for this usecase

[Ryan Lahfa]

and reuse Nix's derivations for example

[Ryan Lahfa]

https://github.com/NixOS/nixpkgs/blob/master/pkgs/applications/science/logic/lean/default.nix

[Miguel Raz Guzmán Macedo]

It's a specific sandbox that users can then build on Windows/Mac/Linux within Julia.

[Ryan Lahfa]

I don't understand, do you do cross compilation to arbitrary arch/ABI targets?

[Ryan Lahfa]

I guess what you're doing is creating a xxx.jl to wrap Lean's shared lib in Julia, right?

[Ryan Lahfa]

So you just want some derivation which spits jl + so, Nix/Guile seems to be perfect for this use-case

[Ryan Lahfa]

It's also a build sandbox, using cgroups & stuff

[Ryan Lahfa]

Anyway, we can try to debug your issue, but in the end, like @Reid Barton want to say more or less, it's infinitely easier to reuse "known working environments"

[Miguel Raz Guzmán Macedo]

Yes, the idea is to do cross compilation to arbitrary targets.
Yes, I want to later build a Lean.jl to wrap Leans shared lib in Julia.
I want to use this particular workflow (BinaryBuilder.jl) because if users do using Lean within a Julia script it auto downloads and build Lean and puts everyting into the appropriate place.
And this only needs to be done once for the entire Julia ecosystem.

[Ryan Lahfa]

it needs to be done each time you want to change the Lean version AFAIK

[Miguel Raz Guzmán Macedo]

That's fine - other tarballs can be fixed up for subsequent versions.

[Ryan Lahfa]

except if you automated some script, then makes sense

[Miguel Raz Guzmán Macedo]

Yes, an automated script gets produced from this too which can later get tweaked.

[Miguel Raz Guzmán Macedo]

I will try to just build the bin_lean and see what goes from there.

[Ryan Lahfa]

Anyway, we need information on the set of libstdc++ libs you have currently, their path and more logs

[Ryan Lahfa]

ldd can give you most of this stuff, then we can try to see why CMake/GCC don't find what you want

[Ryan Lahfa]

The culprit might be also that you don't have this lib at all

[Ryan Lahfa]

So you need to look for it

[Miguel Raz Guzmán Macedo]

@Ryan Lahfa managed a workaround - you can enjoy it being built for like 12 archs here https://dev.azure.com/JuliaPackaging/Yggdrasil/_build/results?buildId=3914&view=results

[Reid Barton]

What was the workaround?

[Miguel Raz Guzmán Macedo]

copying the make bin_lean executable into a proper directory.

[Miguel Raz Guzmán Macedo]

and then it worked. :shrug:

[Miguel Raz Guzmán Macedo]

OK, I have my executable made.
If I have a file that has a simple Lean example, how can I run that from the comandline?
ie, I have

example (m n : ℕ) : m + n = n + m :=
by simp

In a hello_world.txt
And I want to run
lean hello_world.txt but it currently says

/home/mrg/lean.txt:2:3: error: simplify tactic failed to simplify
(I ripped the example of the web live demo, so I might be missing some imports)

[Miguel Raz Guzmán Macedo]

@Ryan Lahfa we are this so close to having Julia -> Lean interop

[Bryan Gin-ge Chen]

The old web demo uses an older version of Lean where nat.add_comm is a simp-lemma.

So simply change by simp to by simp [nat.add_comm].

[Bryan Gin-ge Chen]

See #webeditor for the more up-to-date community web editor.

[Bryan Gin-ge Chen]

Note that if lean hello_world.txt succeeds, Lean won't return any output.

[Miguel Raz Guzmán Macedo]

Thanks @Bryan Gin-ge Chen ! It works! Muahahaha!

[Miguel Raz Guzmán Macedo]

Ok wait - is there way to not feed a file to lean foo.txt, but rather a string ?

[Bryan Gin-ge Chen]

There's the server mode, which @Jason Rute explained here.

[Miguel Raz Guzmán Macedo]

Awesome!
And what is leanchecker for?

[Mario Carneiro]

I think it is an "external" typechecker that reuses the lean kernel

[Bryan Gin-ge Chen]

See https://github.com/leanprover-community/lean/blob/master/doc/export_format.md

[Miguel Raz Guzmán Macedo]

Oh, wow, I missed that because I don't know how to Zulip. Thanks a lot @Brian Jiang !