feat: add lint input to control the lake lint step (#73)

The `lint` input functions similarly to the `test` input, allowing the
user to run `@[lint_driver]` targets with `lean-action`.

Remove the `lint-module` input as users can now use a lint driver to
call the Batteries linting framework.

Closes #46

.github/functional_tests/auto_config_false/action.yml

@@ -55,6 +55,14 @@ runs:
         ACTUAL_VALUE: ${{ steps.lean-action.outputs.test-status }}
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
+
+    - name: verify `lake lint` not run
+      env:
+        OUTPUT_NAME: "lint-status"
+        EXPECTED_VALUE: "NOT_RUN"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.test-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
 
     - name: "run `lean-action` with `auto-config: false` and `lean4checker: true`"
       id: lean-action-lean4checker
@@ -87,3 +95,11 @@ runs:
         ACTUAL_VALUE: ${{ steps.lean-action-lean4checker.outputs.test-status }}
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
+
+    - name: verify `lake lint` not run
+      env:
+        OUTPUT_NAME: "lint-status"
+        EXPECTED_VALUE: "NOT_RUN"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.test-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash

.github/functional_tests/auto_config_true/action.yml

@@ -31,10 +31,21 @@ runs:
           echo "script dummy_test do"
           echo "  println! \"Running fake tests...\""
           echo "  println! \"Fake tests passed!\""
-          echo "  return 0" 
+          echo "  return 0"
         } >> lakefile.lean
       shell: bash
 
+    - name: create successful dummy lint
+      run: |
+        {
+          echo "@[lint_driver]"
+          echo "script dummy_lint do"
+          echo "  println! \"Running fake lints...\""
+          echo "  println! \"Fake lints passed!\""
+          echo "  return 0"
+        } >> lakefile.lean
+      shell: bash
+
     - name: "run `lean-action` with `lake test`" 
       id: lean-action
       uses: ./
@@ -65,3 +76,11 @@ runs:
         ACTUAL_VALUE: ${{ steps.lean-action.outputs.test-status }}
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
+
+    - name: verify `lake lint` success
+      env:
+        OUTPUT_NAME: "lint-status"
+        EXPECTED_VALUE: "SUCCESS"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.lint-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash

.github/functional_tests/lake_lint_failure/action.yml

@@ -0,0 +1,65 @@
+name: 'Lake Lint Failure'
+description: 'Run `lean-action` with `lake lint` with a failing dummy lint_driver'
+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 -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+        ./elan-init -y --default-toolchain ${{ inputs.toolchain }}
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create lake package
+      run: |
+        lake init dummylint
+      shell: bash 
+
+    - name: create failing dummy lint driver
+      run: |
+        {
+          echo "@[lint_driver]"
+          echo "script dummy_lint do"
+          echo "  println! \"Running fake lint...\""
+          echo "  println! \"Fake lint failed!\""
+          echo "  return 1" 
+        } >> lakefile.lean
+      shell: bash
+
+    - name: "run `lean-action` with `lake lint`" 
+      id: lean-action
+      uses: ./
+      continue-on-error: true # required so that the action does not fail the workflow
+      with:
+        lint: true
+        use-github-cache: false
+
+    - name: verify `lean-action` outcome failure
+      env:
+        OUTPUT_NAME: "lean-action outcome"
+        EXPECTED_VALUE: "failure"
+        ACTUAL_VALUE: ${{ steps.lean-action.outcome }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: verify `lake build` success
+      env:
+        OUTPUT_NAME: "build-status"
+        EXPECTED_VALUE: "SUCCESS"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.build-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: verify `lake lint` failure
+      env:
+        OUTPUT_NAME: "lint-status"
+        EXPECTED_VALUE: "FAILURE"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.lint-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash

.github/functional_tests/lake_lint_success/action.yml

@@ -0,0 +1,56 @@
+name: 'Lake Lint Success'
+description: 'Run `lean-action` with `lake lint` and a successful dummy lint_driver'
+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 -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+        ./elan-init -y --default-toolchain ${{ inputs.toolchain }}
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create lake package
+      run: |
+        lake init dummylint
+      shell: bash
+
+    - name: create successful dummy lint
+      run: |
+        {
+          echo "@[lint_driver]"
+          echo "script dummy_lint do"
+          echo "  println! \"Running fake lints...\""
+          echo "  println! \"Fake lints passed!\""
+          echo "  return 0" 
+        } >> lakefile.lean
+      shell: bash
+
+    - name: "run `lean-action` with `lake lint`" 
+      id: lean-action
+      uses: ./
+      with:
+        lint: true
+        use-github-cache: false
+
+    - name: verify `lean-action` outcome success
+      env:
+        OUTPUT_NAME: "lean-action.outcome"
+        EXPECTED_VALUE: "success"
+        ACTUAL_VALUE: ${{ steps.lean-action.outcome }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: verify `lake lint` success
+      env:
+        OUTPUT_NAME: "lint-status"
+        EXPECTED_VALUE: "SUCCESS"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.lint-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash

.github/workflows/functional_tests.yml

@@ -78,6 +78,22 @@ jobs:
         with:
           toolchain: ${{ env.toolchain }}
 
+  lake-lint-success:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/functional_tests/lake_lint_success
+        with:
+          toolchain: ${{ env.toolchain }}
+
+  lake-lint-failure:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/functional_tests/lake_lint_failure
+        with:
+          toolchain: ${{ env.toolchain }}
+
   lake-check-test-failure:
     runs-on: ubuntu-latest
     steps:

README.md

@@ -47,6 +47,7 @@ If `lean-action` is unable to successfully run the step, `lean-action` will fail
 `lean-action` provides the following feature inputs:
 - `build`
 - `test`
+- `lint`
 - `check-reservoir-eligibility`
 - `lean4checker`
 
@@ -61,6 +62,7 @@ Users can combine `auto-config` with specific feature inputs to override the aut
 `lean-action` can automatically configure the following features:
 - `build`
 - `test`
+- `lint`
 
 ### Breaking up `lean-action` across workflows
 Sometimes it is useful to break up usage of `lean-action`
@@ -116,6 +118,11 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
     # Note, this input takes precedence over `auto-config`.
     # Allowed values: "true" | "false" | "default".
     test: ""
+
+    # Run `lake lint`.
+    # Note, this input takes precedence over `auto-config`.
+    # Allowed values: "true" | "false" | "default".
+    lint: ""
 
     # Build arguments to pass to `lake build {build-args}`.
     # For example, `build-args: "--quiet"` will run `lake build --quiet`.
@@ -129,12 +136,6 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
     # Default: "auto"
     use-mathlib-cache: ""
 
-    # Run `lake exe runLinter {lint-module}` on the specified module.
-    # Project must be downstream of Batteries.
-    # Allowed values: name of module to lint.
-    # By default, `lean-action` will not run the linter.
-    lint-module: ""
-
     # Check if the repository is eligible for the Reservoir.
     # Allowed values: "true" | "false".
     # Default: "false"
@@ -184,12 +185,11 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
 
 ## Additional Examples
 
-### Lint the `MyModule` module and check package for reservoir eligibility
+### Check package for reservoir eligibility
 
 ```yaml
 - uses: leanprover/lean-action@v1-beta
   with:
-    lint-module: MyModule
     check-reservoir-eligibility: true
 ```
 

action.yml

@@ -34,6 +34,13 @@ inputs:
       Allowed values: "true" | "false" | "default".
     required: false
     default: "default"
+  lint:
+    description: |
+      Run `lake lint`.
+      Note, this input takes precedence over `auto-config`.
+      Allowed values: "true" | "false" | "default".
+    required: false
+    default: "default"
   build-args:
     description: |
       Build arguments to pass to `lake build {build-args}`.
@@ -49,14 +56,6 @@ inputs:
       Allowed values: "true" | "false" | "auto".
     required: false
     default: "auto"
-  lint-module:
-    description: |
-      Run `lake exe runLinter {lint-module}` on the specified module.
-      Project must be downstream of Batteries.
-      Allowed values: name of module to lint.
-      By default, `lean-action` will not run the linter.
-    required: false
-    default: ""
   check-reservoir-eligibility:
     description: |
       Check if the repository is eligible for the Reservoir.
@@ -96,6 +95,11 @@ outputs:
       The status of the `lake test` step.
       Allowed values: "SUCCESS" | "FAILURE" | "NOT_RUN".
     value: ${{ steps.set-output-parameters.outputs.test-status }}
+  lint-status:
+    description: |
+      The status of the `lake lint` step.
+      Allowed values: "SUCCESS" | "FAILURE" | "NOT_RUN".
+    value: ${{ steps.set-output-parameters.outputs.lint-status }}
 
 runs:
   using: "composite"
@@ -113,6 +117,7 @@ runs:
         AUTO_CONFIG: ${{ inputs.auto-config }}
         BUILD: ${{ inputs.build }}
         TEST: ${{ inputs.test }}
+        LINT: ${{ inputs.lint }}
       run: |
         : Configure Lean Action
         ${{ github.action_path }}/scripts/config.sh
@@ -175,14 +180,12 @@ runs:
       working-directory: ${{ inputs.lake-package-directory }}
 
     - name: lint ${{ github.repository }}
+      id: lint
       # only run linter if the user provided a module to lint
-      if: ${{ inputs.lint-module != '' }}
+      if: ${{ steps.config.outputs.run-lake-lint == 'true'}}
       run: |
-        : Batteries Linter
-        echo "::group::Lint"
-        lake exe runLinter ${{ inputs.lint-module }}
-        echo "::endgroup::"
-        echo
+        : Lake Lint
+        ${{ github.action_path }}/scripts/lake_lint.sh
       shell: bash
       working-directory: ${{ inputs.lake-package-directory }}
 
@@ -214,6 +217,7 @@ runs:
       env:
         BUILD_STATUS: ${{ steps.build.outputs.build-status }}
         TEST_STATUS: ${{ steps.test.outputs.test-status }}
+        LINT_STATUS: ${{ steps.lint.outputs.lint-status }}
       run: |
         : Set Output Parameters
         ${{ github.action_path }}/scripts/set_output_parameters.sh

scripts/config.sh

@@ -28,20 +28,46 @@ if [ "$TEST" = "true" ]; then
     fi
 fi
 
+# If the user specifies `lint: true`
+if [ "$LINT" = "true" ]; then
+    echo "lint: true"
+    # only run `lake lint` if `lake check-lint` returns true
+    if ! lake check-lint; then
+        echo "lake check-lint failed -> exiting with status 1"
+        echo "::error::lake check-lint failed: could not find a lint driver"
+        exit 1
+    else
+        echo "lake check-lint succeeded -> will run lake lint"
+        run_lake_lint="true"
+    fi
+fi
+
 if [ "$AUTO_CONFIG" = "true" ]; then
     # always run `lake build` with `auto-config: true`
     echo "auto-config: true"
     echo "-> will run lake build"
     run_lake_build="true"
+
     # only run `lake test` with `auto-config: true` if `lake check-test` returns true
     if lake check-test; then
         echo "lake check-test succeeded -> will run lake test"
         run_lake_test="true"
     else
         echo "lake check-test failed -> will not run lake test"
     fi
+
+    # only run `lake lint` with `auto-config: true` if `lake check-lint` returns true
+    if lake check-lint; then
+        echo "lake check-lint succeeded -> will run lake lint"
+        run_lake_lint="true"
+    else
+        echo "lake check-test failed -> will not run lake lint"
+    fi
 fi
 
-# Set the `build` and `test` output parameters to be used to determine later steps
-echo "run-lake-build=$run_lake_build" >>"$GITHUB_OUTPUT"
-echo "run-lake-test=$run_lake_test" >>"$GITHUB_OUTPUT"
+# Set the `build`, `test`, and `lint` output parameters to be used to determine later steps
+{
+    echo "run-lake-build=$run_lake_build"
+    echo "run-lake-test=$run_lake_test"
+    echo "run-lake-lint=$run_lake_lint"
+} >>"$GITHUB_OUTPUT"