feat: add auto-config and build inputs. (#61)

`auto-config` allows users to specify if `lean-action` should use the Lake workspace to automatically decide which CI features to run. `build` allows users to specify if `lean-action` runs `lake build`. By default, `auto-config: true`. The `test` and `build` (and soon `lint`, see #46) inputs allow users to override the automatically configured behavior or configure `lean-action` when `auto-config: false`. `auto-config: true` is close to the previous default behavior, however there is a difference in the outcome of the `lake test` step. When users set `test: true` manually, `lean-action` must find tests with `lake check-test` and run `lake test` or it will fail (this was the previous behavior). However with `auto-config: true`, if `lake check-test` fails, `lean-action` will not run `lake test` and this won't cause `lean-action` to fail. Closes #60, #53, and #30.
leanprover · Jul 11, 2024 · df9ad20 · df9ad20
1 parent de3e024
commit df9ad20
Show file tree

Hide file tree

Showing 11 changed files with 383 additions and 21 deletions.
diff --git a/.github/functional_tests/auto_config_false/action.yml b/.github/functional_tests/auto_config_false/action.yml
@@ -0,0 +1,85 @@
+name: 'Auto Config False Functional Test'
+description: |
+  Run `lean-action` with `auto-config: false` and no feature inputs.
+  Verify that build and test steps do not run.
+  Run `lean-action` with `auto-config: false` and `lean4checker: true`.
+  Verify that build and tests steps do not run and action succeeds.
+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 leanprover/lean4:v4.8.0-rc1
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create lake package
+      run: |
+        lake init autoconfigtest
+      shell: bash
+
+    - name: "run `lean-action` with `auto-config: false`" 
+      id: lean-action
+      uses: ./
+      with:
+        auto-config: false
+        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 build` not run
+      env:
+        OUTPUT_NAME: "build-status"
+        EXPECTED_VALUE: "NOT_RUN"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.build-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: verify `lake test` not run
+      env:
+        OUTPUT_NAME: "test-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
+      uses: ./
+      with:
+        auto-config: false
+        lean4checker: 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-lean4checker.outcome }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: verify `lake build` not run
+      env:
+        OUTPUT_NAME: "build-status"
+        EXPECTED_VALUE: "NOT_RUN"
+        ACTUAL_VALUE: ${{ steps.lean-action-lean4checker.outputs.build-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: verify `lake test` not run
+      env:
+        OUTPUT_NAME: "test-status"
+        EXPECTED_VALUE: "NOT_RUN"
+        ACTUAL_VALUE: ${{ steps.lean-action-lean4checker.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
@@ -0,0 +1,63 @@
+name: 'Auto Config True Functional Test'
+description: |
+  Run `lean-action` with `auto-config: true` and no feature inputs
+  on a package generated with `lake init` and a dummy test runner added.
+  Verify `lake build` and `lake test` run successfully.
+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 leanprover/lean4:v4.8.0-rc1
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create lake package
+      run: |
+        lake init autoconfigtest
+      shell: bash
+
+    - name: create successful dummy test
+      run: |
+        {
+          echo "@[test_runner]"
+          echo "script dummy_test do"
+          echo "  println! \"Running fake tests...\""
+          echo "  println! \"Fake tests passed!\""
+          echo "  return 0" 
+        } >> lakefile.lean
+      shell: bash
+
+    - name: "run `lean-action` with `lake test`" 
+      id: lean-action
+      uses: ./
+      with:
+        auto-config: 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 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 test` success
+      env:
+        OUTPUT_NAME: "test-status"
+        EXPECTED_VALUE: "SUCCESS"
+        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/lake_check_test_failure/action.yml b/.github/functional_tests/lake_check_test_failure/action.yml
@@ -0,0 +1,52 @@
+name: 'Lake Check Test Failure'
+description: |
+  Run `lean-action` with `test: true` without a test_driver in the Lake workspace.
+  Verify `lean-action` fails and `lake build` and `lake test` are not run.
+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 leanprover/lean4:v4.8.0-rc1
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create lake package
+      run: |
+        lake init dummytest
+      shell: bash
+
+    - name: "run `lean-action` with `test: true`" 
+      id: lean-action
+      uses: ./
+      continue-on-error: true # required so that the action failure does not fail the workflow
+      with:
+        test: 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` not run
+      env:
+        OUTPUT_NAME: "build-status"
+        EXPECTED_VALUE: "NOT_RUN"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.build-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: verify `lake test` not run
+      env:
+        OUTPUT_NAME: "test-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/lake_init_success/action.yml b/.github/functional_tests/lake_init_success/action.yml
@@ -28,7 +28,6 @@ runs:
       id: lean-action
       uses: ./
       with:
-        test: false
         use-github-cache: false
 
     - name: verify `lean-action` outcome success

diff --git a/.github/functional_tests/subdirectory_lake_package/action.yml b/.github/functional_tests/subdirectory_lake_package/action.yml
@@ -29,7 +29,6 @@ runs:
       id: lean-action
       uses: ./
       with:
-        test: false
         use-github-cache: false
         lake-package-directory: "a_subdirectory"
 

diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml
@@ -46,6 +46,18 @@ jobs:
         with:
           toolchain: ${{ env.toolchain }}
 
+  auto-config-true:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/functional_tests/auto_config_true
+
+  auto-config-false:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/functional_tests/auto_config_false
+
   lake-test-success:
     runs-on: ubuntu-latest
     steps:
@@ -62,6 +74,12 @@ jobs:
         with:
           toolchain: ${{ env.toolchain }}
 
+  lake-check-test-failure:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/functional_tests/lake_check_test_failure
+
   subdirectory-lake-package:
     runs-on: ubuntu-latest
     steps:

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -13,6 +13,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - `build-status` and `test-status` output parameters
 - new `lake-package-directory` input to specify the directory to run Lake commands. 
 This input will enable users to use `lean-action` when Lake packages are contained in repository subdirectories.
+- new `auto-config` input to configure `lean-action` to use the Lake workspace to decide which steps to run
 
 ### Changed
 - upgrade elan version to `v3.1.1`

diff --git a/README.md b/README.md
@@ -26,15 +26,95 @@ jobs:
       - uses: leanprover/lean-action@v1-beta
 ```
 
+## Configuring which features `lean-action` runs
+
+Most use cases only require a subset of `lean-action`'s features
+in a specific GitHub workflow.
+Additionally, you may want to break up usage of `lean-action`
+across multiple workflows with different triggers,
+e.g., one workflow for PRs and another workflow scheduled by a cron job.
+
+To support these use cases,
+`lean-action` provides inputs to specify the subset of desired features of `lean-action`.
+
+### Directly specifying a desired feature with specific feature inputs
+Each feature of `lean-action` has a corresponding input which users can set to `true` or `false`.
+Specific feature inputs have the highest precedence
+when `lean-action` determines which features to run.
+When a feature input is set `lean-action` will always try to run the corresponding step.
+If `lean-action` is unable to successfully run the step, `lean-action` will fail.
+
+`lean-action` provides the following feature inputs:
+- `build`
+- `test`
+- `check-reservoir-eligibility`
+- `lean4checker`
+
+### Automatic configuration
+After feature inputs, `lean-action` uses the `auto-config` input
+to determine if it should use the Lake workspace to decide which steps to run automatically.
+When `auto-config: true`, `lean-action` will use the Lake workspace to detect targets
+and run the corresponding Lake command.
+When `auto-config: false`, `lean-action` will only run features specified directly through specific feature inputs.
+Users can combine `auto-config` with specific feature inputs to override the automatic configuration of `lean-action`.
+
+`lean-action` can automatically configure the following features:
+- `build`
+- `test`
+
+### Breaking up `lean-action` across workflows
+Sometimes it is useful to break up usage of `lean-action`
+across multiple workflows with different triggers,
+e.g., one workflow for PRs and another workflow scheduled by a cron job.
+`auto-config: false` allows users to run only a specific subset of features of `lean-action`.
+
+For example, run only `lean4checker` in a cron job workflow:
+
+```yaml
+- name: "run `lean-action` with only `lean4checker: true`"
+  id: lean-action
+  uses: leanprover/lean-action@v1-beta
+  with:
+    auto-config: false
+    lean4checker: true
+```
+
+### Differences between using `auto-config` and feature inputs
+When you specify a feature with a feature input, `lean-action` will fail if it can't complete that step.
+However, if you use `auto-config`,
+`lean-action` will only fail if it detects a target in the Lake workspace and the detected target fails.
+
+For example, if the `lakefile.lean` contains an improperly configured `test_driver` target
+and you configure `lean-action` with `test: true`, `lean-action` will fail.
+However the same improperly configured `test_driver` may not cause a `lean-action` failure with `auto-config: true`,
+because `lean-action` may not detect the `test_driver` in the Lake workspace.
+
+To be certain `lean-action` runs a step, specify the desire feature with a feature input.
+
 ## Customization
 `lean-action` provides optional configuration inputs to customize the behavior for your specific workflow.
 
 ```yaml
 - uses: leanprover/lean-action@v1-beta
   with:
-    # Run lake test.
-    # Allowed values: "true" | "false".
+    
+    # Automatically configure `lean-action` based on the Lake workspace.
+    # When set to "true", `lean-action` will use the Lake workspace to determine
+    # the set of features to run on the repository, such as `lake build` and `lake test`.
+    # Even when set to "true", the user can still override the auto configuration
+    # with the `build` and `test` inputs.
+    # Allowed values: "true" or "false".
     # Default: "true"
+    auto-config: ""
+
+    # Run `lake build`.
+    # Note, this input takes precedence over `auto-config`.
+    # Allowed values: "true" | "false" | "default".
+    build: ""
+
+    # Run `lake test`.
+    # Note, this input takes precedence over `auto-config`.
+    # Allowed values: "true" | "false" | "default".
     test: ""
 
     # Build arguments to pass to `lake build {build-args}`.