Zulip Chat Archive

Stream: new members

Topic: SIGABRT while building Lean


view this post on Zulip Jean Lo (Jun 23 2019 at 13:18):

Attempting and failing to build lean from source on a new system. The last few lines from the make output were

[68%] built target lean
[68%] built target bin_lean

Before the process stops with a Signal 6 / Error code 1. Not sure what's happening, nor where to begin trying to find out.

The process also issued a lot of warnings complaining about 'operator delete' has a non-throwing exception specification but can still throw, and though I thiiink it isn't something that I should be worried about, I don't remember this happening on previous builds.

view this post on Zulip Kenny Lau (Jun 23 2019 at 13:22):

OS?

view this post on Zulip Jean Lo (Jun 23 2019 at 13:36):

FreeBSD 12.0-RELEASE

view this post on Zulip Jean Lo (Jun 23 2019 at 13:40):

At this point lean and leanpkg already exist in bin, but trying to run either of those just gets me a Abort trap (core dumped).

view this post on Zulip Kenny Lau (Jun 23 2019 at 13:42):

download a windows emulator and then use vscode and elan

view this post on Zulip Jean Lo (Jun 23 2019 at 13:43):

How about I go onto my windows computer then use vscode and elan

view this post on Zulip Kenny Lau (Jun 23 2019 at 13:43):

that would be better

view this post on Zulip Jean Lo (Jun 23 2019 at 13:45):

but yeah i realise i was probably being a stupid by assuming everything would just work the same as when it was on linux D:

view this post on Zulip Mario Carneiro (Jun 23 2019 at 13:45):

For the most part lean works better on linux

view this post on Zulip Mario Carneiro (Jun 23 2019 at 13:45):

not sure if FreeBSD has an issue

view this post on Zulip Kenny Lau (Jun 23 2019 at 13:46):

so you can download a linux emulator in the windows emulator and build lean in the linux inside windows inside FreeBSD, but use VSCode in the windows inside FreeBSD

view this post on Zulip Jean Lo (Jun 23 2019 at 13:46):

I was hoping it'd happen to all just work out if i compiled the source within FreeBSD

view this post on Zulip Jean Lo (Jun 23 2019 at 13:46):

@Kenny Lau : no.

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 14:14):

If bin_lean has been built, then usually the next thing cmake tries to do is to build the standard library (check the standard_lib target in src/CMakeLists.txt), which involves running the lean executable (you should be able to find it in your_build_directory/shell/lean and bin/lean). I suspect that that is what is crashing, so if you want to dig into this, you can try running lean --make (inside the library directory) from gdb or some other debugger and then looking at the stack trace when it crashes.

I'm a little surprised that lean and bin_lean are being built at 68% though, usually they're among the last things being built. Out of curiosity, could you share a link to your full build log?

view this post on Zulip Mario Carneiro (Jun 23 2019 at 14:16):

I think if the test suite is getting built that would come after

view this post on Zulip Mario Carneiro (Jun 23 2019 at 14:16):

which is the default IIRC

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 14:17):

That makes sense. I'm more used to seeing logs that look like this though.

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 14:44):

Ah, the difference is probably whether you run make -j2 or just make.

view this post on Zulip Jean Lo (Jun 23 2019 at 14:53):

why would make -j2 help in this case?

also, sorry, was mucking around & didn't have the logs anymore. Here's they are : https://pastebin.com/raw/DJLHdXCN https://pastebin.com/raw/Nzts85BG . The stderr is stupid huge but appears to just be warnings about the same thing every time it crops up?

view this post on Zulip Jean Lo (Jun 23 2019 at 15:02):

tried make -j2, it moved the errors down some. Now it's the linker that's dying instead: https://pastebin.com/raw/dawrJe76

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 15:30):

Sorry, I didn't mean that make -j2 would help with your problem. It would just explain the difference in build order.

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 15:35):

Hmm, the final error log suggests that -fPIC is missing from the build flags. The culprit might be this overly-specific test. You might want to go through that file and change some of the Linux conditionals to allow for FreeBSD and see if that helps.

view this post on Zulip Jean Lo (Jun 23 2019 at 15:42):

ah, okay.

I just naively tried getting cmake to -fPIC everything by adding a line in the CMakeLists.txt because I didn't see your message yet & didn't know about the test. The build process on that try has just concluded - it died at the very end with Abort trap (core dumped) after building lean and bin_lean.

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 15:50):

Yeah, as above, that looks like lean is crashing when trying to build the standard library.

view this post on Zulip Jean Lo (Jun 23 2019 at 16:34):

right.

I didn't have gdb on this system when I set it up, so that took a while. And in honesty this is more digging than I'm really used to doing, especially that I don't really know how Lean works, so sorry for this being me getting confused and asking many silly questions.

Anyways - here's the bt from the crash. (Would rebuilding with the CMAKE_BUILD_TYPE flag set to debug make this more informative?)

#0  0x0000000800f1d45a in thr_kill () from /lib/libc.so.7
#1  0x0000000800f1b844 in raise () from /lib/libc.so.7
#2  0x0000000800e8e079 in abort () from /lib/libc.so.7
#3  0x0000000800cea8ba in ?? () from /lib/libcxxrt.so.1
#4  0x00000000004c876e in lean::get_exe_location() ()
#5  0x00000000004cba6d in lean::get_builtin_search_path() ()
#6  0x00000000004cc5a2 in lean::standard_search_path::standard_search_path() ()
#7  0x000000000049807d in main ()

view this post on Zulip Reid Barton (Jun 23 2019 at 16:37):

It's trying to use snprintf(path, PATH_MAX, "/proc/%d/exe", pid);--I assume BSD doesn't have /proc

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 16:41):

Wow, nice catch! That line is in src/util/path.cpp. So it looks like you'll need to write an #elif there with an appropriate path for FreeBSD.

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 16:42):

Maybe something using linprocfs? (This is just random googling on my part.)

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 16:44):

(deleted)

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 16:57):

There are two suggestions for getting the current executable path in FreeBSD in this SO answer: the first one links to a question with some C code that might work, the second one suggests that you might be able to just mount procfs to /proc before running lean (maybe this works?)

view this post on Zulip Jean Lo (Jun 23 2019 at 16:58):

eh, I'm very very new to BSD as well. but did some random googling. Yeah, I suspect reading /proc/curproc/filewould work if I have procfs mounted.

view this post on Zulip Jean Lo (Jun 23 2019 at 17:00):

I'll go and put in the #elifs, recompile, see what happens maybe?

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 17:02):

You might not even have to put in the #elif if you mount procfs to /proc. nevermind, I missed you need /file and not /exe at the end.

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2019 at 17:04):

There's also another reference to /proc in src/util/memory.cpp.

view this post on Zulip Jean Lo (Jun 23 2019 at 17:06):

oh, thanks for the catch. would've hated to be hit by that after waiting for it to compile another time

view this post on Zulip Jean Lo (Jun 23 2019 at 18:43):

aaand it worked. sort of.

I edited in the /proc/execthing, but wasn't sure what the proper way was to do what statm does on Linux, but since the process just defaults to returning 0 if it can't read the file, I thought it'd be worth trying just compiling the thing anyway while I figure that out. And the make install terminated without incident!

So I now have a functional installation of Lean that doesn't know how much memory it's using, at least not for now. Not sure what sort of other consequences that'd have, or if there's anything else that's going to break but hasn't yet. I'm still unsure about the statm thing; but random googling suggests there's a way of doing both that and the pid/exe thing from earlier without asking the user to mount procfs, so I might spend some time later and properly put some code in for both of those.

view this post on Zulip Chris Hughes (Jun 23 2019 at 20:17):

You could always use elan.

view this post on Zulip Reid Barton (Jun 23 2019 at 22:16):

but does elan have BSD binaries?

view this post on Zulip Keeley Hoek (Jun 24 2019 at 11:23):

No

view this post on Zulip Wojciech Nawrocki (Jun 24 2019 at 12:08):

@Jean Lo If you do get Lean building & running on FreeBSD, you could submit a PR to leanprover-community/lean/ :)


Last updated: May 10 2021 at 18:22 UTC