Skip to content

Test with Lean nightly #2

Test with Lean nightly

Test with Lean nightly #2

Workflow file for this run

name: Test with Lean nightly
on:
workflow_dispatch:
schedule:
- cron: '0 0 * * *' # Run every day at midnight
jobs:
update-toolchain:
runs-on: ubuntu-latest
steps:
- name: Install elan
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: Check out code
uses: actions/checkout@v4
- name: Get latest release tag from leanprover/lean4-nightly
id: get-latest-release
run: |
RELEASE_TAG="$(curl -s "https://api.github.com/repos/leanprover/lean4-nightly/releases" | jq -r '.[0].tag_name')"
echo "RELEASE_TAG=$RELEASE_TAG" >> "${GITHUB_ENV}"
- name: Select Lean version ${{env.RELEASE_TAG}}
run: |
echo "leanprover/lean4:${RELEASE_TAG}" > lean-toolchain
- name: Build the project
continue-on-error: true
id: build
run: |
lake build
- name: Configure demo/test subproject
if: always() && steps.build.outcome == 'success'
continue-on-error: true
id: config-test
run: |
pushd demo
lake update
lake build :examples
popd
- name: Run tests
if: always() && steps.config-test.outcome == 'success'
continue-on-error: true
id: test
run: |
lake exe subverso-tests
- name: Create/update issue on failure
if: always() && (steps.build.outcome == 'failure') || (steps.config-test.outcome == 'failure') || (steps.test.outcome == 'failure')
uses: JasonEtco/create-an-issue@v2
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
with:
update_existing: true
search_existing: open
filename: .github/NIGHTLY_FAILURE.md