Skip to content

Commit

Permalink
chore: add nightly testing script to CI (#47)
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Sep 18, 2024
1 parent bb0deee commit fc4c15e
Show file tree
Hide file tree
Showing 2 changed files with 74 additions and 0 deletions.
11 changes: 11 additions & 0 deletions .github/NIGHTLY_FAILURE.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
---
title: Builds failing with Lean nightly
---

The build is failing with the latest Lean nightly as of {{ date | date('YYYY-MM-DD') }}.

Details:

* SubVerso ref: `{{ payload.ref }}`
* SubVerso SHA: `{{ payload.sha }}`
* Release tag: `{{ env.RELEASE_TAG }}`
63 changes: 63 additions & 0 deletions .github/workflows/nightly.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
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
${{ matrix.platform.installer }}
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

0 comments on commit fc4c15e

Please sign in to comment.