feat: add auto-config and build inputs.

`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` should run `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.
leanprover · Jun 14, 2024 · 7698a08 · 7698a08
1 parent 52906d4
commit 7698a08
Show file tree

Hide file tree

Showing 10 changed files with 365 additions and 18 deletions.
diff --git a/.github/functional_tests/auto_config_false/action.yml b/.github/functional_tests/auto_config_false/action.yml
@@ -0,0 +1,97 @@
+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: 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 `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
@@ -25,7 +25,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
@@ -25,7 +25,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
@@ -33,6 +33,18 @@ jobs:
       - uses: actions/checkout@v4
       - uses: ./.github/functional_tests/lake_init_failure
 
+  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:
@@ -45,6 +57,12 @@ jobs:
       - uses: actions/checkout@v4
       - uses: ./.github/functional_tests/lake_test_failure
 
+  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/README.md b/README.md
@@ -26,6 +26,60 @@ jobs:
       - uses: leanprover/lean-action@v1-beta
 ```
 
+## Selecting which features of `lean-action`
+
+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 schedule 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`.
+These inputs are the first place `lean-action` looks.
+If one of these is set `lean-action` will try to run the corresponding step.
+If `lean-action` is unable to successfully run the step, `lean-action` will fail.
+
+### Automatic configuration
+After checking the feature inputs `lean-action` uses the `auto-config` input
+to determine if it should use the Lake workspace to decide which features to use 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 through the feature inputs.
+Users can combine `auto-config` with specific feature inputs to override the automatic configuration of `lean-action`.
+
+### 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 schedule by a cron job.
+`auto-config: false` allows users to run 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: ./
+  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` uses a feature, specify the desire feature with a feature input.
+
 ## Usage
 
 ```yaml