From cb8868da52fa1a6fb6e5d0212c02cc311228e474 Mon Sep 17 00:00:00 2001 From: Aaron Hill Date: Fri, 10 Oct 2025 12:31:14 +0200 Subject: [PATCH 1/6] Test on multiple Lean versions --- .github/workflows/lean_action_ci.yml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 09cd4ca..2c3e3ab 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -8,7 +8,17 @@ on: 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' && '' || '+matrix.lean-version' }}" From 65f8e5c2f24433416ad2f5d4da378dc3db5218bd Mon Sep 17 00:00:00 2001 From: Aaron Hill Date: Fri, 10 Oct 2025 12:33:21 +0200 Subject: [PATCH 2/6] Try to fix build --- .github/workflows/lean_action_ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 2c3e3ab..34abf2a 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -21,4 +21,4 @@ jobs: 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' && '' || '+matrix.lean-version' }}" + build-args: matrix.lean-version == 'from-toolchain' && '' || format('+{}', matrix.lean-version) From eab7d5c35764d79694ca1755f5c7705f7fb823cc Mon Sep 17 00:00:00 2001 From: Aaron Hill Date: Fri, 10 Oct 2025 12:34:18 +0200 Subject: [PATCH 3/6] Only run on prs and pushes to main --- .github/workflows/lean_action_ci.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 34abf2a..95dd841 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -2,6 +2,8 @@ name: Lean Action CI on: push: + branches: + - main pull_request: workflow_dispatch: From dcfec4a186ae6adff951fe04a8787cbc08fad9cd Mon Sep 17 00:00:00 2001 From: Aaron Hill Date: Fri, 10 Oct 2025 12:36:52 +0200 Subject: [PATCH 4/6] Try again --- .github/workflows/lean_action_ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 95dd841..646ca44 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -23,4 +23,4 @@ jobs: 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('+{}', matrix.lean-version) + build-args: ${{ matrix.lean-version 'from-toolchain' && '' || format('+{}', matrix.lean-version) }} From 175d15b88e9fd5ee1dc53b262cd2125b10869444 Mon Sep 17 00:00:00 2001 From: Aaron Hill Date: Fri, 10 Oct 2025 12:37:31 +0200 Subject: [PATCH 5/6] Fix typo --- .github/workflows/lean_action_ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 646ca44..b04effe 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -23,4 +23,4 @@ jobs: 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('+{}', matrix.lean-version) }} + build-args: ${{ matrix.lean-version == 'from-toolchain' && '' || format('+{}', matrix.lean-version) }} From 9ec23bdeeaecaddb368c56094af4a1f2bd32c9d4 Mon Sep 17 00:00:00 2001 From: Aaron Hill Date: Fri, 10 Oct 2025 12:38:20 +0200 Subject: [PATCH 6/6] Fix format --- .github/workflows/lean_action_ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index b04effe..2037e16 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -23,4 +23,4 @@ jobs: 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('+{}', matrix.lean-version) }} + build-args: ${{ matrix.lean-version == 'from-toolchain' && '' || format('+{0}', matrix.lean-version) }}