OpenBSD

Stream: general

[Thanos Tsouanas]

I'm trying to install Lean on OpenBSD.
First, I had to remove -ldl from the flags because the build process breaks with:

ld: error: unable to find library -ldl

Ideally, the build process should detect this by itself, so I added the following to src/CMakeLists.txt:

@@ -308,6 +308,10 @@ if (EMSCRIPTEN)
     # no dlopen
 elseif((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
   # TODO(Jared): config dlopen windows support
+elseif(${CMAKE_SYSTEM_NAME} MATCHES "OpenBSD")
+  # OpenBSD does NOT require -lcrypt, -ldl, or -lrt.
+  # The functions provided by these libraries are part of libc.
+  # See: https://www.openbsd.org/faq/ports/guide.html
 else()
   set(EXTRA_LIBS ${EXTRA_LIBS} dl)
 endif()

This solved the missing dl problem but then I hit this:

[ 68%] Built target bin_lean
libc++abi: terminating with uncaught exception of type lean::exception: failed to locate Lean executable location

Apparently the builder is trying to find the Lean executable via /proc, and OpenBSD doesn't use/have procfs.

Obs: Using -j2 it went much further:

[ 98%] Linking CXX executable lean_js
[ 98%] Built target lean_js
gmake: *** [Makefile:166: all] Error 2

...but I suppose the problem is the same.

Found a relevant discussion here, but FreeBSD does have procfs.

Any ideas how I could go about solving this?

[Eric Wieser]

Just to check, which version of Lean?

[Johan Commelin]

@Jean Lo is our local BSD expert. But afaik it was always a bit tricky to get lean up and running on BSD.

[Thanos Tsouanas]

Just to check, which version of Lean?

I just git clone https://github.com/leanprover/lean so I guess it's 3. I'll try now with lean4.

[Gabriel Ebner]

The leanprover/lean repo is outdated. You should be using https://github.com/leanprover-community/lean instead.

[Thanos Tsouanas]

But afaik it was always a bit tricky to get lean up and running on BSD.

Many times it's just a matter of getting rid of some bureaucratic linuxism here or there. I'm hoping that it is the case with Lean.

[Eric Wieser]

Gabriel Ebner said:

The leanprover/lean repo is outdated. You should be using https://github.com/leanprover-community/lean instead.

It's a bit misleading that leanprover/leans readme starts with "Important Lean 3.4.2 is the latest release. ". Should we reword that to prevent new users falling into this trap?

(which would requiring getting Leo to un-archive the repo, edit the readme, then re-archive it)

[Thanos Tsouanas]

The leanprover/lean repo is outdated.

Thanks! Cloning that one to give it a try, also trying lean4..

[Jannis Limperg]

Worth noting that Lean 4 is pre-release, substantially different from Lean 3 and has no libraries at the moment. So depending on what you want to do, it might not be super useful even if you get it to work on BSD. ;)

[Jannis Limperg]

Although you can use Nix to build Lean 4, so if Nix supports OpenBSD, that should work.

[Thanos Tsouanas]

No Nix for OpenBSD :(

[Thanos Tsouanas]

About lean3 vs lean4, if I can get either of them working I'll be happy...

[Thanos Tsouanas]

leanprover-community/lean gives me the exact same problem as the outdated leanprover/lean. I'll try lean4 now.

[Jean Lo]

Johan Commelin said:

Jean Lo is our local BSD expert. But afaik it was always a bit tricky to get lean up and running on BSD.

I'm far from an expert! I only made a lot of noise flailing around trying to get this to work around this time last year :sweat_smile:

I'm not sure if @Thanos Tsouanas has also seen this conversation, and the patch that replaced the bit of code that tries to follow the /proc/<pid>/exe symlink (which is causing the problem you are seeing) with a sysctl call which works on BSD without procfs. That got (the then-current version, 3.14.0, of) Lean to compile, but farther down the thread we discover that there seem to be other problems between 'producing a binary that runs' and 'producing a working Lean'.

Hoping that this is of some help. Unfortunately that was as far as I got before I gave up for the time, so I'd love to know if this gets figured out!

[Thanos Tsouanas]

About lean4: I needed to tweak a few similar things here and there, but I cannot get past this point:

[ 82%] Built target leancpp
error: failed to locate application
/cave/thanos/lean/lean4/build/release/stage1/bin/../share/lean/lean.mk:99: ../build/release/stage1/lib/temp/Init.depend: No such file or directory
make[7]: *** [/cave/thanos/lean/lean4/build/release/stage1/bin/../share/lean/lean.mk:51: ../build/release/stage1/lib/temp/Init.depend] Error 1

Not sure what this DEPS at line 99 of lean.mk is supposed to include, nor if a Init.depend file should really exist.

[Thanos Tsouanas]

@Jean Lo , thanks for the link, I had not seen that conversation; I'll look into it and the corresponding patch.
Do you remember what problems were encountered "farther down the thread"?

[Jean Lo]

Thanos Tsouanas said:

Jean Lo , thanks for the link, I had not seen that conversation; I'll look into it and the corresponding patch.
Do you remember what problems were encountered "farther down the thread"?

Unfortunately I don't have a lot to say beyond what is written down in the thread itself: that the compiled binary trips over when it tries to compile mathlib, that we tried to see if we could figure out what was wrong by looking at which unit tests it failed, and that we didn't come up with anything conclusive in the end, I think. There are test logs posted in the thread, but since this is an old version of Lean, I suspect those logs are less enlightening than the ones that you can get by running the tests of the current version of Lean once it's built.

[Thanos Tsouanas]

Thanks! Since lean4 failed to build as well, I'll go back to lean3, try the FreeBSD patches on OpenBSD with possible adjustments and see if I can get it to compile and run those tests. On it..

[Thanos Tsouanas]

I managed to build a binary but the test results are worse than the previous ones (which were both on an older version of lean and also on a different OS (FreeBSD):

67% tests passed, 467 tests failed out of 1415

I'm attatching the fails. OpenBSD_test_fails

[Thanos Tsouanas]

(How) can I get a more verbose output on those failed tests?

[Thanos Tsouanas]

Progress! Turns out that all problems so far have been bit of linuxism here and there! 465 of those 467 failed tests was due to a non-posix flag to diff, so switching to GNU diff (available on OpenBSD as a package) we now have 99% tests passed!:

99% tests passed, 2 tests failed out of 1415

Total Test time (real) = 612.87 sec

The following tests FAILED:
          1 - style_check (Failed)
        626 - leanruntest_async_map.lean (Failed)

[Thanos Tsouanas]

The first one, style_check isn't important cause all its errors are about the files I had to tamper with so it's easily fixable and inessential.

[Thanos Tsouanas]

So there's currently exactly one failed test: 626 - leanruntest_async_map.lean:

626/1415 Testing: leanruntest_async_map.lean
626/1415 Test: leanruntest_async_map.lean
Command: "/usr/local/bin/bash" "./test_single.sh" "/cave/thanos/lean/lean/build/release/shell/lean" "async_map.lean"
Directory: /cave/thanos/lean/lean/src/../tests/lean/run
"leanruntest_async_map.lean" start time: Jul 01 09:00 -03
Output:
----------------------------------------------------------
-- testing async_map.lean
-- using result from test_all.sh
failed async_map.lean
<end of output>
Test time =   0.03 sec
----------------------------------------------------------
Test Failed.
"leanruntest_async_map.lean" end time: Jul 01 09:00 -03
"leanruntest_async_map.lean" time elapsed: 00:00:00

[Thanos Tsouanas]

async_map.lean is this one:

meta def list.async_map {α β} (f : α → β) (xs : list α) : list β :=
(xs.map (λ x, task.delay $ λ _, f x)).map task.get

#eval ((list.range 1000000).async_map (+1)).foldl (+) 0

[Thanos Tsouanas]

The output of the failed test doesn't seem particularly helpful. Anybody can share some light on what this async_map is, if/how it is using the system, etc.?

[Gabriel Ebner]

Can you run lean async_map.lean and post the error you get?

[Thanos Tsouanas]

Oh, I hadn't realized it was so simple to run those tests, thanks!

[Thanos Tsouanas]

So, lean async_map.lean produced no standard output but got Segmentation fault.

[Thanos Tsouanas]

Ok, somewhat of a success with this failed test too:
Changing the 1000000 of that #eval to a smaller number like 1000 completed the test successfully.
I changed it back to 1000000 but used ulimit -Sd 8388608 and again, the test completes successfully.

[Thanos Tsouanas]

So: with minor/insignificant tweaks lean3 compiles on OpenBSD and passes 100% of the tests! :tada:

[Thanos Tsouanas]

One thing that might be worrying, but I am probably wrong: usually one would use ulimit -Sd to avoid "out of memory" errors, not segfaults. However, this segfault went away this way. It gives me the impression that there might be something wrong in the code that leads to an unnecessary segfault.

[Gabriel Ebner]

The segfault looks like a stack overflow to me. On linux, we can detect the stack size (see stackinfo.cpp and thread.cpp) and throw an exception instead of overflowing. Maybe this doesn't work on openbsd?

[Thanos Tsouanas]

Hmmm I found two different stackinfo.cpp:
tests/util/stackinfo.cpp and util/stackinfo.cpp
I think that the non-tests version should work on OpenBSD, it seems to be calling getrlimit(2).

[Gabriel Ebner]

Yeah, I'm just guessing here. Can you run lean in a debugger and capture a stacktrace?

[Thanos Tsouanas]

The __APPLE__ version and the "else" version are identical, and should work correctly on OpenBSD.
But I'm not sure this stackinfo.cpp is relevant when I'm running the tests, maybe the other one is?

#if defined(LEAN_WINDOWS)
size_t get_stack_size(int main) {
    if (main) {
        return LEAN_WIN_STACK_SIZE;
    } else {
        return lthread::get_thread_stack_size();
    }
}
#elif defined (__APPLE__)
size_t get_stack_size(int main) {
    if (main) {
        // Retrieve stack size of the main thread.
        struct rlimit curr;
        if (getrlimit(RLIMIT_STACK, &curr) != 0) {
            throw_get_stack_size_failed();
        }
        return curr.rlim_cur;
    } else {
        return lthread::get_thread_stack_size();
    }
}
#else
size_t get_stack_size(int main) {
    if (main) {
        // Retrieve stack size of the main thread.
        struct rlimit curr;
        if (getrlimit(RLIMIT_STACK, &curr) != 0) {
            throw_get_stack_size_failed();
        }
        return curr.rlim_cur;
    } else {
        return lthread::get_thread_stack_size();
    }
}
#endif

[Thanos Tsouanas]

(Is there a reason that the two stackinfo.cpp files are different, or have they just fallen out of sync?)

[Gabriel Ebner]

There's only one stackinfo.cpp file, and it's in src/util/stackinfo.cpp. All of this is complete speculation, but a segfault that goes away with a ulimit change sounds very much like a stack overflow, and the detection code is not particularly portable. I wouldn't be surprised if save_stack_info was miscompiled on openbsd, or if the thread stack size was not set correctly (or silently truncated by the wrong ulimit setting?).

[Thanos Tsouanas]

There's only one stackinfo.cpp file, and it's in src/util/stackinfo.cpp.

There are two:

• https://github.com/leanprover-community/lean/blob/master/src/util/stackinfo.cpp
• https://github.com/leanprover-community/lean/blob/master/src/tests/util/stackinfo.cpp

[Thanos Tsouanas]

Playing with different ulimit values I got some that it segfaults, one non-reproducable that SIGABRT'ed, and for small values it seem to be stuck (it was running 6 hours without any output). Starting from values of about 2G it terminates successfully.

[Thanos Tsouanas]

Some questions, in no particular order:
(a) Does it seem safe to assume that Lean should work fine on my system given that it passed 100% of the tests?
(b) On the async_map test, the number 1000000 has any particular reason behind it? I mean.. would it serve the same purpose if it was changed to 100000 or to 10000000?
(c) Still curious about the two stackinfo.cpp, which from @Gabriel Ebner 's answer I suppose the second one shouldn't exist..?
(d) Any hopes in getting someone to apply the tweaks "upstream" so that installation on OpenBSD becomes trivial? If so, who would be the right person to bughelp with this?

[Gabriel Ebner]

The tests one is the the test (as the name implies), it's not used in lean.

[Gabriel Ebner]

The meaning of 1000000 is "it should work for large lists". If it can be worked around by setting the correct ulimit, then I would leave the test as it is.

[Gabriel Ebner]

For other portability fixes, please file a PR at https://github.com/leanprover-community/lean

[Thanos Tsouanas]

Thanks a lot for the replies, @Gabriel Ebner! :D

The tests one is the the test (as the name implies), it's not used in lean.

Their methods of getting the stack size are different (trying to understand why), so when the tests are run, which of the two is used?

The meaning of 1000000 is "it should work for large lists".

Thought so! I was wondering if there is something in mathlib (or some other widely used lib) that specifically demands "around such a high number" already. I still think that the ulimit "fix" is more of a dirty hack than an actual fix. Curious if on mac os it passes this test with a "low" ulimit like 1500000.

[Thanos Tsouanas]

For other portability fixes, please file a PR

Perfect, thanks again!

[Gabriel Ebner]

Thanos Tsouanas said:

Their methods of getting the stack size are different (trying to understand why), so when the tests are run, which of the two is used?

I'm not sure I see the difference. Both the test as well as Lean core use save_stack_info to save a pointer to the start of the stack, and then use get_used_stack_size to see how far are now away from the original pointer (= how much stack space we've used).

In either case, the test that fails for you makes no use of src/tests/util/stackinfo.cpp whatsoever.

[Thanos Tsouanas]

Ah, I see now. The tests one actually uses the core one, so the things that seemed to be missing, are actually there, just under the carpet.

In either case, the test that fails for you makes no use of src/tests/util/stackinfo.cpp whatsoever.

Perfect, so one less place to look for possible fixes.

[Thanos Tsouanas]

If someone with access to a mac os system can check this particular test (async_map) with a few low ulimitvalues like 1500000, 1000000, etc. , I'd be grateful.

[Moritz Buhl]

Thanos Tsouanas said:

So: with minor/insignificant tweaks lean3 compiles on OpenBSD and passes 100% of the tests! :tada:

Is there any chance that you will build a port out of this?

[Thanos Tsouanas]

That's the idea but the best route is to first see if we can get those tweaks upstream. I will file a PR as Gabriel Ebner suggested. But first I'd like to use it a bit to see if it's usable/stable-ish.

[Jean Lo]

Thanos Tsouanas said:

So: with minor/insignificant tweaks lean3 compiles on OpenBSD and passes 100% of the tests! :tada:

Love to see this! thanks so much for your work on this & eagerly awaiting the fixes to be upstreamed.

[Thanos Tsouanas]

So, took a break to play the NNG, seemed to work great on my browser (though it seems that sometimes one needs to hit an extra enter to get an extra blank line, in order for it to register that it's complete).

Now back on trying to run things on my own system.
I see elan is not available, but leanproject installed fine.
I tried running it inside the tutorials dir, the leanproject check runs fine and lies to my face with a "Everything looks fine." message.
But trying to run something like leanproject build I get:

[Errno 2] No such file or directory: 'leanpkg'

[Thanos Tsouanas]

How/where/when is leanpkg normally installed?

[Bryan Gin-ge Chen]

leanpkg comes with lean, you might try adding an alias to it.

[Thanos Tsouanas]

Lean-mode seems to be working OK in Emacs, but I would like to install mathlib (even if it's in a "manual" way, and not auto-handled by elan/leanproject and whatnot).

[Thanos Tsouanas]

Aaaaah! Thanks @Bryan Gin-ge Chen , I had missed that!

[Bryan Gin-ge Chen]

I think you can have it point to bin/leanpkg in your lean directory.

[Thanos Tsouanas]

Yes, that's what I did, and now leanproject build is downloading some stuff..

[Thanos Tsouanas]

Still, would it be possible/sensible to simply install mathlib (and update it every now and then) somewhere under lean's path and use lean independently of the elan/leanproject toolchain? (Via Emacs's lean-mode.)

[Bryan Gin-ge Chen]

It is possible with leanproject global-install, but not recommended since different projects can depend on different versions of mathlib.

[Thanos Tsouanas]

So if elan was available for OpenBSD, elan would be the tool to organize all this for me, right? Having various versions installed on my system (of lean, mathlib, etc.), and selecting the right one for each project based on the project's leanpkg.toml. Is it more-or-less like this?

[Bryan Gin-ge Chen]

Yep, that's right! In case you haven't already seen it, there's a bit of explanation here: https://leanprover-community.github.io/toolchain.html

[Thanos Tsouanas]

Thanks!! I had come across this website, but lost it afterwards and was looking for it! Ehehe... Btw, I think in this site the text about adding a symlink to lean should be altered to mention leanpkg as well.

[Bryan Gin-ge Chen]

Good idea! Do you mind making a PR? The source file is here: https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/toolchain.md

[Gabriel Ebner]

Thanos Tsouanas said:

So if elan was available for OpenBSD, elan would be the tool to organize all this for me, right?

Don't expect too much. elan downloads binary builds of lean (and we only build for amd64 linux and some other proprietary operating systems). You can still use elan to manage locally-built versions of lean, but it's only half the fun.

[Bryan Gin-ge Chen]

There's no reason we couldn't distribute OpenBSD binaries though, if Thanos submits a suitable patch.

[Bryan Gin-ge Chen]

Oh wait, I guess it might be tricky to build with GitHub actions.

[Gabriel Ebner]

Yes, that's also the reason we don't have builds for aarch64 linux and aarch64 mac.

[Thanos Tsouanas]

What is the deal with GitHub actions? Sorry, I'm afraid I've only used github for personal projects so far, which is why I'm delaying the PR's here. But getting on to it soon.

[Thanos Tsouanas]

(And that leanproject build inside the tutorials is still compiling, so it really seems like a good idea to have binary versions available.. )

[Thanos Tsouanas]

Once i'm done with the tutorials, in order to avoid recompiling the whole thing, could I simply copy the mathlib dir in some "more general" place and then add it to lean's path by editing ~/.lean/leanpkg.path ?

[Patrick Massot]

Thanos Tsouanas said:

I tried running it inside the tutorials dir, the leanproject check runs fine and lies to my face with a "Everything looks fine." message.

That's not a lie, that's you misunderstanding what this command is checking. And, as explained in the first paragraph of the README:

the tools described here won't give you anything if Lean itself is not available

[Thanos Tsouanas]

Hah, thanks, I was half-joking about the lying thing. I wasn't expecting leanproject to actually come with lean/leanpkg included or anything like that; I just thought that missing... lean would be mentioned at least as a warning.

[Thanos Tsouanas]

But it does make sense after your message, so thanks again! I guess it checks the project directory itself and not the toolkit one might need to actually use such project.

[Julian Berman]

never mind this sort of thing was already mentioned above

[Patrick Massot]

Actually this check command could be removed since it fights an issue that is no longer present. As explained in leanprojet -h, it only checks that olean files (ie compiled lean files) are more recent than their source. Lean used to use timestamps to decide whether it should recompile stuff, and there were ways to mess up the timestamps without actually needing to recompile, hence wasting a lot of time and computing power.

[Thanos Tsouanas]

(I noticed also that in the source it checks both mathlib and core olean files, but in the description it mentions only mathlib ones.)
Thanks for the explanation, and good to know that the to-compile-or-not-to-compile became more sophisticated!

[Moritz Buhl]

Any news on this?

[Alex J. Best]

I think tagging @Thanos Tsouanas to be sure he sees this is a good idea.

[Moritz Buhl]

I thought about the get_exe_location function a bit:
OpenBSD does not offer a way to locate the binary. It would be possible to use argv[0] and PATH (if argv[0] is only the binary name) or cwd (if it is a path). Getting argv0 to the utility function should be terrible. And all this for two locations where this function is called.
Java is using the environment variable JAVA_HOME in a similar way, is this an option for lean3?

[Moritz Buhl]

tb has this https://marc.info/?l=openbsd-ports&m=162914200004765&w=2

[Thanos Tsouanas]

Thanks for tagging me @Alex J. Best, and sorry for the 4-month hiatus over here!
Happy and grateful to see that in the meantime tb created a Lean port for OpenBSD, as @Moritz Buhl mentioned, making it so much easier to play with Lean natively! (Lean v3.32.1 made it to the OpenBSD 7.0 release, and since last week OpenBSD-current has v3.35.1!)