CI #13
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: CI | |
| on: | |
| push: | |
| branches: | |
| - 'master' | |
| tags: | |
| - '*' | |
| pull_request: | |
| branches: | |
| - master | |
| schedule: | |
| - cron: '0 7 * * *' # 8AM CET/11PM PT | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }}-${{ github.event_name }} | |
| cancel-in-progress: true | |
| jobs: | |
| set-nightly: | |
| runs-on: ubuntu-latest | |
| outputs: | |
| nightly: ${{ steps.set.outputs.nightly }} | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v3 | |
| # don't schedule nightlies on forks | |
| if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' | |
| - name: Set Nightly | |
| if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' | |
| id: set | |
| run: | | |
| if [[ -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 | |
| echo "nightly=$LEAN_VERSION_STRING" >> $GITHUB_OUTPUT | |
| fi | |
| fi | |
| # This job determines if this CI build is for a tagged release. | |
| # It only runs when a tag is pushed to the `leanprover` repository. | |
| # It sets `set-release.outputs.RELEASE_TAG` to the tag, if the tag is "v" followed by a valid semver, | |
| # and sets `set-release.outputs.{LEAN_VERSION_MAJOR,LEAN_VERSION_MINOR,LEAN_VERSION_PATCH,LEAN_SPECIAL_VERSION_DESC}` | |
| # to the semver components parsed via regex. | |
| set-release: | |
| runs-on: ubuntu-latest | |
| outputs: | |
| LEAN_VERSION_MAJOR: ${{ steps.set.outputs.LEAN_VERSION_MAJOR }} | |
| LEAN_VERSION_MINOR: ${{ steps.set.outputs.LEAN_VERSION_MINOR }} | |
| LEAN_VERSION_PATCH: ${{ steps.set.outputs.LEAN_VERSION_PATCH }} | |
| LEAN_SPECIAL_VERSION_DESC: ${{ steps.set.outputs.LEAN_SPECIAL_VERSION_DESC }} | |
| RELEASE_TAG: ${{ steps.set.outputs.RELEASE_TAG }} | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v3 | |
| if: startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4' | |
| - name: Check for official release | |
| if: startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4' | |
| id: set | |
| run: | | |
| TAG_NAME=${GITHUB_REF##*/} | |
| # From https://github.com/fsaintjacques/semver-tool/blob/master/src/semver | |
| NAT='0|[1-9][0-9]*' | |
| ALPHANUM='[0-9]*[A-Za-z-][0-9A-Za-z-]*' | |
| IDENT="$NAT|$ALPHANUM" | |
| FIELD='[0-9A-Za-z-]+' | |
| SEMVER_REGEX="\ | |
| ^[vV]?\ | |
| ($NAT)\\.($NAT)\\.($NAT)\ | |
| (\\-(${IDENT})(\\.(${IDENT}))*)?\ | |
| (\\+${FIELD}(\\.${FIELD})*)?$" | |
| if [[ ${TAG_NAME} =~ ${SEMVER_REGEX} ]]; then | |
| echo "Tag ${TAG_NAME} matches SemVer regex, with groups ${BASH_REMATCH[1]} ${BASH_REMATCH[2]} ${BASH_REMATCH[3]} ${BASH_REMATCH[4]}" | |
| echo "LEAN_VERSION_MAJOR=${BASH_REMATCH[1]}" >> $GITHUB_OUTPUT | |
| echo "LEAN_VERSION_MINOR=${BASH_REMATCH[2]}" >> $GITHUB_OUTPUT | |
| echo "LEAN_VERSION_PATCH=${BASH_REMATCH[3]}" >> $GITHUB_OUTPUT | |
| echo "LEAN_SPECIAL_VERSION_DESC=${BASH_REMATCH[4]##-}" >> $GITHUB_OUTPUT | |
| echo "RELEASE_TAG=$TAG_NAME" >> $GITHUB_OUTPUT | |
| else | |
| echo "Tag ${TAG_NAME} did not match SemVer regex." | |
| fi | |
| build: | |
| needs: [set-nightly, set-release] | |
| if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4' | |
| runs-on: ${{ matrix.os }} | |
| defaults: | |
| run: | |
| shell: ${{ matrix.shell || 'nix-shell --run "bash -euxo pipefail {0}"' }} | |
| strategy: | |
| matrix: | |
| include: | |
| # portable release build: use channel with older glibc (2.27) | |
| - name: Linux LLVM | |
| os: ubuntu-latest | |
| release: false | |
| 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 | |
| # reverse-ffi needs to be updated to link to LLVM libraries | |
| CTEST_OPTIONS: -E 'foreign|leanlaketest_reverse-ffi' | |
| CMAKE_OPTIONS: -DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config | |
| - name: Linux release | |
| 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' | |
| - name: Linux | |
| os: ubuntu-latest | |
| check-stage3: true | |
| test-speedcenter: true | |
| - name: Linux Debug | |
| os: ubuntu-latest | |
| CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Debug | |
| # exclude seriously slow tests | |
| CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest|benchtest' | |
| - name: Linux fsanitize | |
| os: ubuntu-latest | |
| # turn off custom allocator & symbolic functions to make LSAN do its magic | |
| CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF | |
| # exclude seriously slow/problematic tests (laketests crash) | |
| CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest|benchtest' | |
| - name: macOS | |
| os: macos-latest | |
| release: true | |
| shell: bash -euxo pipefail {0} | |
| llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst | |
| prepare-llvm: ../script/prepare-llvm-macos.sh lean-llvm* | |
| binary-check: otool -L | |
| tar: gtar # https://github.com/actions/runner-images/issues/2619 | |
| - name: macOS aarch64 | |
| os: macos-latest | |
| release: true | |
| cross: true | |
| shell: bash -euxo pipefail {0} | |
| CMAKE_OPTIONS: -DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-darwin_aarch64 | |
| llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst | |
| prepare-llvm: EXTRA_FLAGS=--target=aarch64-apple-darwin ../script/prepare-llvm-macos.sh lean-llvm-aarch64-* lean-llvm-x86_64-* | |
| binary-check: otool -L | |
| tar: gtar # https://github.com/actions/runner-images/issues/2619 | |
| - name: Windows | |
| os: windows-2022 | |
| release: true | |
| shell: msys2 {0} | |
| CMAKE_OPTIONS: -G "Unix Makefiles" -DUSE_GMP=OFF | |
| # for reasons unknown, interactivetests are flaky on Windows | |
| CTEST_OPTIONS: --repeat until-pass:2 | |
| llvm-url: https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst | |
| prepare-llvm: ../script/prepare-llvm-mingw.sh lean-llvm* | |
| binary-check: ldd | |
| - name: Linux aarch64 | |
| os: ubuntu-latest | |
| CMAKE_OPTIONS: -DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64 | |
| release: true | |
| cross: true | |
| shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{ localSystem.config = \"aarch64-unknown-linux-gnu\"; }}" --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 https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst | |
| prepare-llvm: EXTRA_FLAGS=--target=aarch64-unknown-linux-gnu ../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-* | |
| - name: Web Assembly | |
| os: ubuntu-latest | |
| # Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build | |
| CMAKE_OPTIONS: -DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX="" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake | |
| wasm: true | |
| cross: true | |
| shell: bash -euxo pipefail {0} | |
| # Just a few selected test because wasm is slow | |
| CTEST_OPTIONS: -R "leantest_1007\.lean|leantest_Format\.lean|leanruntest\_1037.lean|leanruntest_ac_rfl\.lean" | |
| # complete all jobs | |
| fail-fast: false | |
| name: ${{ matrix.name }} | |
| env: | |
| # must be inside workspace | |
| CCACHE_DIR: ${{ github.workspace }}/.ccache | |
| CCACHE_COMPRESS: true | |
| # current cache limit | |
| CCACHE_MAXSIZE: 200M | |
| # squelch error message about missing nixpkgs channel | |
| NIX_BUILD_SHELL: bash | |
| LSAN_OPTIONS: max_leaks=10 | |
| # somehow MinGW clang64 (or cmake?) defaults to `g++` even though it doesn't exist | |
| CXX: c++ | |
| MACOSX_DEPLOYMENT_TARGET: 10.15 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: true | |
| - name: Install Nix | |
| uses: cachix/install-nix-action@v18 | |
| with: | |
| install_url: https://releases.nixos.org/nix/nix-2.12.0/install | |
| if: matrix.os == 'ubuntu-latest' && !matrix.wasm | |
| - name: Install MSYS2 | |
| uses: msys2/setup-msys2@v2 | |
| with: | |
| msystem: clang64 | |
| # `:p` means prefix with appropriate msystem prefix | |
| pacboy: "make python cmake:p clang:p ccache:p gmp:p git zip unzip diffutils binutils tree zstd:p tar" | |
| if: matrix.os == 'windows-2022' | |
| - name: Install Brew Packages | |
| run: | | |
| brew install ccache tree zstd coreutils gmp | |
| if: matrix.os == 'macos-latest' | |
| - name: Setup emsdk | |
| uses: mymindstorm/setup-emsdk@v11 | |
| with: | |
| version: 3.1.44 | |
| actions-cache-folder: emsdk | |
| if: matrix.wasm | |
| - name: Install 32bit c libs | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y gcc-multilib g++-multilib ccache | |
| if: matrix.wasm | |
| - name: Cache | |
| uses: actions/cache@v3 | |
| with: | |
| path: .ccache | |
| key: ${{ matrix.name }}-build-v3-${{ github.sha }} | |
| # fall back to (latest) previous cache | |
| restore-keys: | | |
| ${{ matrix.name }}-build-v3 | |
| - name: Setup | |
| run: | | |
| # open nix-shell once for initial setup | |
| true | |
| if: matrix.os == 'ubuntu-latest' | |
| - name: Set up core dumps | |
| run: | | |
| mkdir -p $PWD/coredumps | |
| # store in current directory, for easy uploading together with binary | |
| echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern | |
| if: matrix.os == 'ubuntu-latest' | |
| - name: Build | |
| run: | | |
| mkdir build | |
| cd build | |
| ulimit -c unlimited # coredumps | |
| OPTIONS=() | |
| if [[ -n '${{ matrix.prepare-llvm }}' ]]; then | |
| wget -q ${{ matrix.llvm-url }} | |
| PREPARE="$(${{ matrix.prepare-llvm }})" | |
| eval "OPTIONS+=($PREPARE)" | |
| fi | |
| if [[ -n '${{ matrix.release }}' && -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then | |
| OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.set-nightly.outputs.nightly }}) | |
| fi | |
| if [[ -n '${{ matrix.release }}' && -n '${{ needs.set-release.outputs.RELEASE_TAG }}' ]]; then | |
| OPTIONS+=(-DLEAN_VERSION_MAJOR=${{ needs.set-release.outputs.LEAN_VERSION_MAJOR }}) | |
| OPTIONS+=(-DLEAN_VERSION_MINOR=${{ needs.set-release.outputs.LEAN_VERSION_MINOR }}) | |
| OPTIONS+=(-DLEAN_VERSION_PATCH=${{ needs.set-release.outputs.LEAN_VERSION_PATCH }}) | |
| OPTIONS+=(-DLEAN_VERSION_IS_RELEASE=1) | |
| OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.set-release.outputs.LEAN_SPECIAL_VERSION_DESC }}) | |
| fi | |
| # contortion to support empty OPTIONS with old macOS bash | |
| cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/.. | |
| make -j4 | |
| make install | |
| - name: Check Binaries | |
| run: ${{ matrix.binary-check }} lean-*/bin/* || true | |
| - name: List Install Tree | |
| run: | | |
| # omit contents of Init/, ... | |
| tree --du -h lean-* | grep -E ' (Init|Lean|Lake|LICENSE|[a-z])' | |
| - name: Pack | |
| run: | | |
| dir=$(echo lean-*) | |
| mkdir pack | |
| # high-compression tar.zst + zip for release, fast tar.zst otherwise | |
| if [[ '${{ startsWith(github.ref, 'refs/tags/') && matrix.release }}' == true || -n '${{ needs.set-nightly.outputs.nightly }}' || -n '${{ needs.set-release.outputs.RELEASE_TAG }}' ]]; then | |
| ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -19 -o pack/$dir.tar.zst | |
| zip -rq pack/$dir.zip $dir | |
| else | |
| ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst | |
| fi | |
| - uses: actions/upload-artifact@v3 | |
| if: matrix.release | |
| with: | |
| name: build-${{ matrix.name }} | |
| path: pack/* | |
| - name: Lean stats | |
| run: | | |
| build/stage1/bin/lean --stats src/Lean.lean | |
| if: ${{ !matrix.cross }} | |
| - name: Test | |
| run: | | |
| cd build/stage1 | |
| ulimit -c unlimited # coredumps | |
| # exclude nonreproducible test | |
| ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null | |
| if: matrix.wasm || !matrix.cross | |
| - name: Check Test Binary | |
| run: ${{ matrix.binary-check }} tests/compiler/534.lean.out | |
| if: ${{ !matrix.cross }} | |
| - name: Build Stage 2 | |
| run: | | |
| cd build | |
| ulimit -c unlimited # coredumps | |
| make -j4 stage2 | |
| if: matrix.build-stage2 || matrix.check-stage3 | |
| - name: Check Stage 3 | |
| run: | | |
| cd build | |
| ulimit -c unlimited # coredumps | |
| make -j4 check-stage3 | |
| if: matrix.check-stage3 | |
| - name: Test Speedcenter Benchmarks | |
| run: | | |
| echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid | |
| export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH | |
| cd tests/bench | |
| nix shell .#temci -c temci exec --config speedcenter.yaml --included_blocks fast --runs 1 | |
| if: matrix.test-speedcenter | |
| - name: Check rebootstrap | |
| run: | | |
| cd build | |
| ulimit -c unlimited # coredumps | |
| make update-stage0 && make -j4 | |
| if: matrix.name == 'Linux' | |
| - name: CCache stats | |
| run: ccache -s | |
| - name: Show stacktrace for coredumps | |
| if: ${{ failure() }} && matrix.os == 'ubuntu-latest' | |
| run: | | |
| for c in coredumps/*; do | |
| progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")" | |
| echo bt | $GDB/bin/gdb -q $progbin $c || true | |
| done | |
| - name: Upload coredumps | |
| uses: actions/upload-artifact@v3 | |
| if: ${{ failure() }} && matrix.os == 'ubuntu-latest' | |
| with: | |
| name: coredumps-${{ matrix.name }} | |
| path: | | |
| ./coredumps | |
| ./build/stage0/bin/lean | |
| ./build/stage0/lib/lean/libleanshared.so | |
| ./build/stage1/bin/lean | |
| ./build/stage1/lib/lean/libleanshared.so | |
| ./build/stage2/bin/lean | |
| ./build/stage2/lib/lean/libleanshared.so | |
| # This job creates releases from tags | |
| # (whether they are "unofficial" releases for experiments, or official releases when the tag is "v" followed by a semver string.) | |
| # We do not attempt to automatically construct a changelog here: | |
| # unofficial releases don't need them, and official release notes will be written by a human. | |
| release: | |
| if: startsWith(github.ref, 'refs/tags/') | |
| runs-on: ubuntu-latest | |
| needs: build | |
| steps: | |
| - uses: actions/download-artifact@v3 | |
| with: | |
| path: artifacts | |
| - name: Release | |
| uses: softprops/action-gh-release@v1 | |
| with: | |
| files: artifacts/*/* | |
| fail_on_unmatched_files: true | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| # This job creates nightly releases during the cron job. | |
| # It is responsible for creating the tag, and automatically generating a changelog. | |
| release-nightly: | |
| needs: [set-nightly, build] | |
| if: needs.set-nightly.outputs.nightly | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v3 | |
| with: | |
| # needed for tagging | |
| fetch-depth: 0 | |
| token: ${{ secrets.PUSH_NIGHTLY_TOKEN }} | |
| - uses: actions/download-artifact@v3 | |
| with: | |
| path: artifacts | |
| - name: Prepare Nightly Release | |
| run: | | |
| git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git | |
| git fetch nightly --tags | |
| git tag ${{ needs.set-nightly.outputs.nightly }} | |
| git push nightly ${{ needs.set-nightly.outputs.nightly }} | |
| last_tag=$(git log HEAD^ --simplify-by-decoration --pretty="format:%d" | grep -o "nightly-[-0-9]*" | head -n 1) | |
| echo -e "*Changes since ${last_tag}:*\n\n" > diff.md | |
| git show $last_tag:RELEASES.md > old.md | |
| #./script/diff_changelogs.py old.md doc/changes.md >> diff.md | |
| diff --changed-group-format='%>' --unchanged-group-format='' old.md RELEASES.md >> diff.md || true | |
| echo -e "\n*Full commit log*\n" >> diff.md | |
| git log --oneline $last_tag..HEAD | sed 's/^/* /' >> diff.md | |
| - name: Release Nightly | |
| uses: softprops/action-gh-release@v1 | |
| with: | |
| body_path: diff.md | |
| prerelease: true | |
| files: artifacts/*/* | |
| fail_on_unmatched_files: true | |
| tag_name: ${{ needs.set-nightly.outputs.nightly }} | |
| repository: ${{ github.repository_owner }}/lean4-nightly | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.PUSH_NIGHTLY_TOKEN }} |