feat: bundle LLVM on Windows

.github/workflows/ci.yml

@@ -28,6 +28,7 @@ jobs:
             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/13.0.0/lean-llvm-x86_64-linux-gnu.tar.zst
+            prepare-llvm: script/prepare-llvm-linux.sh lean-llvm*
           - name: Linux
             os: ubuntu-latest
             check-stage3: true
@@ -49,9 +50,11 @@ jobs:
             os: windows-2022
             release: true
             shell: msys2 {0}
-            CMAKE_OPTIONS: -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
+            CMAKE_OPTIONS: -G "Unix Makefiles"
             # for reasons unknown, interactivetests are flaky on Windows
             CTEST_OPTIONS: --repeat until-pass:2
+            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/13.0.0/lean-llvm-x86_64-w64-windows-gnu.tar.zst
+            prepare-llvm: script/prepare-llvm-mingw.sh lean-llvm*
       # complete all jobs
       fail-fast: false
     name: ${{ matrix.name }}
@@ -74,7 +77,8 @@ jobs:
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
         with:
-          install: make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git zip unzip diffutils binutils tree mingw-w64-x86_64-zstd
+          msystem: clang64
+          install: make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache git zip unzip diffutils binutils tree mingw-w64-clang-x86_64-zstd tar
         if: matrix.os == 'windows-2022'
       - name: Install Brew Packages
         run: |
@@ -102,10 +106,8 @@ jobs:
           mkdir build
           cd build
           OPTIONS=()
-          if [[ '${{ matrix.llvm-url }}' && "${{ matrix.name }}" == "Linux release" ]]; then
-            wget -q ${{ matrix.llvm-url }}
-            eval "OPTIONS+=($(../script/prepare-llvm-linux.sh lean-llvm*))"
-          fi
+          [[ -z '${{ matrix.llvm-url }}' ]] || wget -q ${{ matrix.llvm-url }}
+          [[ -z '${{ matrix.prepare-llvm }}' ]] || eval "OPTIONS+=($(../${{ matrix.prepare-llvm }}))"
           if [[ $GITHUB_EVENT_NAME == 'schedule' && -n '${{ matrix.release }}' && -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
             git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
             git fetch nightly --tags
@@ -121,7 +123,7 @@ jobs:
           make -j4
           make install
       - name: Check binaries
-        if: matrix.name == 'Linux release'
+        if: matrix.os != 'macos-latest'
         run: |
           ldd -v lean-*/bin/* || true
       - name: Patch
@@ -138,13 +140,6 @@ jobs:
             otool -L $f
           done
           ls -l lib/
-      - name: Patch
-        if: matrix.name == 'Windows'
-        run: |
-          cd build/stage1
-          cp $(ldd bin/lean.exe | cut -f3 -d' ' | grep mingw) bin/
-          ldd bin/lean.exe
-          ls -l bin/
       - name: List Install Tree
         run: |
           # omit contents of src/, Init/, ...

script/prepare-llvm-linux.sh

@@ -3,7 +3,7 @@ set -uo pipefail
 
 # run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in
 # ```
-# eval cmake ../.. $(../../script/prepare-llvm-linux.sh ~/Downloads/clang+llvm-13.0.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz)
+# eval cmake ../.. $(../../script/prepare-llvm-linux.sh ~/Downloads/lean-llvm-x86_64-linux-gnu.tar.zst)
 # ```
 
 # use full LLVM release for compiling C++ code, but subset for compiling C code and distribution

script/prepare-llvm-mingw.sh

@@ -0,0 +1,41 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# run from root build directory in clang64 shell (NOT mingw64) as in
+# ```
+# eval cmake ../.. $(../../script/prepare-llvm-mingw.sh ~/Downloads/lean-llvm-x86_64-w64-windows-gnu.tar.zst)
+# ```
+
+# use full LLVM release for compiling C++ code, but subset for compiling C code and distribution
+
+# must run `tar` twice in case of symlinked files listed before their targets...
+[[ -d llvm ]] || (mkdir llvm; tar xf $1 --dereference --strip-components 1 --directory llvm || tar xf $1 --dereference --strip-components 1 --directory llvm)
+mkdir -p stage1/{bin,lib,include/clang}
+# a C compiler!
+cp llvm/bin/clang stage1/bin/
+# a linker!
+cp llvm/bin/{ld.lld,lld} stage1/bin/
+# dependencies of the above
+cp $(ldd llvm/bin/{clang,lld}.exe | cut -f3 -d' ' --only-delimited | grep llvm) stage1/bin
+# lean.h dependencies
+cp llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang
+# single Windows dependency
+echo '
+// https://docs.microsoft.com/en-us/windows/win32/api/errhandlingapi/nf-errhandlingapi-seterrormode
+#define SEM_FAILCRITICALERRORS 0x0001
+__declspec(dllimport) __stdcall unsigned int SetErrorMode(unsigned int uMode);' > stage1/include/clang/windows.h
+# COFF dependencies
+cp /clang64/x86_64-w64-mingw32/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
+# runtime
+(cd llvm; cp --parents lib/clang/*/lib/*/libclang_rt.builtins* ../stage1)
+# further dependencies
+cp /clang64/x86_64-w64-mingw32/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 " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DLEAN_CXX_STDLIB='-lc++ -lc++abi'"
+echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"
+# allow C++ code to include /usr since it needs quite a few more headers
+echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -I/clang64/include/ -I/clang64/x86_64-w64-mingw32/include/'"
+echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -I ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -lucrtbase -fuse-ld=lld'"
+# do not set `LEAN_CC` for tests
+echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF"
+echo -n " -DLEAN_TEST_VARS=''"

src/CMakeLists.txt

@@ -270,11 +270,11 @@ include_directories(${CMAKE_BINARY_DIR}/include)
 # libleancpp/Lean as well as libleanrt/Init/Std are cyclically dependent. This works by default on macOS, which also doesn't like
 # the linker flags necessary on other platforms.
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean -lleanrt")
+  set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lleancpp -lInit -lStd -lLean -lleanrt")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean -lnodefs.js -lleanrt")
+  set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lleancpp -lInit -lStd -lLean -lnodefs.js -lleanrt")
 else()
-  set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group")
+  set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group")
 endif()
 
 set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")

stage0/src/runtime/io.cpp

@@ -7,6 +7,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 #if defined(LEAN_WINDOWS)
 #include <windows.h>
 #include <io.h>
+#define NOMINMAX // prevent ntdef.h from defining min/max macros
 #include <ntdef.h>
 #include <bcrypt.h>
 #elif defined(__APPLE__)