feat: alignment of Array.set lemmas with List lemmas (#6365) #25494
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: | |
| merge_group: | |
| schedule: | |
| - cron: '0 7 * * *' # 8AM CET/11PM PT | |
| # for manual re-release of a nightly | |
| workflow_dispatch: | |
| inputs: | |
| action: | |
| description: 'Action' | |
| required: true | |
| default: 'release nightly' | |
| type: choice | |
| options: | |
| - release nightly | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }}-${{ github.event_name }} | |
| cancel-in-progress: true | |
| jobs: | |
| # This job determines various settings for the following CI runs; see the `outputs` for details | |
| configure: | |
| runs-on: ubuntu-latest | |
| outputs: | |
| # 0: PRs without special label | |
| # 1: PRs with `merge-ci` label, merge queue checks, master commits | |
| # 2: PRs with `release-ci` label, releases (incl. nightlies) | |
| check-level: ${{ steps.set-level.outputs.check-level }} | |
| # The build matrix, dynamically generated here | |
| matrix: ${{ steps.set-matrix.outputs.result }} | |
| # Should we make a nightly release? If so, this output contains the lean version string, else it is empty | |
| nightly: ${{ steps.set-nightly.outputs.nightly }} | |
| # Should this be the CI for a tagged release? | |
| # Yes only if a tag is pushed to the `leanprover` repository, and the tag is "v" followed by a valid semver. | |
| # It sets `set-release.outputs.RELEASE_TAG` to the tag | |
| # 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. | |
| LEAN_VERSION_MAJOR: ${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }} | |
| LEAN_VERSION_MINOR: ${{ steps.set-release.outputs.LEAN_VERSION_MINOR }} | |
| LEAN_VERSION_PATCH: ${{ steps.set-release.outputs.LEAN_VERSION_PATCH }} | |
| LEAN_SPECIAL_VERSION_DESC: ${{ steps.set-release.outputs.LEAN_SPECIAL_VERSION_DESC }} | |
| RELEASE_TAG: ${{ steps.set-release.outputs.RELEASE_TAG }} | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| # don't schedule nightlies on forks | |
| if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly' | |
| - name: Set Nightly | |
| if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly' | |
| id: set-nightly | |
| 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 | |
| - name: Check for official release | |
| if: startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4' | |
| id: set-release | |
| 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]}" | |
| echo "LEAN_VERSION_MINOR=${BASH_REMATCH[2]}" | |
| echo "LEAN_VERSION_PATCH=${BASH_REMATCH[3]}" | |
| echo "LEAN_SPECIAL_VERSION_DESC=${BASH_REMATCH[4]##-}" | |
| echo "RELEASE_TAG=$TAG_NAME" | |
| } >> "$GITHUB_OUTPUT" | |
| else | |
| echo "Tag ${TAG_NAME} did not match SemVer regex." | |
| fi | |
| - name: Set check level | |
| id: set-level | |
| # We do not use github.event.pull_request.labels.*.name here because | |
| # re-running a run does not update that list, and we do want to be able to | |
| # rerun the workflow run after setting the `release-ci`/`merge-ci` labels. | |
| run: | | |
| check_level=0 | |
| if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" ]]; then | |
| check_level=2 | |
| elif [[ "${{ github.event_name }}" != "pull_request" ]]; then | |
| check_level=1 | |
| else | |
| labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels')" | |
| if echo "$labels" | grep -q "release-ci"; then | |
| check_level=2 | |
| elif echo "$labels" | grep -q "merge-ci"; then | |
| check_level=1 | |
| fi | |
| fi | |
| echo "check-level=$check_level" >> "$GITHUB_OUTPUT" | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| - name: Configure build matrix | |
| id: set-matrix | |
| uses: actions/github-script@v7 | |
| with: | |
| script: | | |
| const level = ${{ steps.set-level.outputs.check-level }}; | |
| console.log(`level: ${level}`); | |
| // use large runners where available (original repo) | |
| let large = ${{ github.repository == 'leanprover/lean4' }}; | |
| let matrix = [ | |
| { | |
| // portable release build: use channel with older glibc (2.27) | |
| "name": "Linux LLVM", | |
| "os": "ubuntu-latest", | |
| "release": false, | |
| "check-level": 2, | |
| "shell": "nix develop .#oldGlibc -c 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": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest", | |
| "release": true, | |
| "check-level": 0, | |
| "shell": "nix develop .#oldGlibc -c 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": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest", | |
| "check-stage3": level >= 2, | |
| "test-speedcenter": level >= 2, | |
| "check-level": 1, | |
| }, | |
| { | |
| "name": "Linux Debug", | |
| "os": "ubuntu-latest", | |
| "check-level": 2, | |
| "CMAKE_PRESET": "debug", | |
| // exclude seriously slow tests | |
| "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest|bv_bitblast_stress'" | |
| }, | |
| // TODO: suddenly started failing in CI | |
| /*{ | |
| "name": "Linux fsanitize", | |
| "os": "ubuntu-latest", | |
| "check-level": 2, | |
| // turn off custom allocator & symbolic functions to make LSAN do its magic | |
| "CMAKE_PRESET": "sanitize", | |
| // exclude seriously slow/problematic tests (laketests crash) | |
| "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'" | |
| },*/ | |
| { | |
| "name": "macOS", | |
| "os": "macos-13", | |
| "release": true, | |
| "check-level": 2, | |
| "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-14", | |
| "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64", | |
| "release": true, | |
| "check-level": 0, | |
| "shell": "bash -euxo pipefail {0}", | |
| "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-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": "Windows", | |
| "os": "windows-2022", | |
| "release": true, | |
| "check-level": 2, | |
| "shell": "msys2 {0}", | |
| "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/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": "nscloud-ubuntu-22.04-arm64-4x8", | |
| "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64", | |
| "release": true, | |
| "check-level": 2, | |
| "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}", | |
| "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst", | |
| "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*" | |
| }, | |
| { | |
| "name": "Linux 32bit", | |
| "os": "ubuntu-latest", | |
| // Use 32bit on stage0 and stage1 to keep oleans compatible | |
| "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/", | |
| "cmultilib": true, | |
| "release": true, | |
| "check-level": 2, | |
| "cross": true, | |
| "shell": "bash -euxo pipefail {0}" | |
| }, | |
| { | |
| "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 -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32 -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/", | |
| "wasm": true, | |
| "cmultilib": true, | |
| "release": true, | |
| "check-level": 2, | |
| "cross": true, | |
| "shell": "bash -euxo pipefail {0}", | |
| // Just a few selected tests because wasm is slow | |
| "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\"" | |
| } | |
| ]; | |
| console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`) | |
| return matrix.filter((job) => level >= job["check-level"]) | |
| build: | |
| needs: [configure] | |
| if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4' | |
| strategy: | |
| matrix: | |
| include: ${{fromJson(needs.configure.outputs.matrix)}} | |
| # complete all jobs | |
| fail-fast: false | |
| runs-on: ${{ matrix.os }} | |
| defaults: | |
| run: | |
| shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }} | |
| 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: Install Nix | |
| uses: DeterminateSystems/nix-installer-action@main | |
| if: runner.os == 'Linux' && !matrix.cmultilib | |
| - name: Install MSYS2 | |
| uses: msys2/setup-msys2@v2 | |
| with: | |
| msystem: clang64 | |
| # `:` means do not prefix with msystem | |
| pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:" | |
| if: runner.os == 'Windows' | |
| - name: Install Brew Packages | |
| run: | | |
| brew install ccache tree zstd coreutils gmp libuv | |
| if: runner.os == 'macOS' | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| # the default is to use a virtual merge commit between the PR and master: just use the PR | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| # Do check out some CI-relevant files from virtual merge commit to accommodate CI changes on | |
| # master (as the workflow files themselves are always taken from the merge) | |
| # (needs to be after "Install *" to use the right shell) | |
| - name: CI Merge Checkout | |
| run: | | |
| git fetch --depth=1 origin ${{ github.sha }} | |
| git checkout FETCH_HEAD flake.nix flake.lock | |
| if: github.event_name == 'pull_request' | |
| # (needs to be after "Checkout" so files don't get overridden) | |
| - name: Setup emsdk | |
| uses: mymindstorm/setup-emsdk@v14 | |
| with: | |
| version: 3.1.44 | |
| actions-cache-folder: emsdk | |
| if: matrix.wasm | |
| - name: Install 32bit c libs | |
| run: | | |
| sudo dpkg --add-architecture i386 | |
| sudo apt-get update | |
| sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 | |
| if: matrix.cmultilib | |
| - name: Cache | |
| uses: actions/cache@v4 | |
| with: | |
| path: .ccache | |
| key: ${{ matrix.name }}-build-v3-${{ github.event.pull_request.head.sha }} | |
| # fall back to (latest) previous cache | |
| restore-keys: | | |
| ${{ matrix.name }}-build-v3 | |
| save-always: true | |
| # open nix-shell once for initial setup | |
| - name: Setup | |
| run: | | |
| ccache --zero-stats | |
| if: runner.os == 'Linux' | |
| - name: Set up NPROC | |
| run: | | |
| echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV | |
| - name: Build | |
| run: | | |
| mkdir build | |
| cd build | |
| # arguments passed to `cmake` | |
| # this also enables githash embedding into stage 1 library | |
| OPTIONS=(-DCHECK_OLEAN_VERSION=ON) | |
| OPTIONS+=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true) | |
| if [[ -n '${{ matrix.cross_target }}' ]]; then | |
| # used by `prepare-llvm` | |
| export EXTRA_FLAGS=--target=${{ matrix.cross_target }} | |
| OPTIONS+=(-DLEAN_PLATFORM_TARGET=${{ matrix.cross_target }}) | |
| fi | |
| 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.configure.outputs.nightly }}' ]]; then | |
| OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.configure.outputs.nightly }}) | |
| fi | |
| if [[ -n '${{ matrix.release }}' && -n '${{ needs.configure.outputs.RELEASE_TAG }}' ]]; then | |
| OPTIONS+=(-DLEAN_VERSION_MAJOR=${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}) | |
| OPTIONS+=(-DLEAN_VERSION_MINOR=${{ needs.configure.outputs.LEAN_VERSION_MINOR }}) | |
| OPTIONS+=(-DLEAN_VERSION_PATCH=${{ needs.configure.outputs.LEAN_VERSION_PATCH }}) | |
| OPTIONS+=(-DLEAN_VERSION_IS_RELEASE=1) | |
| OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.configure.outputs.LEAN_SPECIAL_VERSION_DESC }}) | |
| fi | |
| # contortion to support empty OPTIONS with old macOS bash | |
| cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/.. | |
| time make -j$NPROC | |
| - name: Install | |
| run: | | |
| make -C build install | |
| - name: Check Binaries | |
| run: ${{ matrix.binary-check }} lean-*/bin/* || true | |
| - name: Count binary symbols | |
| run: | | |
| for f in lean-*/bin/*; do | |
| echo "$f: $(nm $f | grep " T " | wc -l) exported symbols" | |
| done | |
| if: matrix.name == 'Windows' | |
| - 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.configure.outputs.nightly }}' || -n '${{ needs.configure.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@v4 | |
| 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 | |
| id: test | |
| run: | | |
| time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }} | |
| if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.check-level >= 1 | |
| - name: Test Summary | |
| uses: test-summary/action@v2 | |
| with: | |
| paths: build/stage1/test-results.xml | |
| # prefix `if` above with `always` so it's run even if tests failed | |
| if: always() && steps.test.conclusion != 'skipped' | |
| - name: Check Test Binary | |
| run: ${{ matrix.binary-check }} tests/compiler/534.lean.out | |
| if: (!matrix.cross) && steps.test.conclusion != 'skipped' | |
| - name: Build Stage 2 | |
| run: | | |
| make -C build -j$NPROC stage2 | |
| if: matrix.test-speedcenter | |
| - name: Check Stage 3 | |
| run: | | |
| make -C build -j$NPROC check-stage3 | |
| if: matrix.test-speedcenter | |
| - name: Test Speedcenter Benchmarks | |
| run: | | |
| # Necessary for some timing metrics but does not work on Namespace runners | |
| # and we just want to test that the benchmarks run at all here | |
| #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: | | |
| # clean rebuild in case of Makefile changes | |
| make -C build update-stage0 && rm -rf build/stage* && make -C build -j$NPROC | |
| if: matrix.name == 'Linux' && needs.configure.outputs.check-level >= 1 | |
| - name: CCache stats | |
| run: ccache -s | |
| # This job collects results from all the matrix jobs | |
| # This can be made the "required" job, instead of listing each | |
| # matrix job separately | |
| all-done: | |
| name: Build matrix complete | |
| runs-on: ubuntu-latest | |
| needs: build | |
| # mark as merely cancelled not failed if builds are cancelled | |
| if: ${{ !cancelled() }} | |
| steps: | |
| - if: ${{ contains(needs.*.result, 'failure') && github.repository == 'leanprover/lean4' && github.ref_name == 'master' }} | |
| uses: zulip/github-actions-zulip/send-message@v1 | |
| with: | |
| api-key: ${{ secrets.ZULIP_BOT_KEY }} | |
| email: "[email protected]" | |
| organization-url: "https://lean-fro.zulipchat.com" | |
| to: "infrastructure" | |
| topic: "Github actions" | |
| type: "stream" | |
| content: | | |
| A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}). | |
| - if: contains(needs.*.result, 'failure') | |
| uses: actions/github-script@v7 | |
| with: | |
| script: | | |
| core.setFailed('Some jobs failed') | |
| # 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@v4 | |
| with: | |
| path: artifacts | |
| - name: Release | |
| uses: softprops/action-gh-release@v2 | |
| with: | |
| files: artifacts/*/* | |
| fail_on_unmatched_files: true | |
| prerelease: ${{ !startsWith(github.ref, 'refs/tags/v') || contains(github.ref, '-rc') }} | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Update release.lean-lang.org | |
| run: | | |
| gh workflow -R leanprover/release-index run update-index.yml | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_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: [configure, build] | |
| if: needs.configure.outputs.nightly | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| with: | |
| # needed for tagging | |
| fetch-depth: 0 | |
| token: ${{ secrets.PUSH_NIGHTLY_TOKEN }} | |
| - uses: actions/download-artifact@v4 | |
| 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.configure.outputs.nightly }}" | |
| git push nightly "${{ needs.configure.outputs.nightly }}" | |
| git push -f origin refs/tags/${{ needs.configure.outputs.nightly }}:refs/heads/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@v2 | |
| with: | |
| body_path: diff.md | |
| prerelease: true | |
| files: artifacts/*/* | |
| fail_on_unmatched_files: true | |
| tag_name: ${{ needs.configure.outputs.nightly }} | |
| repository: ${{ github.repository_owner }}/lean4-nightly | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.PUSH_NIGHTLY_TOKEN }} | |
| - name: Update release.lean-lang.org | |
| run: | | |
| gh workflow -R leanprover/release-index run update-index.yml | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }} | |
| - name: Update toolchain on mathlib4's nightly-testing branch | |
| run: | | |
| gh workflow -R leanprover-community/mathlib4 run nightly_bump_toolchain.yml | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }} |