M1 Universal Binary

Stream: lean4

[Julian Berman]

Has anyone successfully compiled a universal binary on macOS (or know whether doing so is possible at the minute)?

I tried rm -rf build/release && mkdir -p build/release && cd build/release && cmake -DCMAKE_OSX_ARCHITECTURES='arm64;x86_64' -DCMAKE_INSTALL_PREFIX=/opt/lean4/nightly/ ../.. && make -j4 SDKROOT=$(xcrun --sdk macosx --show-sdk-path), where CMAKE_OSX_ARCHITECTURES was I thought how to do so, but the resulting binaries are not universal.

[Sebastian Ullrich]

We do many steps such as linking outside of CMake via leanc directly, so I'm not surprised it doesn't work out of the box. But I don't really know how universal binaries are created. Only that our release tarballs are already big enough that it doesn't seem desirable.

[Julian Berman]

Aha, thanks. OK, will try to see if it's easy to dig through the non-cmake bits to add it, I've already needed to do slightly similar things previously to add -fPIC for compiling on Android so maybe doing so won't be too hard. And yeah I definitely am not suggesting release builds be universal.

[Matthew Ballard]

I am curious if there is any progress on this. Am I correct in believing it would allow building of M1 binaries on x86 runners?

[Sebastian Ullrich]

Universal binaries should not make that any easier (probably harder, as by the above) compared to standard cross-compilation. If we want full-featured cross-compiled Lean releases, the first step would be to cross-compile LLVM itself (using our custom build flags) so that we can bundle it... I didn't feel like tackling that particular mountain just yet.