Skip to content

Commit

Permalink
chore: upgrade functional test version to 4.13.0 (#107)
Browse files Browse the repository at this point in the history
  • Loading branch information
austinletson authored Nov 20, 2024
1 parent b471931 commit 657d852
Show file tree
Hide file tree
Showing 7 changed files with 11 additions and 10 deletions.
7 changes: 4 additions & 3 deletions .github/functional_tests/auto_config_false/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ runs:

- name: create lake package
run: |
lake init autoconfigtest
lake init autoconfigtest .lean
lake update
shell: bash

Expand Down Expand Up @@ -69,6 +69,7 @@ runs:
uses: ./
with:
auto-config: false
build: true
lean4checker: true
use-github-cache: false

Expand All @@ -80,10 +81,10 @@ runs:
run: .github/functional_tests/test_helpers/verify_action_output.sh
shell: bash

- name: verify `lake build` not run
- name: verify `lake build` ran
env:
OUTPUT_NAME: "build-status"
EXPECTED_VALUE: ""
EXPECTED_VALUE: "SUCCESS"
ACTUAL_VALUE: ${{ steps.lean-action-lean4checker.outputs.build-status }}
run: .github/functional_tests/test_helpers/verify_action_output.sh
shell: bash
Expand Down
2 changes: 1 addition & 1 deletion .github/functional_tests/auto_config_true/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ runs:

- name: create lake package
run: |
lake init autoconfigtest
lake init autoconfigtest .lean
lake update
shell: bash

Expand Down
2 changes: 1 addition & 1 deletion .github/functional_tests/lake_lint_failure/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ runs:

- name: create lake package
run: |
lake init dummylint
lake init dummylint .lean
lake update
shell: bash

Expand Down
2 changes: 1 addition & 1 deletion .github/functional_tests/lake_lint_success/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ runs:

- name: create lake package
run: |
lake init dummylint
lake init dummylint .lean
lake update
shell: bash

Expand Down
2 changes: 1 addition & 1 deletion .github/functional_tests/lake_test_failure/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ runs:

- name: create lake package
run: |
lake init dummytest
lake init dummytest .lean
lake update
shell: bash

Expand Down
2 changes: 1 addition & 1 deletion .github/functional_tests/lake_test_success/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ runs:

- name: create lake package
run: |
lake init dummytest
lake init dummytest .lean
lake update
shell: bash

Expand Down
4 changes: 2 additions & 2 deletions .github/workflows/functional_tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -13,12 +13,12 @@ on:
toolchain:
description: "The Lean toolchain to use when running the tests."
required: false
default: "leanprover/lean4:v4.12.0"
default: "leanprover/lean4:v4.13.0"

# This environment variable is nessecary in addition ot the workflow_dispatch input
# because the workflow_dispatch input is not available when the workflow is triggered by a pull request
env:
toolchain: ${{ github.event.inputs.toolchain || 'leanprover/lean4:v4.12.0' }}
toolchain: ${{ github.event.inputs.toolchain || 'leanprover/lean4:v4.13.0' }}

jobs:
lake-init-success:
Expand Down

0 comments on commit 657d852

Please sign in to comment.