macos sonoma

Stream: mathlib4

[Matthew Ballard]

I got excited about the new snoopy watch face and it ended up with me installing the (first) public beta for MacOS Sonoma. I figured a short report would be useful to some.

Good news (so far): everything already on my machine seems to work ok (including homebrew and nix).

Bad news: Linking libc++.1.dylib fails when compiling cache or runLinter. I guess (I couldn't figure where this was set) rpath is pointing at ./lake-packages/**/build/lib/ because that was where it tried to look for the missing library. I ended up copying the file from my nix store there and was able to do all the usual things with a fresh copy of mathlib.

[Sebastian Ullrich]

That's good to know. Could you elaborate on "linking fails"?

[Matthew Ballard]

Let me regenerate the error message

[Matthew Ballard]

ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib
dyld[46325]: Library not loaded: @rpath/libc++.1.dylib
  Referenced from: <4C4C4449-5555-3144-A15E-70B77DDF95AA> /Users/matt/GitHub/scratch/extra_scratch/mathlib4/build/bin/cache
  Reason: tried: './lake-packages/proofwidgets/build/lib/libc++.1.dylib' (no such file), './lake-packages/Cli/build/lib/libc++.1.dylib' (no such file), './build/lib/libc++.1.dylib' (no such file), './lake-packages/Qq/build/lib/libc++.1.dylib' (no such file), './lake-packages/aesop/build/lib/libc++.1.dylib' (no such file), './lake-packages/std/build/lib/libc++.1.dylib' (no such file)

[Sebastian Ullrich]

I see, that's interesting. We do ship libc++.dylib, now we'd just have to find out why the same clang suddenly decides to choose a different library

[Matthew Ballard]

Is there a difference with libc++.1.dylib or is that just a copy?

[Sebastian Ullrich]

It's probably a symlink even

[Matthew Ballard]

It's seems to physically be in my ./lake-packages/proofwidgets/build/lib (lol).

[Sebastian Ullrich]

uhh

[Matthew Ballard]

That was my doing

[Matthew Ballard]

Perhaps related: it seems the xcode version from ventura is no longer compatible with sonoma. There is a beta for the new version. I installed that plus the beta command line tools but it appeared to have no effect

[Sebastian Ullrich]

The Lean toolchain should be completely separate from xcode

[Sebastian Ullrich]

Which is why I'm confused that updating the OS broke this

[Matthew Ballard]

So it should be searching in ./elan/toolchains/***/?

[Sebastian Ullrich]

Oh you are right, those paths are not even listed under "tried". Could you copy the failed cmdline Lake invoked and append a -v?

[Matthew Ballard]

I am calling lake exe cache get! and -v seems to have no effect on the output. lake exe runLinter has the same behavior

[Matthew Ballard]

I get more info if I run lake -v exe cache get! from a fresh clone.

info: [9/9] Linking cache
info: > /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/leanc -o ./build/bin/cache ./build/ir/Cache/Main.o ./build/ir/Cache/IO.o ./build/ir/Cache/Hashing.o ./build/ir/Cache/Requests.o
info: stderr:
ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib
dyld[48368]: Library not loaded: @rpath/libc++.1.dylib
  Referenced from: <4C4C4449-5555-3144-A15E-70B77DDF95AA> /Users/matt/GitHub/scratch/extra_scratch/mathlib4/build/bin/cache
  Reason: tried: './lake-packages/proofwidgets/build/lib/libc++.1.dylib' (no such file), './lake-packages/Cli/build/lib/libc++.1.dylib' (no such file), './build/lib/libc++.1.dylib' (no such file), './lake-packages/Qq/build/lib/libc++.1.dylib' (no such file), './lake-packages/aesop/build/lib/libc++.1.dylib' (no such file), './lake-packages/std/build/lib/libc++.1.dylib' (no such file)

[Matthew Ballard]

For the warning it looks like some script is generating the file path from xcode version and os version. But that doesn't exist and didn't on Ventura either

[Sebastian Ullrich]

The warning is likely a red herring. Could you run

/Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/leanc -o ./build/bin/cache ./build/ir/Cache/Main.o ./build/ir/Cache/IO.o ./build/ir/Cache/Hashing.o ./build/ir/Cache/Requests.o -v

?

[Matthew Ballard]

/Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/clang -I /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/include -fstack-clash-protection -fvisibility=hidden -nostdinc -isystem /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/include/clang -o ./build/bin/cache ./build/ir/Cache/Main.o ./build/ir/Cache/IO.o ./build/ir/Cache/Hashing.o ./build/ir/Cache/Requests.o -v -L /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/lib -L /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/lib/libc -fuse-ld=lld -L /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/lib/lean -lleancpp -lInit -lLean -lleanrt -lc++ -L /Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib -Wno-unused-command-line-argument
clang version 15.0.1 (https://github.com/llvm/llvm-project b73d2c8c720a8c8e6e73b11be4e27afa6cb75bdf)
Target: arm64-apple-darwin23.0.0
Thread model: posix
InstalledDir: /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin
 "/Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/ld64.lld" -demangle -dynamic -arch arm64 -platform_version macos 14.0.0 14.0.0 -o ./build/bin/cache -L/Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/lib -L/Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/lib/libc -L/Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/lib/lean -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib ./build/ir/Cache/Main.o ./build/ir/Cache/IO.o ./build/ir/Cache/Hashing.o ./build/ir/Cache/Requests.o -lleancpp -lInit -lLean -lleanrt -lc++ -lSystem /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/lib/clang/15.0.1/lib/darwin/libclang_rt.osx.a
ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib

[Matthew Ballard]

The warning is on all MacOS versions afaik

[Matthew Ballard]

Did clang get upgraded with Sonoma?

[Matthew Ballard]

Yes. I think so

[Sebastian Ullrich]

Again, your system toolchain is completely separate from Lean's

[Matthew Ballard]

Ah ok. It ships with clang?

[Sebastian Ullrich]

Yes, see the beginning of the output

[Matthew Ballard]

Ok

[Sebastian Ullrich]

Oh, it's not linking that fails but loading! That makes more sense but doesn't make it easier...

[Matthew Ballard]

Yes, sorry. I should have been more clear

[Sebastian Ullrich]

Then I think we would need to find out what's the proper way of referencing libc++ on that OS. Since you have a system clang installed, could you try LEAN_CC=clang lake build cache?

[Matthew Ballard]

cache builds without errors

[Sebastian Ullrich]

Great! And what does otool -L say on the produced binary?

[Matthew Ballard]

build/bin/cache:
    @rpath/libc++.1.dylib (compatibility version 1.0.0, current version 1.0.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)

[Sebastian Ullrich]

Right :) . Did it actually rebuild? Could you try removing the binary and then run again with LEAN_CC?

[Matthew Ballard]

Yes, I just realized that

[Matthew Ballard]

That works!

[Sebastian Ullrich]

Nice, what does otool say now?

[Matthew Ballard]

It resolves to /usr/lib/libc++.1.dylib

[Sebastian Ullrich]

Mmh, it sounds like /usr/lib used to be implicitly in the rpath but is not anymore...?

[Matthew Ballard]

Same behavior as in Ventura

[Matthew Ballard]

That was my guess but I couldn't figure who was setting that

[Sebastian Ullrich]

It might simply be undocumented behavior of library resolution that has changed now

[Matthew Ballard]

I couldn't find anyone else complaining about with it a cursory google search

[Matthew Ballard]

Much thanks for the help!

[Sebastian Ullrich]

Let's see if we can move towards an upstreamable solution here. Could you run otool -D on the libc++ shipped with Lean?

[Matthew Ballard]

libclang-cpp.dylib? or am I looking in the wrong place

[Matthew Ballard]

Wrong place

[Matthew Ballard]

@rpath/libc++.1.dylib

[Sebastian Ullrich]

Okay, then let's try changing that by running install_name_tool -id /usr/lib/libc++.1.dylib on that file. Does that fix relinking and loading?

[Matthew Ballard]

Yes.

[Sebastian Ullrich]

Awesome, we can do just that in CI! Thanks for the productive remote debugging session :)

[Matthew Ballard]

Thank you!

[Matthew Ballard]

One more question if possible.

/Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/leanc -o ./build/bin/cache ./build/ir/Cache/Main.o ./build/ir/Cache/IO.o ./build/ir/Cache/Hashing.o ./build/ir/Cache/Requests.o -v

expands to

/Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/clang -I /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/include -fstack-clash-protection -fvisibility=hidden -nostdinc -isystem /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/include/clang -o ./build/bin/cache ./build/ir/Cache/Main.o ./build/ir/Cache/IO.o ./build/ir/Cache/Hashing.o ./build/ir/Cache/Requests.o -v -L /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/lib -L /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/lib/libc -fuse-ld=lld -L /Users/matt/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/lib/lean -lleancpp -lInit -lLean -lleanrt -lc++ -L /Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib -Wno-unused-command-line-argument

what is generating the flag

-L /Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib

since everyone on MacOS gets the warning

ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib

[Sebastian Ullrich]

It's probably this one, let's see: https://github.com/leanprover/lean4/pull/2356/commits/3a0daff81f65eebfab5969fc811c8f62b8439fe1

[Sebastian Ullrich]

@Matthew Ballard By the way, do you get any of these

ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 12.6.0, which is newer than target minimum of 10.15.0

warnings on Sonoma?

[Matthew Ballard]

Those disappeared “on their own” while I was on Ventura (unless I never saw them). Not seen yet on Sonoma.

[Sebastian Ullrich]

Strange, one would assume the two versions would only diverge more. But then the PR should be ready to go.

[Matthew Ballard]

For those interested, nix just pulled down elan 2.0.1 so I think it is fully functional through the update (which hasn't always been the case).

[Sebastian Ullrich]

The elan version should not affect any of these

[Matthew Ballard]

Sorry. That was just a statement about the functionality of nix in the beta.

[Sebastian Ullrich]

Ah, that update :)

[Matthew Ballard]

Everything works great with a clean clone of current mathlib! (Just in time for the next beta lol).

[Matthew Ballard]

Thanks again @Sebastian Ullrich