From ad2fe8de80acb4770444840f75fa488b46c3fb73 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 22 Oct 2021 15:39:11 +0200
Subject: [PATCH] feat: bundle LLVM on macOS

---
 .github/workflows/ci.yml     | 18 +++++------------
 script/prepare-llvm-macos.sh | 39 ++++++++++++++++++++++++++++++++++++
 src/CMakeLists.txt           | 12 ++++-------
 3 files changed, 48 insertions(+), 21 deletions(-)
 create mode 100755 script/prepare-llvm-macos.sh

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 44e29de9a7..ce54f071a6 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -46,6 +46,8 @@ jobs:
             shell: bash -euxo pipefail {0}
             # Mojave, oldest maintained version as of 2021
             CMAKE_OPTIONS: -DCMAKE_OSX_DEPLOYMENT_TARGET=10.14
+            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/13.0.0/lean-llvm-x86_64-apple-darwin.tar.zst
+            prepare-llvm: script/prepare-llvm-macos.sh lean-llvm*
           - name: Windows
             os: windows-2022
             release: true
@@ -82,7 +84,7 @@ jobs:
         if: matrix.os == 'windows-2022'
       - name: Install Brew Packages
         run: |
-          brew install ccache tree zstd
+          brew install ccache tree zstd coreutils
         if: matrix.os == 'macos-latest'
       - name: Cache
         uses: actions/cache@v2
@@ -126,20 +128,10 @@ jobs:
         if: matrix.os != 'macos-latest'
         run: |
           ldd -v lean-*/bin/* || true
-      - name: Patch
+      - name: Check Binaries
         if: matrix.name == 'macOS'
         run: |
-          cd build/stage1
-          cp /usr/local/opt/gmp/lib/libgmp.* lib/
-          for f in lib/lean/libleanshared.dylib bin/lean bin/leanpkg bin/leanc bin/lake; do
-            for lib in $(otool -L $f | tail -n +2 | cut -d' ' -f1); do
-              # copy Homebrew dependencies
-              if [[ "$lib" == /usr/local/opt/* ]]; then cp -n "$lib" lib/ || true; fi
-              [[ "$lib" == /usr/lib/* ]] || install_name_tool -change "$lib" "@rpath/$(basename $lib)" $f
-            done
-            otool -L $f
-          done
-          ls -l lib/
+          otool -L lean-*/bin/* || true
       - name: List Install Tree
         run: |
           # omit contents of src/, Init/, ...
diff --git a/script/prepare-llvm-macos.sh b/script/prepare-llvm-macos.sh
new file mode 100755
index 0000000000..b4c413a590
--- /dev/null
+++ b/script/prepare-llvm-macos.sh
@@ -0,0 +1,39 @@
+#!/usr/bin/env bash
+set -uxo pipefail
+
+# run from root build directory as in
+# ```
+# eval cmake ../.. $(../../script/prepare-llvm-macos.sh)
+# ```
+
+# use full LLVM release for compiling C++ code, but subset for compiling C code and distribution
+
+[[ -d llvm ]] || (mkdir llvm; gtar xf $1 --strip-components 1 --directory llvm)
+SDK=$(xcrun --show-sdk-path)
+mkdir -p stage1/{bin,lib/libc,include/clang}
+CP="gcp -d"  # preserve symlinks
+# a C compiler!
+$CP $(grealpath llvm/bin/clang) stage1/bin/clang
+# a linker!
+gcp llvm/bin/ld64.lld stage1/bin/
+# dependencies of the above
+$CP llvm/lib/lib{clang-cpp,LLVM}.dylib stage1/lib/
+#find stage1 -type f -exec strip --strip-unneeded '{}' \; 2> /dev/null
+# lean.h dependencies
+$CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang
+# runtime
+(cd llvm; $CP --parents lib/clang/*/lib/*/libclang_rt.osx.a ../stage1)
+gcp ${GMP:-/usr/local/opt/gmp}/lib/libgmp.a stage1/lib/
+# libSystem stub, includes libc
+cp $SDK/usr/lib/libSystem.tbd stage1/lib/libc
+# use for linking, use system libs for running
+gcp llvm/lib/lib{c++,c++abi,unwind}.dylib stage1/lib/libc
+echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++"
+# allow C++ code to include /usr since it needs quite a few more headers
+# need no-macro-redefined for weird clang stdint.h
+echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm --stdlib=libc++ -I $SDK/usr/include -Wno-macro-redefined'"
+echo -n " -DGMP_LIBRARIES=lib/libgmp.a -DGMP_INCLUDE_DIR=/usr/local/opt/gmp/include"
+echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -I ROOT/include/clang -Wno-macro-redefined' -DLEANC_CC=ROOT/bin/clang"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
+# do not set `LEAN_CC` for tests
+echo -n " -DLEAN_TEST_VARS=''"
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2ec1848b21..1c67dab805 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -293,8 +293,10 @@ else()
   set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,--gc-sections")
 endif()
 
-set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lm")
-set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lm")
+if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
+  set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lm")
+  set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lm")
+endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
   if(BSYMBOLIC)
@@ -397,12 +399,6 @@ string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
 # These are used in lean.mk (and libleanrt) and passed through by stdlib.make
 # They are not embedded into `leanc` since they are build profile/machine specific
 set(LEANC_OPTS "${LEANC_OPTS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
-if(CMAKE_OSX_SYSROOT)
-  string(APPEND LEANC_OPTS " ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}")
-endif()
-if(CMAKE_OSX_DEPLOYMENT_TARGET)
-  string(APPEND LEANC_OPTS " ${CMAKE_CXX_OSX_DEPLOYMENT_TARGET_FLAG}${CMAKE_OSX_DEPLOYMENT_TARGET}")
-endif()
 
 if(${STAGE} GREATER 1)
   # reuse C++ parts, which don't change