SIGABRT while building Lean

Stream: new members

[Jean Lo]

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.

[Kenny Lau]

OS?

[Jean Lo]

FreeBSD 12.0-RELEASE

[Jean Lo]

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).

[Kenny Lau]

download a windows emulator and then use vscode and elan

[Jean Lo]

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

[Kenny Lau]

that would be better

[Jean Lo]

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:

[Mario Carneiro]

For the most part lean works better on linux

[Mario Carneiro]

not sure if FreeBSD has an issue

[Kenny Lau]

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

[Jean Lo]

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

[Jean Lo]

@Kenny Lau : no.

[Bryan Gin-ge Chen]

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?

[Mario Carneiro]

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

[Mario Carneiro]

which is the default IIRC

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Jean Lo]

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?

[Jean Lo]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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.

[Jean Lo]

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.

[Bryan Gin-ge Chen]

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

[Jean Lo]

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 ()

[Reid Barton]

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

[Bryan Gin-ge Chen]

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.

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

(deleted)

[Bryan Gin-ge Chen]

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?)

[Jean Lo]

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.

[Jean Lo]

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

[Bryan Gin-ge Chen]

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.

[Bryan Gin-ge Chen]

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

[Jean Lo]

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

[Jean Lo]

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.

[Chris Hughes]

You could always use elan.

[Reid Barton]

but does elan have BSD binaries?

[Keeley Hoek]

No

[Wojciech Nawrocki]

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