diff --git a/.github/functional_tests/auto_config_false/action.yml b/.github/functional_tests/auto_config_false/action.yml index 7f8d275..9c302be 100644 --- a/.github/functional_tests/auto_config_false/action.yml +++ b/.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 diff --git a/.github/functional_tests/auto_config_true/action.yml b/.github/functional_tests/auto_config_true/action.yml index 9433010..73fe6c4 100644 --- a/.github/functional_tests/auto_config_true/action.yml +++ b/.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 diff --git a/.github/functional_tests/lake_lint_failure/action.yml b/.github/functional_tests/lake_lint_failure/action.yml new file mode 100644 index 0000000..1a7107c --- /dev/null +++ b/.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 diff --git a/.github/functional_tests/lake_lint_success/action.yml b/.github/functional_tests/lake_lint_success/action.yml new file mode 100644 index 0000000..0682039 --- /dev/null +++ b/.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 diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml index e778189..c1d8738 100644 --- a/.github/workflows/functional_tests.yml +++ b/.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: diff --git a/README.md b/README.md index e9d3452..04eb044 100644 --- a/README.md +++ b/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 ``` diff --git a/action.yml b/action.yml index e468e0a..f66c06e 100644 --- a/action.yml +++ b/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 diff --git a/scripts/config.sh b/scripts/config.sh index 3048ea2..b24ff1b 100755 --- a/scripts/config.sh +++ b/scripts/config.sh @@ -28,11 +28,26 @@ 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" @@ -40,8 +55,19 @@ if [ "$AUTO_CONFIG" = "true" ]; then 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" diff --git a/scripts/lake_lint.sh b/scripts/lake_lint.sh new file mode 100755 index 0000000..e8e79d8 --- /dev/null +++ b/scripts/lake_lint.sh @@ -0,0 +1,21 @@ +#!/bin/bash +set -e + +echo "::group::Lake Lint Output" + +# handle_exit function to handle the exit status of the script +# and set the lint-status output parameter accordingly +handle_exit() { + exit_status=$? + if [ $exit_status -ne 0 ]; then + echo "lint-status=FAILURE" >>"$GITHUB_OUTPUT" + else + echo "lint-status=SUCCESS" >>"$GITHUB_OUTPUT" + fi + echo "::endgroup::" + echo +} + +trap handle_exit EXIT + +lake lint diff --git a/scripts/set_output_parameters.sh b/scripts/set_output_parameters.sh index b3ff7f3..18a9a7e 100755 --- a/scripts/set_output_parameters.sh +++ b/scripts/set_output_parameters.sh @@ -5,7 +5,7 @@ echo "::group::Set Output Parameters" # If the BUILD_STATUS environment variable is not set, # set the `build-status` output parameter to NOT_RUN -# Otherwise, set it to the output of the `lake build` step (the BUILD_STATUS environment variable) +# Otherwise, set it to the output of the `lake build` step, i.e, the BUILD_STATUS environment variable if [ "$BUILD_STATUS" = "" ]; then echo "build-status=NOT_RUN" >>"$GITHUB_OUTPUT" else @@ -14,11 +14,20 @@ fi # If the TEST_STATUS environment variable is not set, # set the `test-status` output parameter to NOT_RUN -# Otherwise, set it to the output of the `lake test` step (the TEST_STATUS environment variable) +# Otherwise, set it to the output of the `lake test` step, i.e., the TEST_STATUS environment variable. if [ "$TEST_STATUS" = "" ]; then echo "test-status=NOT_RUN" >>"$GITHUB_OUTPUT" else echo "test-status=$TEST_STATUS" >>"$GITHUB_OUTPUT" fi +# If the LINT_STATUS environment variable is not set, +# set the `lint-status` output parameter to NOT_RUN +# Otherwise, set it to the output of the `lake lint` step, i.e, the LINT_STATUS environment variable. +if [ "$LINT_STATUS" = "" ]; then + echo "lint-status=NOT_RUN" >>"$GITHUB_OUTPUT" +else + echo "lint-status=$LINT_STATUS" >>"$GITHUB_OUTPUT" +fi + echo "::endgroup::"