From 8d3af73853a40f69a96e4626ade1946226a542ef Mon Sep 17 00:00:00 2001
From: Henrik <hargonix@gmail.com>
Date: Mon, 31 Jul 2023 21:25:03 +0200
Subject: [PATCH] feat: Linux LLVM CI for stage1+

---
 .github/workflows/ci.yml     | 10 ++++++++++
 script/prepare-llvm-linux.sh |  5 +++--
 script/prepare-llvm-macos.sh |  5 +++--
 script/prepare-llvm-mingw.sh |  1 -
 4 files changed, 16 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index bd2c569714..4e59236e53 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -50,6 +50,16 @@ jobs:
       matrix:
         include:
           # portable release build: use channel with older glibc (2.27)
+          - name: Linux LLVM
+            os: ubuntu-latest
+            release: true
+            shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{}}" --run "bash -euxo pipefail {0}"
+            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst
+            prepare-llvm: ../script/prepare-llvm-linux.sh lean-llvm*
+            binary-check: ldd -v
+            # foreign code may be linked against more recent glibc
+            CTEST_OPTIONS: -E 'foreign|leanlaketest_git'
+            CMAKE_OPTIONS: -DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config
           - name: Linux release
             os: ubuntu-latest
             release: true
diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh
index ac76094b4b..a887d166fb 100755
--- a/script/prepare-llvm-linux.sh
+++ b/script/prepare-llvm-linux.sh
@@ -48,10 +48,11 @@ $CP -r llvm/include/*-*-* llvm-host/include/
 $CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc
 for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
 OPTIONS=()
-echo -n " -DLLVM=ON -DLLVM_CONFIG=$PWD/llvm-host/bin/llvm-config" # manually point to `llvm-config` location
+# forward `--target`
+echo -n " -DLEAN_EXTRA_MAKE_OPTS='${EXTRA_FLAGS:-}'"
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
-echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}' -DLEAN_EXTRA_MAKE_OPTS='${EXTRA_FLAGS:-}'"
+echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
 # use target compiler directly when not cross-compiling
 if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
diff --git a/script/prepare-llvm-macos.sh b/script/prepare-llvm-macos.sh
index 4fe15140e1..0a5890da34 100755
--- a/script/prepare-llvm-macos.sh
+++ b/script/prepare-llvm-macos.sh
@@ -39,11 +39,12 @@ gcp llvm/lib/libc++.dylib stage1/lib/libc
 # make sure we search for the library in /usr/lib instead of the rpath, which should not contain `/usr/lib`
 # and apparently since Sonoma does not do so implicitly either
 install_name_tool -id /usr/lib/libc++.dylib stage1/lib/libc/libc++.dylib
-echo -n " -DLLVM=ON -DLLVM_CONFIG=$PWD/llvm-host/bin/llvm-config" # manually point to `llvm-config` location
+# forward `--target`
+echo -n " -DLEAN_EXTRA_MAKE_OPTS='${EXTRA_FLAGS:-}'"
 echo -n " -DLEAN_STANDALONE=ON"
 # do not change C++ compiler; libc++ etc. being system libraries means there's no danger of conflicts,
 # and the custom clang++ outputs a myriad of warnings when consuming the SDK
-echo -n " -DLEAN_EXTRA_CXX_FLAGS='${EXTRA_FLAGS:-}' -DLEAN_EXTRA_MAKE_OPTS='${EXTRA_FLAGS:-}'"
+echo -n " -DLEAN_EXTRA_CXX_FLAGS='${EXTRA_FLAGS:-}'"
 if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
   gcp $GMP/lib/libgmp.a stage1/lib/
diff --git a/script/prepare-llvm-mingw.sh b/script/prepare-llvm-mingw.sh
index 7a96588971..b30bcd6488 100644
--- a/script/prepare-llvm-mingw.sh
+++ b/script/prepare-llvm-mingw.sh
@@ -32,7 +32,6 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
 (cd llvm; cp --parents lib/clang/*/lib/*/libclang_rt.builtins* ../stage1)
 # further dependencies
 cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase}.* /clang64/lib/libgmp.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
-echo -n " -DLLVM=ON -DLLVM_CONFIG=$PWD/llvm/bin/llvm-config" # manually point to `llvm-config` location
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'"
 echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"