diff --git a/.github/functional_tests/lake_lint_args/action.yml b/.github/functional_tests/lake_lint_args/action.yml new file mode 100644 index 0000000..e3734f9 --- /dev/null +++ b/.github/functional_tests/lake_lint_args/action.yml @@ -0,0 +1,135 @@ +name: 'Lake Lint Args' +description: 'Run `lean-action` on with `lint-args` input' +inputs: + toolchain: + description: 'Toolchain to use for the test' + required: true +runs: + using: 'composite' + steps: + # TODO: once `lean-action` supports just setup, use it here + - name: install elan + run: | + set -o pipefail + curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain ${{ inputs.toolchain }} + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + shell: bash + + - name: create lake package with `lake init ${{ inputs.lake-init-arguments }}` + run: | + lake init lintargs .lean + lake update + shell: bash + + - name: create lint script template + run: | + cp lakefile.lean lint_script.template + cat <<'TEMPLATE' >> lint_script.template + @[lint_driver] + script check_lint_args (args) do + let expected := @EXPECTED_ARGS@ + if args == expected then + IO.println s!"✓ Arguments match expected: {expected}" + return 0 + else + IO.eprintln s!"✗ Arguments mismatch!" + IO.eprintln s!" Expected: {expected}" + IO.eprintln s!" Got: {args}" + return 1 + TEMPLATE + shell: bash + + - name: configure script for single driver argument test + run: | + sed 's/@EXPECTED_ARGS@/["test-arg"]/' lint_script.template > lakefile.lean + shell: bash + + - name: "run `lean-action` with single lint-arg passed to driver" + id: lean-action-single + uses: ./ + with: + lint: true + lint-args: "-- test-arg" + use-github-cache: false + + - name: verify `lean-action` outcome success + env: + OUTPUT_NAME: "lean-action-single.outcome" + EXPECTED_VALUE: "success" + ACTUAL_VALUE: ${{ steps.lean-action-single.outcome }} + run: .github/functional_tests/test_helpers/verify_action_output.sh + shell: bash + + - name: verify single argument was passed correctly + env: + OUTPUT_NAME: "lint-status (single arg)" + EXPECTED_VALUE: "SUCCESS" + ACTUAL_VALUE: ${{ steps.lean-action-single.outputs.lint-status }} + run: .github/functional_tests/test_helpers/verify_action_output.sh + shell: bash + + - name: lake clean + run: lake clean + shell: bash + + - name: configure script for multiple driver arguments test + run: | + sed 's/@EXPECTED_ARGS@/["arg1", "arg2", "arg3"]/' lint_script.template > lakefile.lean + shell: bash + + - name: "run `lean-action` with multiple lint args passed to driver" + id: lean-action-multiple + uses: ./ + with: + lint: true + lint-args: "-- arg1 arg2 arg3" + use-github-cache: false + + - name: verify `lean-action-multiple` outcome success + env: + OUTPUT_NAME: "lean-action-multiple.outcome" + EXPECTED_VALUE: "success" + ACTUAL_VALUE: ${{ steps.lean-action-multiple.outcome }} + run: .github/functional_tests/test_helpers/verify_action_output.sh + shell: bash + + - name: verify multiple arguments were passed correctly + env: + OUTPUT_NAME: "lint-status (multiple args)" + EXPECTED_VALUE: "SUCCESS" + ACTUAL_VALUE: ${{ steps.lean-action-multiple.outputs.lint-status }} + run: .github/functional_tests/test_helpers/verify_action_output.sh + shell: bash + + - name: lake clean + run: lake clean + shell: bash + + - name: configure script for empty args test (lake flags) + run: | + sed 's/@EXPECTED_ARGS@/([] : List String)/' lint_script.template > lakefile.lean + shell: bash + + - name: "run `lean-action` with lake flags (not driver args)" + id: lean-action-flags + uses: ./ + with: + lint: true + lint-args: "--quiet" + use-github-cache: false + + - name: verify `lean-action-flags` outcome success + env: + OUTPUT_NAME: "lean-action-flags.outcome" + EXPECTED_VALUE: "success" + ACTUAL_VALUE: ${{ steps.lean-action-flags.outcome }} + run: .github/functional_tests/test_helpers/verify_action_output.sh + shell: bash + + - name: verify lake flag was passed correctly + env: + OUTPUT_NAME: "lint-status (lake flags)" + EXPECTED_VALUE: "SUCCESS" + ACTUAL_VALUE: ${{ steps.lean-action-flags.outputs.lint-status }} + run: .github/functional_tests/test_helpers/verify_action_output.sh + shell: bash diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml index 69a3f92..0c6216d 100644 --- a/.github/workflows/functional_tests.yml +++ b/.github/workflows/functional_tests.yml @@ -118,6 +118,14 @@ jobs: with: toolchain: ${{ env.toolchain }} + lake-lint-args: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v5 + - uses: ./.github/functional_tests/lake_lint_args + with: + toolchain: ${{ env.toolchain }} + lake-check-test-failure: runs-on: ubuntu-latest steps: diff --git a/CHANGELOG.md b/CHANGELOG.md index 4188efe..d73e7f4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## Unreleased +### Added + +- new `lint-args` input to specify arguments to pass to `lake lint` + ## v1.4.0 - 2026-01-15 ### Added diff --git a/README.md b/README.md index 3fb88de..ba5747c 100644 --- a/README.md +++ b/README.md @@ -183,6 +183,11 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu # By default, `lean-action` calls `lake test` with no arguments. test-args: "" + # Lint arguments to pass to `lake lint {lint-args}`. + # For example, `lint-args: "--quiet"` will run `lake lint --quiet`. + # By default, `lean-action` calls `lake lint` with no arguments. + lint-args: "" + # By default, `lean-action` attempts to automatically detect a Mathlib dependency and run `lake exe cache get` accordingly. # Setting `use-mathlib-cache` will override automatic detection and run (or not run) `lake exe cache get`. # Project must be downstream of Mathlib to use the Mathlib cache. diff --git a/action.yml b/action.yml index 6fb754e..95e7212 100644 --- a/action.yml +++ b/action.yml @@ -61,6 +61,13 @@ inputs: By default, `lean-action` calls `lake test` with no arguments. required: false default: "" + lint-args: + description: | + Lint arguments to pass to `lake lint {lint-args}`. + For example, `lint-args: "--quiet"` will run `lake lint --quiet`. + By default, `lean-action` calls `lake lint` with no arguments. + required: false + default: "" use-mathlib-cache: description: | By default, `lean-action` attempts to automatically detect a Mathlib dependency and run `lake exe cache get` accordingly. @@ -225,6 +232,8 @@ runs: - name: test ${{ github.repository }} id: test if: ${{ steps.config.outputs.run-lake-test == 'true'}} + env: + TEST_ARGS: ${{ inputs.test-args }} run: | : Lake Test ${GITHUB_ACTION_PATH}/scripts/lake_test.sh @@ -235,6 +244,8 @@ runs: id: lint # only run linter if the user provided a module to lint if: ${{ steps.config.outputs.run-lake-lint == 'true'}} + env: + LINT_ARGS: ${{ inputs.lint-args }} run: | : Lake Lint ${GITHUB_ACTION_PATH}/scripts/lake_lint.sh diff --git a/scripts/lake_lint.sh b/scripts/lake_lint.sh index c8075f9..a54d35b 100755 --- a/scripts/lake_lint.sh +++ b/scripts/lake_lint.sh @@ -19,4 +19,5 @@ handle_exit() { trap handle_exit EXIT -lake lint +# use eval to ensure lint arguments are expanded +eval "lake lint $LINT_ARGS"