CI #154
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: | |
| types: [opened, synchronize, reopened, labeled] | |
| merge_group: | |
| schedule: | |
| - cron: '0 7 * * *' # 8AM CET/11PM PT | |
| 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: | |
| # Should we run only a quick CI? Yes on a pull request without the full-ci label | |
| quick: ${{ steps.set-quick.outputs.quick }} | |
| # 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: Run quick CI? | |
| id: set-quick | |
| env: | |
| quick: ${{ | |
| github.event_name == 'pull_request' && !contains( github.event.pull_request.labels.*.name, 'full-ci') | |
| }} | |
| run: | | |
| echo "quick=${{env.quick}}" >> "$GITHUB_OUTPUT" | |
| - name: Configure build matrix | |
| id: set-matrix | |
| uses: actions/github-script@v7 | |
| with: | |
| script: | | |
| const quick = ${{ steps.set-quick.outputs.quick }}; | |
| console.log(`quick: ${quick}`); | |
| // use large runners outside PRs where available (original repo) | |
| // disabled for now as this mostly just speeds up the test suite which is not a bottleneck | |
| // let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : ""; | |
| let matrix = [ | |
| { | |
| // portable release build: use channel with older glibc (2.27) | |
| "name": "Linux LLVM", | |
| "os": "ubuntu-latest", | |
| "release": false, | |
| "quick": false, | |
| "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": "ubuntu-latest", | |
| "release": true, | |
| "quick": true, | |
| "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": "ubuntu-latest", | |
| "check-stage3": true, | |
| "test-speedcenter": true, | |
| "quick": false, | |
| }, | |
| { | |
| "name": "Linux Debug", | |
| "os": "ubuntu-latest", | |
| "quick": false, | |
| "CMAKE_OPTIONS": "-DCMAKE_BUILD_TYPE=Debug", | |
| // exclude seriously slow tests | |
| "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'" | |
| }, | |
| // TODO: suddenly started failing in CI | |
| /*{ | |
| "name": "Linux fsanitize", | |
| "os": "ubuntu-latest", | |
| "quick": false, | |
| // 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-13", | |
| "release": true, | |
| "quick": false, | |
| "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-13", | |
| "release": true, | |
| "quick": false, | |
| "cross": true, | |
| "cross_target": "aarch64-apple-darwin", | |
| "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": "../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, | |
| "quick": false, | |
| "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, | |
| "quick": false, | |
| "cross": true, | |
| "cross_target": "aarch64-unknown-linux-gnu", | |
| "shell": "nix develop .#oldGlibcAArch -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 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-aarch64-* lean-llvm-x86_64-*" | |
| }, | |
| { | |
| "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", | |
| "cmultilib": true, | |
| "release": true, | |
| "quick": false, | |
| "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", | |
| "wasm": true, | |
| "cmultilib": true, | |
| "release": true, | |
| "quick": false, | |
| "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\"" | |
| } | |
| ]; | |
| console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`) | |
| if (quick) { | |
| return matrix.filter((job) => job.quick) | |
| } else { | |
| return matrix | |
| } | |
| - 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-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 | |
| 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: Checkout | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: true | |
| # 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 }} | |
| - name: Install Nix | |
| uses: cachix/install-nix-action@v18 | |
| with: | |
| install_url: https://releases.nixos.org/nix/nix-2.12.0/install | |
| if: runner.os == 'Linux' && !matrix.cmultilib | |
| - 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: runner.os == 'Windows' | |
| - name: Install Brew Packages | |
| run: | | |
| brew install ccache tree zstd coreutils gmp | |
| if: runner.os == 'macOS' | |
| - name: Setup emsdk | |
| uses: mymindstorm/setup-emsdk@v12 | |
| 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.cmultilib | |
| - 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: runner.os == 'Linux' | |
| - 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: runner.os == 'Linux' | |
| - name: Build | |
| run: | | |
| mkdir build | |
| cd build | |
| ulimit -c unlimited # coredumps | |
| # 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 .. ${{ 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.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@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 --progress --output-junit test-results.xml --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null | |
| if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false' | |
| - 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() && (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false' | |
| - name: Check Test Binary | |
| run: ${{ matrix.binary-check }} tests/compiler/534.lean.out | |
| if: ${{ !matrix.cross && needs.configure.outputs.quick == 'false' }} | |
| - name: Build Stage 2 | |
| run: | | |
| cd build | |
| ulimit -c unlimited # coredumps | |
| make -j4 stage2 | |
| if: matrix.test-speedcenter | |
| - name: Check Stage 3 | |
| run: | | |
| cd build | |
| ulimit -c unlimited # coredumps | |
| make -j4 check-stage3 | |
| if: matrix.test-speedcenter | |
| - 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 | |
| # clean rebuild in case of Makefile changes | |
| make update-stage0 && rm -rf ./stage* && make -j4 | |
| if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false' | |
| - name: CCache stats | |
| run: ccache -s | |
| - name: Show stacktrace for coredumps | |
| if: ${{ failure() && runner.os == 'Linux' }} | |
| run: | | |
| for c in coredumps/*; do | |
| progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")" | |
| echo bt | $GDB/bin/gdb -q $progbin $c || true | |
| done | |
| # has not been used in a long while, would need to be adapted to new | |
| # shared libs | |
| #- name: Upload coredumps | |
| # uses: actions/upload-artifact@v3 | |
| # if: ${{ failure() && runner.os == 'Linux' }} | |
| # 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 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') | |
| 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@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: [configure, build] | |
| if: needs.configure.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.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@v1 | |
| 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 }} |