From 2b5b7199e5fb14bdbac4937d658e5ee44245660d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 8 Sep 2021 18:56:19 +0200 Subject: [PATCH 01/16] chore: use CMake C compiler & GMP when running tests In particular, use ccache if used for build --- src/shell/CMakeLists.txt | 38 +++++++++++++++++---------------- tests/compiler/foreign/Makefile | 5 +++-- 2 files changed, 23 insertions(+), 20 deletions(-) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 005f20f32338..214aef615508 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -46,6 +46,8 @@ add_test(lean_ghash2 "${CMAKE_BINARY_DIR}/bin/lean" --githash) add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "-z") add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_BINARY_DIR}/bin/lean" "boofoo.lean") +set(TEST_VARS "PATH=${LEAN_BIN}:$PATH LEAN_CC='${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER}' LEANC_GMP=${GMP_LIBRARIES}") + # LEAN TESTS file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") FOREACH(T ${LEANTESTS}) @@ -53,7 +55,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leantest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -64,7 +66,7 @@ FOREACH(T ${LEANRUNTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanruntest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -74,15 +76,15 @@ FOREACH(T ${LEANCOMPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leancomptest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T) add_test(NAME leancomptest_foreign WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler/foreign" - COMMAND bash -c "${LEAN_BIN}/leanmake --always-make && ./build/bin/test") + COMMAND bash -c "${TEST_VARS} leanmake --always-make CPP=${CMAKE_CXX_COMPILER} && ./build/bin/test") add_test(NAME leancomptest_doc_example WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler" - COMMAND bash -c "${LEAN_BIN}/leanmake --always-make bin && ./build/bin/test hello world") + COMMAND bash -c "${TEST_VARS} leanmake --always-make bin && ./build/bin/test hello world") # LEAN INTERPRETER TESTS file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean") @@ -91,7 +93,7 @@ FOREACH(T ${LEANINTERPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leaninterptest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single_interpret.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single_interpret.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -103,7 +105,7 @@ FOREACH(T_OUT ${LEANBENCHTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanbenchtest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/bench" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T_OUT) file(GLOB LEANINTERPTESTS "${LEAN_SOURCE_DIR}/../tests/plugin/*.lean") @@ -111,7 +113,7 @@ FOREACH(T ${LEANINTERPTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanplugintest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/plugin" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T) # LEAN TESTS using --trust=0 @@ -120,7 +122,7 @@ FOREACH(T ${LEANT0TESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leant0test_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") ENDFOREACH(T) # LEAN SERVER TESTS @@ -130,7 +132,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leanservertest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/server" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -141,7 +143,7 @@ FOREACH(T ${LEANTESTS}) GET_FILENAME_COMPONENT(T_NAME ${T} NAME) add_test(NAME "leaninteractivetest_${T_NAME}" WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" - COMMAND bash -c "PATH=${LEAN_BIN}:$PATH ./test_single.sh ${T_NAME}") + COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}") endif() ENDFOREACH(T) @@ -149,7 +151,7 @@ add_test(NAME leanpkgtest WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/b" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} leanpkg build # linking requires some manual steps (cd ../a; leanpkg build lib) @@ -160,14 +162,14 @@ add_test(NAME leanpkgtest_cyclic WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/cyclic" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} leanpkg build 2>&1 | grep 'import cycle'") add_test(NAME leanpkgtest_user_ext WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_ext" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake | grep 'world, hello, test'") @@ -175,7 +177,7 @@ add_test(NAME leanpkgtest_user_attr WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake") @@ -183,7 +185,7 @@ add_test(NAME leanpkgtest_user_opt WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_opt" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake") @@ -191,7 +193,7 @@ add_test(NAME leanpkgtest_prv WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/prv" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake 2>&1 | grep 'error: field.*private'") @@ -199,6 +201,6 @@ add_test(NAME leanpkgtest_user_attr_app WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr_app" COMMAND bash -c " set -eu - export PATH=${LEAN_BIN}:$PATH + export ${TEST_VARS} find . -name '*.olean' -delete leanmake bin LINK_OPTS='${LEAN_DYN_EXE_LINKER_FLAGS}' && build/bin/UserAttr") diff --git a/tests/compiler/foreign/Makefile b/tests/compiler/foreign/Makefile index 63601a2de38e..efca965baaa0 100644 --- a/tests/compiler/foreign/Makefile +++ b/tests/compiler/foreign/Makefile @@ -1,4 +1,5 @@ PKG = main +CPP = c++ CPPFLAGS = -O3 include lean.mk @@ -9,7 +10,7 @@ all: $(BIN_OUT)/test $(OUT)/testcpp/%.o: %.cpp @mkdir -p "$(@D)" - c++ -std=c++14 -c -o $@ $< $(CPPFLAGS) `leanc --print-cflags` + $(CPP) -std=c++14 -c -o $@ $< $(CPPFLAGS) `leanc --print-cflags` $(BIN_OUT)/test: $(LIB_OUT)/libmain.a $(CPP_OBJS) | $(BIN_OUT) - c++ -o $@ $^ `leanc --print-ldflags` + $(CPP) -o $@ $^ `leanc --print-ldflags` From ac79254777043fc7950cd5c3d15a29e830316a0a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 8 Sep 2021 19:22:00 +0200 Subject: [PATCH 02/16] fix: leanc: add lib/ to library search path --- src/bin/leanc.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/bin/leanc.in b/src/bin/leanc.in index e6bb09797aff..aa12f55fd96e 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -1,7 +1,7 @@ #!/usr/bin/env bash # used only for building Lean itself root=$(dirname $0) -ldflags=("-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@) +ldflags=("-L$root/lib" "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@) for arg in "$@"; do # ccache doesn't like linker flags being passed here [[ "$arg" = "-c" ]] && ldflags=() From feee0b9ed01e90230c58a8fac430cd88ea6e49b8 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 8 Sep 2021 18:58:57 +0200 Subject: [PATCH 03/16] feat: CI: build & distribute release builds with Zig --- .github/workflows/ci.yml | 24 +++++++++++++++++++----- src/CMakeLists.txt | 21 +++++++++++++++++---- src/zigc++.in | 2 ++ src/zigcc.in | 2 ++ 4 files changed, 40 insertions(+), 9 deletions(-) create mode 100755 src/zigc++.in create mode 100755 src/zigcc.in diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ae58694679a1..c81e23cae3a2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -22,11 +22,13 @@ jobs: strategy: matrix: include: - # portable release build: link most libraries statically and use channel with older glibc (2.27; LLVM 7) - name: Linux release os: ubuntu-latest release: true - shell: nix-shell --arg pkgs "import (fetchTarball \"channel:nixos-19.03\") {{}}" --argstr llvmPackages latest --run "bash -euxo pipefail {0}" + zig-url: https://ziglang.org/download/0.8.1/zig-linux-x86_64-0.8.1.tar.xz + # link against older glibc for compatibility + ZIG_ARGS: -target x86_64-linux-gnu.2.15 + # separate job because Zig can't build stage 2 (yet) - name: Linux os: ubuntu-latest check-stage3: true @@ -44,6 +46,7 @@ jobs: shell: bash -euxo pipefail {0} # Mojave, oldest maintained version as of 2021 CMAKE_OPTIONS: -DCMAKE_OSX_DEPLOYMENT_TARGET=10.14 + zig-url: https://ziglang.org/download/0.8.1/zig-macos-x86_64-0.8.1.tar.xz - name: Windows os: windows-2022 release: true @@ -51,6 +54,7 @@ jobs: CMAKE_OPTIONS: -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ # for reasons unknown, interactivetests are flaky on Windows CTEST_OPTIONS: --repeat until-pass:2 + zig-url: https://ziglang.org/download/0.8.1/zig-windows-x86_64-0.8.1.zip # complete all jobs fail-fast: false name: ${{ matrix.name }} @@ -99,18 +103,24 @@ jobs: run: | mkdir build cd build - OPTIONS= + OPTIONS=() + if [ -n "${{ matrix.zig-url }}" ]; then + wget -q ${{ matrix.zig-url }} + [ -e "zig-*.zip" ] && unzip zig-* || tar xf zig-* + find . -type d -name 'zig-*' -exec mv {} zig \; -prune + OPTIONS+=(-DZIG_ROOT=$PWD/zig -DZIG_ARGS='${{ matrix.ZIG_ARGS }}' -DLEANC_CC='./zig/zig cc ${{ matrix.ZIG_ARGS }}') + fi 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 LEAN_VERSION_STRING="nightly-$(date -u +%F)" # do nothing if commit already has a different tag if [[ $(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo $LEAN_VERSION_STRING) == $LEAN_VERSION_STRING ]]; then - OPTIONS=-DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING + OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=$LEAN_VERSION_STRING) echo "LEAN_VERSION_STRING=$LEAN_VERSION_STRING" >> $GITHUB_ENV fi fi - cmake .. ${{ matrix.CMAKE_OPTIONS }} $OPTIONS + cmake .. ${{ matrix.CMAKE_OPTIONS }} "${OPTIONS[@]}" make -j4 # de-Nix-ify binaries - name: Patch @@ -146,6 +156,10 @@ jobs: cp $(ldd bin/lean.exe | cut -f3 -d' ' | grep mingw) bin/ ldd bin/lean.exe ls -l bin/ + - name: Take Off Every Zig + run: | + cp -r build/zig/ build/stage1/bin + if: matrix.release - name: Test Binary without Nix Shell if: matrix.name != 'Windows' shell: bash {0} diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 65cfaf77f5c6..93ec23a3f27c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -64,6 +64,15 @@ option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current ver set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make") set(LEANC_CC "cc" CACHE STRING "C compiler to use in `leanc`") +set(ZIG_ROOT "" CACHE STRING "Zig compiler to use for compilation") + +if (ZIG_ROOT) + configure_file(zigcc.in zigcc) + set(CMAKE_C_COMPILER ${CMAKE_BINARY_DIR}/zigcc) + configure_file(zigc++.in zigc++) + set(CMAKE_CXX_COMPILER ${CMAKE_BINARY_DIR}/zigc++) + set(CMAKE_CXX_COMPILER_ID Clang) +endif() if ("${FAKE_FREE}" MATCHES "ON") set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_FAKE_FREE") @@ -245,6 +254,9 @@ if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten") else() # GMP find_package(GMP 5.0.5 REQUIRED) + # without this, cmake removes the include below inside a Nix shell because it is in CMAKE_INCLUDE_PATH, + # but without it Zig won't find GMP because it doesn't use NIX_CFLAGS_COMPILE + unset(CMAKE_CXX_IMPLICIT_INCLUDE_DIRECTORIES) include_directories(${GMP_INCLUDE_DIR}) # dlopen set(EXTRA_LIBS ${EXTRA_LIBS} ${CMAKE_DL_LIBS}) @@ -264,8 +276,6 @@ endif() # Python find_package(PythonInterp) -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") @@ -276,7 +286,7 @@ else() set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lStd -lleanrt -Wl,--end-group") endif() -if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") +if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin" OR ZIG_ROOT) set(LEANC_STATIC_LINKER_FLAGS "${LEANC_STATIC_LINKER_FLAGS} -lc++") set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -lc++") else() @@ -430,7 +440,10 @@ string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) # These are used in lean.mk and passed through by stdlib.make set(LEANC_OPTS "${LEANC_OPTS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT} ${CMAKE_CXX_OSX_DEPLOYMENT_TARGET_FLAG}${CMAKE_OSX_DEPLOYMENT_TARGET}") -if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") +if(ZIG_ROOT) + # workaround for `--whole-archive` missing from `zig ld` + set(LEANSHARED_LINKER_FLAGS "`find ${CMAKE_BINARY_DIR} -regextype posix-extended -regex '.*/(Leanpkg|runtmp|shell).*' -prune -o -name '*.o' -print` ${LEANSHARED_LINKER_FLAGS}") +elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") else() set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") diff --git a/src/zigc++.in b/src/zigc++.in new file mode 100755 index 000000000000..6e44cd68c8d5 --- /dev/null +++ b/src/zigc++.in @@ -0,0 +1,2 @@ +#!/usr/bin/env sh +${ZIG_ROOT}/zig c++ ${ZIG_ARGS} "$@" diff --git a/src/zigcc.in b/src/zigcc.in new file mode 100755 index 000000000000..00f5dff05132 --- /dev/null +++ b/src/zigcc.in @@ -0,0 +1,2 @@ +#!/usr/bin/env sh +${ZIG_ROOT}/zig cc ${ZIG_ARGS} "$@" From 925ea9c9785b6ebbfba50e982220126a05a4772d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 10 Sep 2021 15:35:15 +0200 Subject: [PATCH 04/16] fix: disable AUTO_THREAD_FINALIZATION with Zig/Windows needs pthread.h --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c81e23cae3a2..7719254d0691 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -51,7 +51,7 @@ 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" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DAUTO_THREAD_FINALIZATION=OFF # for reasons unknown, interactivetests are flaky on Windows CTEST_OPTIONS: --repeat until-pass:2 zig-url: https://ziglang.org/download/0.8.1/zig-windows-x86_64-0.8.1.zip From e06ad7930d3f07da6cb3b95d3fd6506c94994f00 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 10 Sep 2021 15:32:56 +0200 Subject: [PATCH 05/16] fix: including ntdef.h with Zig --- src/runtime/io.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index fc9d373c433d..933bd74baabf 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -7,6 +7,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich #if defined(LEAN_WINDOWS) #include #include +#define NOMINMAX // prevent ntdef.h from defining min/max macros #include #include #elif defined(__APPLE__) From 0d2f12c8e72938c4c7565890d8aa89f2c291155f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 10 Sep 2021 17:50:10 +0200 Subject: [PATCH 06/16] fix: overlong cmdline on Windows --- src/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 93ec23a3f27c..c2831f3f3f36 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -442,7 +442,7 @@ set(LEANC_OPTS "${LEANC_OPTS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} $ if(ZIG_ROOT) # workaround for `--whole-archive` missing from `zig ld` - set(LEANSHARED_LINKER_FLAGS "`find ${CMAKE_BINARY_DIR} -regextype posix-extended -regex '.*/(Leanpkg|runtmp|shell).*' -prune -o -name '*.o' -print` ${LEANSHARED_LINKER_FLAGS}") + set(LEANSHARED_LINKER_FLAGS "@`find ${CMAKE_BINARY_DIR} -regextype posix-extended -regex '.*/(Leanpkg|runtmp|shell).*' -prune -o -name '*.o' -print > ${CMAKE_BINARY_DIR}/libleansharedinputs; echo ${CMAKE_BINARY_DIR}/libleansharedinputs` ${LEANSHARED_LINKER_FLAGS}") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") else() From a6e6faf932829aef85911e38a15c7ab854bffebf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 14 Sep 2021 10:49:44 +0200 Subject: [PATCH 07/16] fix: collection of object files on Windows, shorter linker cmdline --- src/CMakeLists.txt | 9 +++++---- src/stdlib.make.in | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c2831f3f3f36..b51e6a14afa6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -442,14 +442,15 @@ set(LEANC_OPTS "${LEANC_OPTS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} $ if(ZIG_ROOT) # workaround for `--whole-archive` missing from `zig ld` - set(LEANSHARED_LINKER_FLAGS "@`find ${CMAKE_BINARY_DIR} -regextype posix-extended -regex '.*/(Leanpkg|runtmp|shell).*' -prune -o -name '*.o' -print > ${CMAKE_BINARY_DIR}/libleansharedinputs; echo ${CMAKE_BINARY_DIR}/libleansharedinputs` ${LEANSHARED_LINKER_FLAGS}") + set(LEANSHARED_LINKER_FLAGS "`find . -regextype posix-extended -regex '.*/(Leanpkg|runtmp|shell).*' -prune -o -regex '.*\.o(bj)?' -print` ${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") else() set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") - if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") - set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a") - endif() +endif() + +if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") + set(LEANSHARED_LINKER_FLAGS "${LEANSHARED_LINKER_FLAGS} -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a") endif() # Escape for `make`. Yes, twice. diff --git a/src/stdlib.make.in b/src/stdlib.make.in index c5eacb6b8926..aa5c659c0af0 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -42,7 +42,7 @@ Lean: Init Std # we specify the precise file names here to avoid rebuilds ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${LIB}/lean/libStd.a ${LIB}/lean/libLean.a ${LIB}/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a @echo "[ ] Building $@" - "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${LEANSHARED_LINKER_FLAGS} ${LEANC_OPTS} + cd ${CMAKE_BINARY_DIR}; ./leanc.sh -shared -o $@ ${LEANSHARED_LINKER_FLAGS} ${LEANC_OPTS} -v leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} From 309b6c8362b81e9bc5a4f8659193a5ad7c969d3a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 15 Sep 2021 11:48:11 +0200 Subject: [PATCH 08/16] chore: Zig: disable LTO --- src/CMakeLists.txt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b51e6a14afa6..6700180d510e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -67,6 +67,9 @@ set(LEANC_CC "cc" CACHE STRING "C compiler set(ZIG_ROOT "" CACHE STRING "Zig compiler to use for compilation") if (ZIG_ROOT) + # fails with "undefined symbol: _create_local" (Windows, https://github.com/ziglang/zig/issues/8531?) + # and "unknown filetype for positional input file: '.../binarytrees.lean.o'" (macOS) otherwise + set(ZIG_ARGS "${ZIG_ARGS} -fno-lto") configure_file(zigcc.in zigcc) set(CMAKE_C_COMPILER ${CMAKE_BINARY_DIR}/zigcc) configure_file(zigc++.in zigc++) From 5d1872d9828ef175ad0d6961d4538e2e51f30b91 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 17 Sep 2021 12:13:16 +0200 Subject: [PATCH 09/16] fix: use macOS-compatible `find` invocation --- src/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6700180d510e..836fd32da7c8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -445,7 +445,7 @@ set(LEANC_OPTS "${LEANC_OPTS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} $ if(ZIG_ROOT) # workaround for `--whole-archive` missing from `zig ld` - set(LEANSHARED_LINKER_FLAGS "`find . -regextype posix-extended -regex '.*/(Leanpkg|runtmp|shell).*' -prune -o -regex '.*\.o(bj)?' -print` ${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") + set(LEANSHARED_LINKER_FLAGS "`find . -name 'Leanpkg*' -prune -o -name 'runtmp*' -prune -o -name shell -prune -o -name '*.o' -print -o -name '*.obj' -print` ${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") else() From bbe573dcc4846fdb6a6f19cf0f901c305a5347e7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 20 Sep 2021 18:33:27 +0200 Subject: [PATCH 10/16] fix: temporarily use self-compiled Zig on Windows --- .github/workflows/ci.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7719254d0691..9cdd8d418916 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -54,7 +54,8 @@ jobs: CMAKE_OPTIONS: -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DAUTO_THREAD_FINALIZATION=OFF # for reasons unknown, interactivetests are flaky on Windows CTEST_OPTIONS: --repeat until-pass:2 - zig-url: https://ziglang.org/download/0.8.1/zig-windows-x86_64-0.8.1.zip + # TODO: https://github.com/ziglang/zig/pull/9347 + https://github.com/ziglang/zig/pull/9771 + zig-url: https://pp.ipd.kit.edu/~ullrich/tmp/zig-windows-x86_64-0.9.0-dev.961+aa881c483.zip # complete all jobs fail-fast: false name: ${{ matrix.name }} From 72f90f713ea3ce61d4c5ef875f443ed52db2b411 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 21 Sep 2021 20:25:52 +0200 Subject: [PATCH 11/16] fix: use absolute include paths to placate Zig/Windows --- src/bin/leanc.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/bin/leanc.in b/src/bin/leanc.in index aa12f55fd96e..9c6dc2d3fbe8 100755 --- a/src/bin/leanc.in +++ b/src/bin/leanc.in @@ -1,6 +1,6 @@ #!/usr/bin/env bash # used only for building Lean itself -root=$(dirname $0) +root="$(cd $(dirname $0); pwd)" # ensure absolute path for Zig/Windows ldflags=("-L$root/lib" "-L$root/lib/lean" "${LEANC_GMP:--lgmp}" @LEAN_EXTRA_LINKER_FLAGS@) for arg in "$@"; do # ccache doesn't like linker flags being passed here From 4aeda20b4f261f467bb160250aec950632496a31 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 20 Sep 2021 22:15:09 +0200 Subject: [PATCH 12/16] fix: make thread creation UCRT-compatible --- src/runtime/thread.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/runtime/thread.cpp b/src/runtime/thread.cpp index e742fe1e4184..61f8483946a0 100644 --- a/src/runtime/thread.cpp +++ b/src/runtime/thread.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #ifdef LEAN_WINDOWS #include +#include #else #include #endif @@ -81,15 +82,14 @@ struct lthread::imp { std::function m_proc; HANDLE m_thread; - static DWORD WINAPI _main(void * p) { + static unsigned WINAPI _main(void * p) { thread_main(p); return 0; } imp(runnable const & p) { runnable * f = new std::function(mk_thread_proc(p, get_max_heartbeat())); - m_thread = CreateThread(nullptr, m_thread_stack_size, - _main, f, 0, nullptr); + m_thread = (HANDLE)_beginthreadex(nullptr, m_thread_stack_size, &_main, f, 0, nullptr); if (m_thread == NULL) { throw exception("failed to create thread"); } From 50cb864b0ed1cc299d67f2090ca83536350567cd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 3 Oct 2021 16:47:15 +0200 Subject: [PATCH 13/16] fix: ccache support on Zig/Windows --- src/CMakeLists.txt | 8 ++++---- src/stdlib.make.in | 3 ++- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 836fd32da7c8..023b549d9b4e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -70,10 +70,10 @@ if (ZIG_ROOT) # fails with "undefined symbol: _create_local" (Windows, https://github.com/ziglang/zig/issues/8531?) # and "unknown filetype for positional input file: '.../binarytrees.lean.o'" (macOS) otherwise set(ZIG_ARGS "${ZIG_ARGS} -fno-lto") - configure_file(zigcc.in zigcc) - set(CMAKE_C_COMPILER ${CMAKE_BINARY_DIR}/zigcc) - configure_file(zigc++.in zigc++) - set(CMAKE_CXX_COMPILER ${CMAKE_BINARY_DIR}/zigc++) + configure_file(zigcc.in zigcc.sh) + set(CMAKE_C_COMPILER ${CMAKE_BINARY_DIR}/zigcc.sh) + configure_file(zigc++.in zigc++.sh) + set(CMAKE_CXX_COMPILER ${CMAKE_BINARY_DIR}/zigc++.sh) set(CMAKE_CXX_COMPILER_ID Clang) endif() diff --git a/src/stdlib.make.in b/src/stdlib.make.in index aa5c659c0af0..618f9827143c 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -42,7 +42,8 @@ Lean: Init Std # we specify the precise file names here to avoid rebuilds ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${LIB}/lean/libStd.a ${LIB}/lean/libLean.a ${LIB}/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a @echo "[ ] Building $@" - cd ${CMAKE_BINARY_DIR}; ./leanc.sh -shared -o $@ ${LEANSHARED_LINKER_FLAGS} ${LEANC_OPTS} -v + # cd into directory to make cmdline fit on Windows, do not use ccache because it is confused here on Windows (and irrelevant anyway) + cd ${CMAKE_BINARY_DIR}; LEAN_CC=${CMAKE_C_COMPILER} ./leanc.sh -shared -o $@ ${LEANSHARED_LINKER_FLAGS} ${LEANC_OPTS} leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} From d9f887b4351837bff28a465f95c97862056bee64 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 3 Oct 2021 18:05:23 +0200 Subject: [PATCH 14/16] chore: disable Zig on macOS --- .github/workflows/ci.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9cdd8d418916..cb5ec9b1357b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -46,7 +46,8 @@ jobs: shell: bash -euxo pipefail {0} # Mojave, oldest maintained version as of 2021 CMAKE_OPTIONS: -DCMAKE_OSX_DEPLOYMENT_TARGET=10.14 - zig-url: https://ziglang.org/download/0.8.1/zig-macos-x86_64-0.8.1.tar.xz + # seems to need much more work :( + #zig-url: https://ziglang.org/download/0.8.1/zig-macos-x86_64-0.8.1.tar.xz - name: Windows os: windows-2022 release: true @@ -160,7 +161,7 @@ jobs: - name: Take Off Every Zig run: | cp -r build/zig/ build/stage1/bin - if: matrix.release + if: matrix.zig-url - name: Test Binary without Nix Shell if: matrix.name != 'Windows' shell: bash {0} From 2c3e1a3c18372b964c426a28658d100f8d3d6ce8 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 6 Oct 2021 15:53:28 +0200 Subject: [PATCH 15/16] fix: leanc: complex LEAN_CC --- src/Leanc.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Leanc.lean b/src/Leanc.lean index 9f779335280e..54a9b951e848 100644 --- a/src/Leanc.lean +++ b/src/Leanc.lean @@ -42,9 +42,10 @@ Beware of the licensing consequences since GMP is LGPL." let mut cc := (← IO.getEnv "LEAN_CC").getD "@LEANC_CC@" if cc.startsWith "." then cc := (binDir / cc).toString - - let args := cflags ++ args ++ ldflagsExt ++ ldflags ++ ["-Wno-unused-command-line-argument"] + -- support `LEANC_CC='ccache cc'` + let cc' :: ccArgs ← cc.trim.splitOn | throw <| IO.userError "LEAN_CC is empty" + let args := ccArgs ++ cflags ++ args ++ ldflagsExt ++ ldflags ++ ["-Wno-unused-command-line-argument"] if args.contains "-v" then - IO.eprintln s!"{cc} {" ".intercalate args}" - let child ← IO.Process.spawn { cmd := cc, args := args.toArray } + IO.eprintln s!"{cc'} {" ".intercalate args}" + let child ← IO.Process.spawn { cmd := cc', args := args.toArray } child.wait From 68632828d77a3ad9082219d67139fac4d9cdcef3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 6 Oct 2021 23:35:28 +0200 Subject: [PATCH 16/16] fix: CI: bash < 4.4 --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cb5ec9b1357b..79e0a73aed3b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -122,7 +122,7 @@ jobs: echo "LEAN_VERSION_STRING=$LEAN_VERSION_STRING" >> $GITHUB_ENV fi fi - cmake .. ${{ matrix.CMAKE_OPTIONS }} "${OPTIONS[@]}" + cmake .. ${{ matrix.CMAKE_OPTIONS }} "${OPTIONS[@]-}" make -j4 # de-Nix-ify binaries - name: Patch