Zulip Chat Archive

Stream: general

Topic: Testing Lean 9.9.9


Gabriel Ebner (May 08 2020 at 12:45):

I'd like to move the community fork to github actions. Can you please test if the binaries built with the new CI work for you?

lean +leanprover-community/lean:9.9.9 --version

In particular, I'd like to hear from people using obscure configurations like macos or windows.

Reid Barton (May 08 2020 at 12:55):

9.9.9? How long was I asleep for?

Gabriel Ebner (May 08 2020 at 12:58):

At first I wanted to release version we-love-bors, but then I realized that elan doesn't support non-numeric versions yet. This is a test release. It will be removed after lean#218 is merged.

Alex J. Best (May 08 2020 at 15:54):

+alex:~ 🐌 lean +leanprover-community/lean:9.9.9 --version
info: downloading component 'lean'
 17.6 MiB /  17.6 MiB (100 %)  16.2 MiB/s ETA:   0 s
info: installing component 'lean'
dyld: lazy symbol binding failed: Symbol not found: ____chkstk_darwin
  Referenced from: /Users/alex/.elan/toolchains/leanprover-community-lean-9.9.9/bin/lean (which was built for Mac OS X 10.15)
  Expected in: /usr/lib/libSystem.B.dylib

dyld: Symbol not found: ____chkstk_darwin
  Referenced from: /Users/alex/.elan/toolchains/leanprover-community-lean-9.9.9/bin/lean (which was built for Mac OS X 10.15)
  Expected in: /usr/lib/libSystem.B.dylib

Abort trap: 6

I guess you are right osx is obscure (i'm on 10.13)

Gabriel Ebner (May 08 2020 at 15:58):

This is good to know! I was just about to release 3.11.0.

Gabriel Ebner (May 08 2020 at 15:58):

Is there anything special you have to do to make binaries work across multiple macos versions? Is it enough to build it on 10.13?

Alex J. Best (May 08 2020 at 15:59):

I'm not sure, some discussion here https://github.com/nodegui/nodegui/issues/391 has some discussion maybe its enough to put "-DCMAKE_OSX_DEPLOYMENT_TARGET=10.12" on line 64 of on-push.yml?

Alex J. Best (May 08 2020 at 16:00):

or 10.13 or whatever ;)

Bryan Gin-ge Chen (May 08 2020 at 16:00):

FWIW 9.9.9 worked for me on 10.14.6.

Gabriel Ebner (May 08 2020 at 16:03):

lean#222. We should have binaries for you to try in about 10 minutes.

Alex J. Best (May 08 2020 at 16:08):

Thanks, I should be able to try them in 15 mins or so, feel free to ping me if I dont respond back!

Yury G. Kudryashov (May 08 2020 at 16:17):

BTW, what are your plans about lean#216 and lean#217?

Gabriel Ebner (May 08 2020 at 16:23):

I think we should merge them right after 3.11. The reason I want to get 3.11 out now is because of lean#211, where we already have a mathlib branch with fixes.

Gabriel Ebner (May 08 2020 at 16:43):

@Alex J. Best The binary is now ready: https://github.com/leanprover-community/lean/suites/665118238/artifacts/5909372

Alex J. Best (May 08 2020 at 16:46):

+alex:~/Downloads/lean-3.10.0-darwin 🐌 ./bin/lean --version
Lean (version 3.10.0, commit 2f4d83bab292, Debug)

looks good!

Gabriel Ebner (May 08 2020 at 16:47):

Thank you so much!

Alex J. Best (May 08 2020 at 16:48):

How do I find the release artifact though, rather than the debug one? Or does it not matter?

Gabriel Ebner (May 08 2020 at 16:50):

That's my fault: lean#223. But since this is a linking error, it shouldn't make a difference whether the build is debug or not.

Ryan Lahfa (Aug 19 2021 at 23:07):

Sorry to revive this thread, but I think the release was never removed (or was it and the GH API is lying?) :P (I was writing some automation to turn releases into automagic Nix derivations and stumbled on the nextgen v9.9.9 and we-love-bors releases :>)


Last updated: Dec 20 2023 at 11:08 UTC