feat: add lint-args configuration input

.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

.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:

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

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.

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

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"