Testing Lean 9.9.9

Stream: general

[Gabriel Ebner]

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]

9.9.9? How long was I asleep for?

[Gabriel Ebner]

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]

+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]

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

[Gabriel Ebner]

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]

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]

or 10.13 or whatever ;)

[Bryan Gin-ge Chen]

FWIW 9.9.9 worked for me on 10.14.6.

[Gabriel Ebner]

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

[Alex J. Best]

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]

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

[Gabriel Ebner]

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]

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

[Alex J. Best]

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

looks good!

[Gabriel Ebner]

Thank you so much!

[Alex J. Best]

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

[Gabriel Ebner]

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]

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