Skip to content

Test on multiple Lean versions #6

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Aaron1011 wants to merge 6 commits into
base: main
Choose a base branch
from
Open

Test on multiple Lean versions #6

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
cb8868d
Test on multiple Lean versions
Aaron1011 Oct 10, 2025
65f8e5c
Try to fix build
Aaron1011 Oct 10, 2025
eab7d5c
Only run on prs and pushes to main
Aaron1011 Oct 10, 2025
dcfec4a
Try again
Aaron1011 Oct 10, 2025
175d15b
Fix typo
Aaron1011 Oct 10, 2025
9ec23bd
Fix format
Aaron1011 Oct 10, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions .github/workflows/lean_action_ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,25 @@ name: Lean Action CI

on:
push:
branches:
- main
pull_request:
workflow_dispatch:

jobs:
build:
runs-on: ubuntu-latest

strategy:
matrix:
# TODO - decide if we want to test more versions
# We run lake with '+version' for each version in this array, with the exception of 'from-toolchain'
lean-version: [4.9.0, nightly, from-toolchain]

steps:
- uses: actions/checkout@v4
- uses: leanprover/lean-action@v1
with:
# For the special 'from-toolchain', we specify an empty string for build args,
# so that lake falls back to our 'lean-toolchain file'
build-args: ${{ matrix.lean-version == 'from-toolchain' && '' || format('+{0}', matrix.lean-version) }}
Loading