CI #1192
This file contains hidden or 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.matrix }} | |
| # secondary build jobs that should not block the CI success/merge queue | |
| matrix-secondary: ${{ steps.set-matrix.outputs.matrix-secondary }} | |
| # 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: Check for custom releases (e.g., not in the main lean repository) | |
| if: startsWith(github.ref, 'refs/tags/') && github.repository != 'leanprover/lean4' | |
| id: set-release-custom | |
| run: | | |
| TAG_NAME="${GITHUB_REF##*/}" | |
| echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT" | |
| - 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 }}" || -n "${{ steps.set-release-custom.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' }}; | |
| const isPr = "${{ github.event_name }}" == "pull_request"; | |
| const isPushToMaster = "${{ github.event_name }}" == "push" && "${{ github.ref_name }}" == "master"; | |
| let matrix = [ | |
| /* TODO: to be updated to new LLVM | |
| { | |
| "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/19.1.2/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" | |
| }, */ | |
| { | |
| // portable release build: use channel with older glibc (2.26) | |
| "name": "Linux release", | |
| "os": "ubuntu-latest", | |
| "release": true, | |
| // Special handling for release jobs. We want: | |
| // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient) | |
| // 2. To skip it in merge queues as it takes longer than the | |
| // Linux lake build and adds little value in the merge queue | |
| // 3. To run it in release (obviously) | |
| // 4. To run it for pushes to master so that pushes to master have a Linux toolchain | |
| // available as an artifact for Grove to use. | |
| "check-level": (isPr || isPushToMaster) ? 0 : 2, | |
| "secondary": isPr, | |
| "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}", | |
| "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/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 Lake", | |
| "os": large ? "nscloud-ubuntu-22.04-amd64-8x16" : "ubuntu-latest", | |
| "check-level": 0, | |
| "test": true, | |
| "check-rebootstrap": level >= 1, | |
| "check-stage3": level >= 2, | |
| // NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest` | |
| "test-speedcenter": large && level >= 2, | |
| "CMAKE_OPTIONS": "-DUSE_LAKE=ON", | |
| }, | |
| { | |
| "name": "Linux Reldebug", | |
| "os": "ubuntu-latest", | |
| "check-level": 2, | |
| "CMAKE_PRESET": "reldebug", | |
| // exclude seriously slow/stackoverflowing tests | |
| "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest|bv_bitblast_stress|3807'" | |
| }, | |
| // 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/19.1.2/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", | |
| // standard GH runner only comes with 7GB so use large runner if possible when running tests | |
| "os": large && !isPr ? "nscloud-macos-sonoma-arm64-6x14" : "macos-14", | |
| "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64", | |
| "release": true, | |
| "shell": "bash -euxo pipefail {0}", | |
| "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/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 | |
| // See "Linux release" for release job levels; Grove is not a concern here | |
| "check-level": isPr ? 0 : 2, | |
| "secondary": isPr, | |
| }, | |
| { | |
| "name": "Windows", | |
| "os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "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/19.1.2/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-4x16", | |
| "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/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst", | |
| "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*" | |
| }, | |
| // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation | |
| //{ | |
| // "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/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config", | |
| // "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)}`); | |
| matrix = matrix.filter((job) => level >= job["check-level"]); | |
| core.setOutput('matrix', matrix.filter((job) => !job["secondary"])); | |
| core.setOutput('matrix-secondary', matrix.filter((job) => job["secondary"])); | |
| build: | |
| if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4' | |
| needs: [configure] | |
| uses: ./.github/workflows/build-template.yml | |
| with: | |
| config: ${{needs.configure.outputs.matrix}} | |
| check-level: ${{ needs.configure.outputs.check-level }} | |
| nightly: ${{ needs.configure.outputs.nightly }} | |
| LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }} | |
| LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }} | |
| LEAN_VERSION_PATCH: ${{ needs.configure.outputs.LEAN_VERSION_PATCH }} | |
| LEAN_SPECIAL_VERSION_DESC: ${{ needs.configure.outputs.LEAN_SPECIAL_VERSION_DESC }} | |
| RELEASE_TAG: ${{ needs.configure.outputs.RELEASE_TAG }} | |
| secrets: inherit | |
| # build jobs that should not be considered by `all-done` below | |
| build-secondary: | |
| needs: [configure] | |
| if: needs.configure.outputs.matrix-secondary != '[]' | |
| uses: ./.github/workflows/build-template.yml | |
| with: | |
| config: ${{needs.configure.outputs.matrix-secondary}} | |
| check-level: ${{ needs.configure.outputs.check-level }} | |
| nightly: ${{ needs.configure.outputs.nightly }} | |
| LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }} | |
| LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }} | |
| LEAN_VERSION_PATCH: ${{ needs.configure.outputs.LEAN_VERSION_PATCH }} | |
| LEAN_SPECIAL_VERSION_DESC: ${{ needs.configure.outputs.LEAN_SPECIAL_VERSION_DESC }} | |
| RELEASE_TAG: ${{ needs.configure.outputs.RELEASE_TAG }} | |
| secrets: inherit | |
| # 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.) | |
| 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@72f2c25fcb47643c292f7107632f7a47c1df5cd8 | |
| 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@72f2c25fcb47643c292f7107632f7a47c1df5cd8 | |
| 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-nightly-testing run nightly_bump_toolchain.yml | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }} |