Lean 4 on OpenBSD

Stream: lean4

[Thanos Tsouanas]

Has anyone here managed to build Lean 4 on OpenBSD? I'm trying to build 4.0.0.
First bump was the non-existent sys/random.h. For the time being I have just commented-out the corresponding #include line in runtime/io.cpp. This allowed gmake to move past this bump for the time being, but it hit a second one:

[ 63%] Built target compiler
[ 63%] Built target leancpp
[ 63%] Built target make_stdlib
[ 63%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/stack_overflow.cpp.o
/cave/thanos/devel/lean4/lean4-4.0.0/stage0/src/runtime/stack_overflow.cpp:63:5: error: use of undeclared identifier 'pthread_getattr_np'; did you mean 'pthread_attr'?
    pthread_getattr_np(pthread_self(), &attr);
    ^
/usr/include/pthread.h:96:8: note: 'pthread_attr' declared here
struct pthread_attr;
       ^
1 error generated.
gmake[5]: *** [runtime/CMakeFiles/leanrt_initial-exec.dir/build.make:342: runtime/CMakeFiles/leanrt_initial-exec.dir/stack_overflow.cpp.o] Error 1
gmake[4]: *** [CMakeFiles/Makefile2:1129: runtime/CMakeFiles/leanrt_initial-exec.dir/all] Error 2
gmake[3]: *** [Makefile:146: all] Error 2
gmake[2]: *** [CMakeFiles/stage0.dir/build.make:86: stage0-prefix/src/stage0-stamp/stage0-build] Error 2
gmake[1]: *** [CMakeFiles/Makefile2:90: CMakeFiles/stage0.dir/all] Error 2
gmake: *** [Makefile:136: all] Error 2

I tried messing with src/runtime/stack_overflow.cpp. The following snippet starts on line 56:

bool is_within_stack_guard(void * addr) {
    char * stackaddr;
#ifdef __APPLE__
    stackaddr = static_cast<char *>(pthread_get_stackaddr_np(pthread_self())) - pthread_get_stacksize_np(pthread_self());
#else
    pthread_attr_t attr;
    if (pthread_attr_init(&attr) != 0) return false;
    pthread_getattr_np(pthread_self(), &attr);
    size_t stacksize;
    pthread_attr_getstack(&attr, reinterpret_cast<void **>(&stackaddr), &stacksize);
    pthread_attr_destroy(&attr);
#endif
    // close enough; the actual guard might be bigger, but it's unlikely a Lean function will have stack frames that big
    size_t guardsize = static_cast<size_t>(sysconf(_SC_PAGESIZE));
    // the stack guard is *below* the stack
    return stackaddr - guardsize <= addr && addr < stackaddr;
}

Usually, in cases like these, going the APPLE/MACOSX route has more chances to work for OpenBSD (programs tend to assume that the #else clause corresponds to some GNU/Linux for Linuxism's sake). But for this error neither the #ifdef __APPLE__ route nor the #else route worked. I managed to get past this temporarily by commenting out this whole #ifdef…#endif, although I get a fair warning:

[ 63%] Building CXX object runtime/CMakeFiles/leanrt_initial-exec.dir/stack_overflow.cpp.o
/cave/thanos/devel/lean4/lean4-4.0.0/stage0/src/runtime/stack_overflow.cpp:71:12: warning: variable 'stackaddr' is uninitialized when used here [-Wuninitialized]
    return stackaddr - guardsize <= addr && addr < stackaddr;
           ^~~~~~~~~
/cave/thanos/devel/lean4/lean4-4.0.0/stage0/src/runtime/stack_overflow.cpp:57:21: note: initialize the variable 'stackaddr' to silen
ce this warning
    char * stackaddr;
                    ^
                     = nullptr
1 warning generated.

And now it bumps while trying to build libleanshared.so, with ld errors suggesting to «recompile with -fPIC»:

[    ] Building /cave/thanos/devel/lean4/lean4-4.0.0/build/release/stage0/lib/lean/libleanshared.so
ld: error: relocation R_X86_64_PC32 cannot be used against symbol l_Classical_tacticBy__cases___x3a__; recompile with -fPIC
>>> defined in /cave/thanos/devel/lean4/lean4-4.0.0/build/release/stage0/lib/lean/libInit.a(Classical.o)
>>> referenced by Classical.c
>>>               Classical.o:(initialize_Init_Classical) in archive /cave/thanos/devel/lean4/lean4-4.0.0/build/release/stage0/lib/l
ean/libInit.a

ld: error: relocation R_X86_64_PC32 cannot be used against symbol l_instCoeTC___rarg; recompile with -fPIC
>>> defined in /cave/thanos/devel/lean4/lean4-4.0.0/build/release/stage0/lib/lean/libInit.a(Coe.o)
>>> referenced by Coe.c
>>>               Coe.o:(l_instCoeTC) in archive /cave/thanos/devel/lean4/lean4-4.0.0/build/release/stage0/lib/lean/libInit.a

…and many similar errors, until it dies with exit code 2:

ld: error: relocation R_X86_64_PC32 cannot be used against symbol l_decPropToBool___rarg___boxed; recompile with -fPIC
>>> defined in /cave/thanos/devel/lean4/lean4-4.0.0/build/release/stage0/lib/lean/libInit.a(Coe.o)
>>> referenced by Coe.c
>>>               Coe.o:(l_decPropToBool) in archive /cave/thanos/devel/lean4/lean4-4.0.0/build/release/stage0/lib/lean/libInit.a

ld: error: too many errors emitted, stopping now (use -error-limit=0 to see all errors)
cc: error: linker command failed with exit code 1 (use -v to see invocation)
gmake[6]: *** [/cave/thanos/devel/lean4/lean4-4.0.0/build/release/stage0/stdlib.make:47: /cave/thanos/devel/lean4/lean4-4.0.0/build/release/stage0/lib/lean/libleanshared.so] Error 1
gmake[5]: *** [CMakeFiles/leanshared.dir/build.make:71: CMakeFiles/leanshared] Error 2
gmake[4]: *** [CMakeFiles/Makefile2:1051: CMakeFiles/leanshared.dir/all] Error 2
gmake[3]: *** [Makefile:146: all] Error 2
gmake[2]: *** [CMakeFiles/stage0.dir/build.make:86: stage0-prefix/src/stage0-stamp/stage0-build] Error 2
gmake[1]: *** [CMakeFiles/Makefile2:90: CMakeFiles/stage0.dir/all] Error 2
gmake: *** [Makefile:136: all] Error 2

Any ideas?

[Aisha Tammy]

You need to add another ifdef specifically for openbsd where the function to be used is
pthread_attr_getstackaddr - from pthreads.3 - https://man.openbsd.org/pthreads.3#pthread_attr_getstackaddr
pthreads is a pita as there's over 9000 non-portable (pthread_*_np) functions everywhere.

[Thanos Tsouanas]

Thanks @Aisha Tammy ! I believe this is indeed the proper way to solve the second "bump" I mentioned above.
But looking at the original stack_overflow.cpp code and pthreads(3) man page I am not sure how I should proceed with translating this part.
Do you have any idea about the ld error? (the one suggesting to «recompile with -fPIC»).

[Aisha Tammy]

PIC is for position independent code which is needed when you want to relocate symbols, which typically is needed when creating a shared library as that is going to be loaded by the runtime linker and potentially placed in different locations (aslr/etc.)
The fix here would be to find out what is generating the shared/static libraries and add -fPIC to both CFLAGS and LDFLAGS.
From a quick look it seems like the libInit.a is being built using the leanc.sh, which is where you would need to add -fPIC to the CFLAGS/LDFLAGS, but it is some kind of wrapper around CC and that file itself is autogenerated using CMakelists.txt at here - https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt#L567
Now if we look above that here - https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt#L355 - we see that CMakelists.txt has capability to add fpic but its only doing it for Linux, so the solution is to also add *BSD to that check (or what ever other workaround lean developers would be happy to accept as a patch).
I'm not a lean user or developer nor have I ever seen the lean codebase before this, so I hope you can try to do the next steps yourself :)
best of luck

[Thanos Tsouanas]

Thanks again, @Aisha Tammy! The -fPIC problem was solved thanks to your tip, although I couldn't spot how the stage0's CMakeLists.txt is generated. (So I had to edit both CMakeList.txt files manually.) I still didn't manage to finish the build; I'll keep trying and report back.

[Mario Carneiro]

nothing in stage0 is autogenerated (except by the previous stage, no longer in the source tree)

[Thanos Tsouanas]

Aaah, I just noticed that lean4-4.0.0.tar.gz already has src/CMakeList.txt and stage0/CMakeList.txt. Sorry, I thought stage0's was somehow generated from somewhere. So it makes sense that I had to alter both files in the (so far unsuccessful) attempt to build on OpenBSD.

[Mario Carneiro]

it's unusual (but not unprecedented) to need to modify stage0/, although this is generally on the assumption that there is already an existing build that works and you are just making a modification to it. If this is the first time building on a new platform I can imagine needing to make modifications to both

[Mario Carneiro]

it is interesting that we are shipping lean4 with both stage0 and stage1. @Sebastian Ullrich is it possible to remove stage0 from releases? Seems like that just needlessly increases the distribution size

[Aisha Tammy]

This line here - https://github.com/leanprover/lean4/blob/master/CMakeLists.txt#L6
It says you can pass variables to stage0 with some prefix, if that helps.
@Mario Carneiro OpenBSD is a new platform, with its own everything, so I do imagine a stage0 is needed. I am unfamiliar with how Lean4 builds, presumably at some point the build will be able to have a bootstrap blob and just use that going forward. Would be good if someone makes an official port/package and that way would be easier to keep track of patches/ problems.
@Thanos Tsouanas if you want to create an official OpenBSD package that would be a nice way of moving forward.

[Mario Carneiro]

the "bootstrap blob" is stage0/

[Mario Carneiro]

it's not a blob, although it consists largely of generated C source files so it may as well be to some extent

[Aisha Tammy]

is it possible to build stage0 without the top level cmake being run? The "external project" structure with cmake calling cmake was quite interesting to look at, haven't seen that one before XD

[Mario Carneiro]

the whole build structure is dark magic and voodoo as far as I can understand. I've been considering writing a bootstrap chain for lean4 but disentangling those cmake files is a nightmare

[Aisha Tammy]

Haha, agreed, cmake is not the most fun tool but oh well.

[Thanos Tsouanas]

Aisha Tammy said:

This line here [...] says you can pass variables to stage0 with some prefix, if that helps.

Knowing that stage0/CMakeLists.txt actually exists on the source tree I suppose it's better if I patch both CMakeList.txt files.
There is an official port, but it's Lean 3. I'll check with the maintainer to see what the plans are for a possible upgrade.

[Sebastian Ullrich]

Mario Carneiro said:

it is interesting that we are shipping lean4 with both stage0 and stage1. Sebastian Ullrich is it possible to remove stage0 from releases? Seems like that just needlessly increases the distribution size

We aren't, I assume @Thanos Tsouanas was talking about the source tarball

[Thanos Tsouanas]

Yes, I was talking about lean4-4.0.0.tar.gz, which comes with stage0. But I got curious: what would «shipping» refer to, if not the source tarball?

[Mario Carneiro]

Lean is primarily delivered to users as "releases", either nightlies or tagged versions

[Mario Carneiro]

e.g. https://github.com/leanprover/lean4/releases/tag/v4.0.0

[Mario Carneiro]

you can also find nightlies on https://github.com/leanprover/lean4-nightly/tags

[Mario Carneiro]

but most people get new nightlies or releases by specifying them in the lean-toolchain and letting elan download the new version from these sources

[Thanos Tsouanas]

Yes; and it was actually harder-than-I-remember-it to spot the source tarball (via the installation instructions website). But it seems to be the only option to try on OpenBSD at the moment.

e.g. https://github.com/leanprover/lean4/releases/tag/v4.0.0

That's exactly where I got the source tarball from, that's why I thought it's part of what's being «shipped» as a release.

[Thanos Tsouanas]

From what I understand elan only looks for something already built/compiled to download, for the specific system it recognizes as being run from; there's no fallback to build from .lean sources having a "bootstrap" minilean or something like that, right? Speaking of which, is the -D CMAKE_BUILD_TYPE=MINSIZEREL option something like that? (I'd appreciate pointers to the documentation about how the procedure works.)

[Sebastian Ullrich]

I don't think we ever used that. The binary size of Lean is not an issue compared to its stdlib size

[Thanos Tsouanas]

With lots of help from Theo Buehler (maintainer of OpenBSD's port for Lean (currently Lean 3)), stage0 managed to build on OpenBSD :tada: :blowfish:
Still, stage1 dies because lean cannot load libleanshared.so:

-- Build files have been written to: /cave/thanos/devel/lean4/lean4-4.1.0/build/release/stage1
[ 62%] Performing build step for 'stage1'
[ 12%] Built target kernel
[ 12%] Built target initialize
[ 17%] Built target constructions
[ 31%] Built target library
[ 50%] Built target compiler
[ 63%] Built target util
[ 63%] Built target leancpp
ld.so: lean: can't load library 'libleanshared.so'
/cave/thanos/devel/lean4/lean4-4.1.0/build/release/stage0/bin/lean --deps Init.lean failed (137):
/cave/thanos/devel/lean4/lean4-4.1.0/build/release/stage1/bin/../share/lean/lean.mk:126: ../build/release/stage1/lib/temp/Init.depend: No such file or directory
make[7]: *** [/cave/thanos/devel/lean4/lean4-4.1.0/build/release/stage1/bin/../share/lean/lean.mk:58: ../build/release/stage1/lib/temp/Init.depend] Error 1
make[6]: *** [/cave/thanos/devel/lean4/lean4-4.1.0/build/release/stage1/stdlib.make:37: Init] Error 2
make[5]: *** [CMakeFiles/make_stdlib.dir/build.make:70: CMakeFiles/make_stdlib] Error 2
make[4]: *** [CMakeFiles/Makefile2:1028: CMakeFiles/make_stdlib.dir/all] Error 2
make[3]: *** [Makefile:146: all] Error 2
make[2]: *** [CMakeFiles/stage1.dir/build.make:86: stage1-prefix/src/stage1-stamp/stage1-build] Error 2
make[1]: *** [CMakeFiles/Makefile2:116: CMakeFiles/stage1.dir/all] Error 2
make: *** [Makefile:136: all] Error 2

Any ideas?
I also noticed that on lean4-4.1.0, the src/CMakeList.txt and stage0/src/CMakeList.txt differ thus:

< set(LEAN_VERSION_MINOR 1)
---
> set(LEAN_VERSION_MINOR 0)

(This is probably something to fix, but unrelated to my issue.)