test: parameterize functional tests by Lean toolchain

.github/functional_tests/lake_init_failure/action.yml

@@ -1,5 +1,9 @@
 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'
+inputs:
+  toolchain:
+    description: 'Toolchain to use for the test'
+    required: true
 runs: 
   using: 'composite'
   steps:
@@ -8,7 +12,7 @@ runs:
       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
+        ./elan-init -y --default-toolchain ${{ inputs.toolchain }}
         echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
       shell: bash
 

.github/functional_tests/lake_init_success/action.yml

@@ -4,6 +4,9 @@ inputs:
   lake-init-arguments:
       description: 'arguments to pass to `lake init {lake-init-arguments}`'
       required: true
+  toolchain:
+    description: 'Toolchain to use for the test'
+    required: true
 runs: 
   using: 'composite'
   steps:
@@ -12,7 +15,7 @@ runs:
       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
+        ./elan-init -y --default-toolchain ${{ inputs.toolchain }}
         echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
       shell: bash
 

.github/functional_tests/lake_test_failure/action.yml

@@ -1,5 +1,9 @@
 name: 'Lake Test Failure'
 description: 'Run `lean-action` with `lake test` with a failing dummy test_runner'
+inputs:
+  toolchain:
+    description: 'Toolchain to use for the test'
+    required: true
 runs: 
   using: 'composite'
   steps:
@@ -8,7 +12,7 @@ runs:
       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
+        ./elan-init -y --default-toolchain ${{ inputs.toolchain }}
         echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
       shell: bash
 

.github/functional_tests/lake_test_success/action.yml

@@ -1,5 +1,9 @@
 name: 'Lake Test Success'
 description: 'Run `lean-action` with `lake test` and a successful dummy test_runner'
+inputs:
+  toolchain:
+    description: 'Toolchain to use for the test'
+    required: true
 runs: 
   using: 'composite'
   steps:
@@ -8,7 +12,7 @@ runs:
       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
+        ./elan-init -y --default-toolchain ${{ inputs.toolchain }}
         echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
       shell: bash
 

.github/functional_tests/subdirectory_lake_package/action.yml

@@ -2,6 +2,10 @@ name: 'Subdirectory Lake Package Functional Test'
 description: |
   Run `lean-action` with the `lake-package-directory` input
   on Lake package generated by `lake init` in a subdirectory of the repository.
+inputs:
+  toolchain:
+    description: 'Toolchain to use for the test'
+    required: true
 runs: 
   using: 'composite'
   steps:
@@ -10,7 +14,7 @@ runs:
       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
-        ./elan-init -y --default-toolchain leanprover/lean4:v4.8.0-rc1
+        ./elan-init -y --default-toolchain ${{ inputs.toolchain }}
         echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
       shell: bash
 

.github/workflows/functional_tests.yml

@@ -9,6 +9,16 @@ on:
       - ".github/workflows/functional_tests.yml"
       - ".github/functional_tests/**"
   workflow_dispatch:
+    inputs:
+      toolchain:
+        description: 'The Lean toolchain to use when running the tests.'
+        required: false
+        default: 'leanprover/lean4:v4.8.0'
+
+# This environment variable is nessecary in addition ot the workflow_dispatch input
+# because the workflow_dispatch input is not available when the workflow is triggered by a pull request
+env:
+  toolchain: ${{ github.event.inputs.toolchain || 'leanprover/lean4:v4.8.0' }}
 
 jobs:
   lake-init-success:
@@ -26,27 +36,36 @@ jobs:
       - uses: ./.github/functional_tests/lake_init_success
         with:
           lake-init-arguments: ${{ matrix.lake-init-arguments}}
+          toolchain: ${{ env.toolchain }}
 
   lake-init-failure:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
       - uses: ./.github/functional_tests/lake_init_failure
+        with:
+          toolchain: ${{ env.toolchain }}
 
   lake-test-success:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
       - uses: ./.github/functional_tests/lake_test_success
+        with:
+          toolchain: ${{ env.toolchain }}
 
   lake-test-failure:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
       - uses: ./.github/functional_tests/lake_test_failure
+        with:
+          toolchain: ${{ env.toolchain }}
 
   subdirectory-lake-package:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
       - uses: ./.github/functional_tests/subdirectory_lake_package
+        with:
+          toolchain: ${{ env.toolchain }}

CONTRIBUTING.md

@@ -34,16 +34,29 @@ Here are the steps to create a new test:
     - Create a subdirectory named after the test in `.github/functional_tests`.
     - Create an `action.yml` GitHub action file within the directory, which initializes the test and calls `lean-action`.
         - 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).
+        - Parameterize your test by the lean toolchain 
+        (see `.github/functional_tests/lake_init_failure/action.yml` for an example).
+        - If appropriate, you can parameterize your test with additional action inputs for more flexibility
+        (see the `.github/functional_tests/lake_init_success/action.yml` 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 with a specific Lean toolchain
+When triggered by a pull request,
+the `functional_tests.yml` workflow uses the Lean toolchain defined in the `toolchain` environment variable
+at the top of the `functional_tests.yml`  workflow file.
+
+When `functional_tests.yml` is triggered by a manual workflow dispatch,
+users can specify the Lean toolchain as seen in the below screenshot.
+![2024-06-26-09:18:19-screenshot](https://github.com/leanprover/lean-action/assets/21346448/7752b2c1-c986-4544-93ff-9a7864cd155c)
+
 ### Running functional tests locally with `act`
 `lean-action` developers can leverage [act](https://github.com/nektos/act) to run tests locally.
 
 Here are two useful commands:
 - Run all tests locally: `act workflow_dispatch '.github/workflows/functional_tests.yml'`.
 - Run a specific test by running a job within the `functional_tests.yml` workflow:
 `act workflow_dispatch -j {job-name} -W '.github/workflows/functional_tests.yml'`,
-e.g., `act workflow_dispatch -j lake-test -W '.github/workflows/functional_tests.yml'`
+e.g., `act workflow_dispatch -j lake-test -W '.github/workflows/functional_tests.yml'`.