Merge branch 'main' into 34-support-repositories-with-subdirectory-le…

…an-packages

.github/functional_tests/lake_init_failure/action.yml

@@ -0,0 +1,55 @@
+name: 'Lake Init Failure Functional Test'
+description: 'Run `lean-action` on Lake package generated by `lake init` with a modified `lakefile.lean` to cause a build failure'
+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 with `lake init`
+      run: |
+        lake init failingpackage
+      shell: bash
+
+    - name: introduce a syntax error in `lakefile.lean`
+      run: |
+        echo "syntax error" >> lakefile.lean
+      shell: bash
+
+    - name: "run `lean-action`"
+      id: lean-action
+      uses: ./
+      continue-on-error: true # required so that the action does not fail the workflow
+      with:
+        test: false
+        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` failure
+      env:
+        OUTPUT_NAME: "build-status"
+        EXPECTED_VALUE: "FAILURE"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.build-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: verify `lake test` didn't 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

.github/functional_tests/lake_init_success/action.yml

@@ -0,0 +1,53 @@
+name: 'Lake Init Success Functional Test'
+description: 'Run `lean-action` on Lake package generated by `lake init`'
+inputs:
+  lake-init-arguments:
+      description: 'arguments to pass to `lake init {lake-init-arguments}`'
+      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 leanprover/lean4:v4.8.0-rc1
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create lake package with `lake init ${{ inputs.lake-init-arguments }}`
+      run: |
+        lake init ${{ inputs.lake-init-arguments }}
+      shell: bash
+
+    - name: "run `lean-action`"
+      id: lean-action
+      uses: ./
+      with:
+        test: 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` 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` didn't 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

.github/functional_tests/lake_test_failure/action.yml

@@ -0,0 +1,61 @@
+name: 'Lake Test Failure'
+description: 'Run `lean-action` with `lake test` with a failing dummy test_runner'
+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: create failing dummy test
+      run: |
+        {
+          echo "@[test_runner]"
+          echo "script dummy_test do"
+          echo "  println! \"Running fake tests...\""
+          echo "  println! \"Fake tests failed!\""
+          echo "  return 1" 
+        } >> lakefile.lean
+      shell: bash
+
+    - name: "run `lean-action` with `lake test`" 
+      id: lean-action
+      uses: ./
+      continue-on-error: true # required so that the action 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` 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` failure
+      env:
+        OUTPUT_NAME: "test-status"
+        EXPECTED_VALUE: "FAILURE"
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.test-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash

.github/functional_tests/lake_test/action.yml → .github/functional_tests/lake_test_success/action.yml

@@ -1,13 +1,13 @@
-name: 'Lake Test Functional Tests'
-description: 'Run `lean-action` with `lake test` and a dummy test_runner'
+name: 'Lake Test Success'
+description: 'Run `lean-action` with `lake test` and a successful dummy test_runner'
 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/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+        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
@@ -16,8 +16,8 @@ runs:
       run: |
         lake init dummytest
       shell: bash
-    
-    - name: create dummy test
+
+    - name: create successful dummy test
       run: |
         {
           echo "@[test_runner]"
@@ -29,7 +29,24 @@ runs:
       shell: bash
 
     - name: "run `lean-action` with `lake test`" 
+      id: lean-action
       uses: ./
       with:
         test: 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 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

.github/functional_tests/test_helpers/verify_action_output.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+
+# Expects the following environment variables to be set in the calling job step:
+# - OUTPUT_NAME: the name of the output to verify
+# - EXPECTED_VALUE: the expected value of the output
+# - ACTUAL_VALUE: the actual value of the output
+if [ "$ACTUAL_VALUE" != "$EXPECTED_VALUE" ]; then
+    echo "Unexpected value for output $OUTPUT_NAME: $ACTUAL_VALUE (expected: $EXPECTED_VALUE)"
+    exit 1
+fi
+echo "Output $OUTPUT_NAME = $EXPECTED_VALUE verified"

.github/workflows/functional_tests.yml

@@ -11,23 +11,40 @@ on:
   workflow_dispatch:
 
 jobs:
-  lake-init:
+  lake-init-success:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        # run for standalone package and one which depends on mathlib
+        # run `lean-action` on a package generated with `lake init` for:
+        #  - a standalone package
+        #  - a package with a mathlib dependency
+        #  - a package with a `lakefile.toml` file
         # see ./github/functional_tests/lake_init/action.yml for more details on lake-init-arguments
-        lake-init-arguments: ["standalone", "mathdep math"]
+        lake-init-arguments: ["standalone", "mathdep math", "tomltest .toml"]
     steps:
       - uses: actions/checkout@v4
-      - uses: ./.github/functional_tests/lake_init
+      - uses: ./.github/functional_tests/lake_init_success
         with:
           lake-init-arguments: ${{ matrix.lake-init-arguments}}
-  lake-test:
+
+  lake-init-failure:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/functional_tests/lake_init_failure
+
+  lake-test-success:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - uses: ./.github/functional_tests/lake_test
+      - uses: ./.github/functional_tests/lake_test_success
+
+  lake-test-failure:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/functional_tests/lake_test_failure
+
   subdirectory-lake-package:
     runs-on: ubuntu-latest
     steps:

CHANGELOG.md

@@ -8,9 +8,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 - new `use-github-cache` input to specify if `lean-action` should use `actions/cache` to cache the `.lake` folder
+- `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.
 
+### Changed
+- upgrade elan version to `v3.1.1`
+
 ## v1-beta - 2024-05-21
 
 ### Added

CONTRIBUTING.md

@@ -20,6 +20,13 @@ which runs when a PR proposes changes to critical files in the `lean-action` rep
 In the future, we will likely introduce additional entry points for tests,
 such as a more comprehensive test suite for release candidates.
 
+### Verifying `lean-action` outputs with `verify_action_output.sh`
+Functional tests use `verify_action_output.sh` (located in `.github/functional_tests/test_helpers`)
+along with a verification step in the test workflow
+to verify `lean-action` functions as expected in a given test scenario.
+
+See the `lake_test_failure` functional test for an example.
+
 ### Creating a new test
 When introducing new functionality to `lean-action`, consider creating a new functional test.
 Here are the steps to create a new test:
@@ -29,6 +36,7 @@ Here are the steps to create a new test:
         - Write a meaningful description of what use cases your test covers.
         - If appropriate, you can parameterize your test with action inputs for more flexibility (see the `.github/functional_tests/lake_init` directory for an example).
         - For more information on the action syntax, see [creating a composite action](https://docs.github.com/en/actions/creating-actions/creating-a-composite-action).
+    - Create a final step in your test which verifies the outputs of `lean-action` using `verify_action_output.sh`.
 - Create a new job in `.github/workflows/functional_tests.yml` with a call to the newly created action.
 
 ### Running functional tests locally with `act`

README.md

@@ -76,7 +76,30 @@ jobs:
     lake-package-directory: ""
 ```
 
-## Examples
+## Output Parameters
+`lean-action` provides the following output parameters for downstream steps:
+
+- `build-status` 
+  - Values: "SUCCESS" | "FAILURE" | "NOT_RUN"
+- `test-status`
+  - Values: "SUCCESS" | "FAILURE" | "NOT_RUN"
+### Example: Use `test-status` output parameter in downstream step
+
+```yaml
+- name: "run `lean-action` with `lake test`" 
+  id: lean-action
+  uses: leanprover/lean-action@v1-beta
+  continue-on-error: true
+  with:
+    test: true
+
+- name: log `lean-action` `test-status` output
+  env:
+    TEST_STATUS: ${{ steps.lean-action.outputs.test-status }}
+  run: echo "Test status: $TEST_STATUS"
+```
+
+## Additional Examples
 
 ### Lint the `MyModule` module and check package for reservoir eligibility
 
@@ -122,6 +145,7 @@ steps:
       rm import_graph.dot
 ```
 
+
 ## Projects which use `lean-action`
 - [leanprover-community/aesop](https://github.com/leanprover-community/aesop/blob/master/.github/workflows/build.yml#L16)
 - [leanprover-community/import-graph](https://github.com/leanprover-community/import-graph/blob/main/.github/workflows/build.yml#L8)