fix: simp fails to discharge autoParam premises even when it can reduce them to True
#12848
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}`) | |
| let matrix = [ | |
| { | |
| // portable release build: use channel with older glibc (2.27) | |
| "name": "Linux LLVM", | |
| "os": "ubuntu-latest", | |
| "release": false, | |
| "quick": 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, | |
| "quick": 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, | |
| "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'" | |
| }, | |
| { | |
| "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-latest", | |
| "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-latest", | |
| "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-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": "../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-shell --run "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: matrix.os == 'ubuntu-latest' && !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: 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@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: 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 | |
| # 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 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null | |
| if: (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 | |
| make update-stage0 && make -j4 | |
| if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false' | |
| - 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 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 | |
| if: ${{ always() }} | |
| steps: | |
| - if: contains(needs.*.result, 'failure') || contains(needs.*.result, 'cancelled') | |
| 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 }} |