refactor: break out functional tests into actions

As we more functional tests are added, the functional_tests.yml file
will become unwieldy. Breaking out the functional tests into actions
gives us more flexibility in how we run the tests
(on PRs, on release, etc.)

.github/functional_tests/lake_init/action.yml

@@ -0,0 +1,31 @@
+name: 'Lake Init Functional Tests'
+description: 'Run `lean action` on Lake package generated by `lake init`'
+inputs:
+  lake-init-arguments:
+      description: 'arguments to pass to `lake init`'
+      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/v1.4.2/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 }}
+        ls
+        pwd
+      shell: bash
+
+    - name: "run `lean-action`" 
+      uses: ./
+      with:
+        test: false
+        use-github-cache: false

.github/functional_tests/lake_test/action.yml

@@ -0,0 +1,33 @@
+name: 'Lake Test Functional Tests'
+description: 'Run `lean-action` with `lake test` and a 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
+        ./elan-init -y --default-toolchain leanprover/lean4:v4.8.0-rc1
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+    - name: create lake package
+      run: |
+        lake init dummytest
+        ls
+    
+    - name: create 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
+
+    - name: "run `lean-action` with `lake test`" 
+      uses: ./
+      with:
+        test: true
+        use-github-cache: false

.github/workflows/functional_tests.yml

@@ -7,51 +7,23 @@ on:
       - "scripts/**"
       - "action.yml"
       - ".github/workflows/functional_tests.yml"
+      - ".github/functional_tests/**"
   workflow_dispatch:
 
 jobs:
   lake-init:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        # run with and without `lake test'
-        lake-test: ["true", "false"]
         # run for standalone package and one which depends on mathlib
-        lake-init-command: ["init standalone", "init mathdep math"]
+        lake-init-arguments: ["init standalone", "init mathdep math"]
     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
-          ./elan-init -y --default-toolchain leanprover/lean4:v4.8.0-rc1
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-
       - uses: actions/checkout@v4
-
-      - name: create standalone project
-        run: |
-          lake ${{ matrix.lake-init-command }}
-          ls
-
-      - name: create dummy test
-        if: ${{ matrix.lake-test == 'true' }}
-        run: |
-          {
-            echo "@[test_runner]"
-            echo "script dummy_test do"
-            echo "  println! \"Running fake tests...\""
-            echo "  println! \"Fake tests passed!\""
-            echo "  return 0" 
-          } >> lakefile.lean
-
-      - name: ls and pwd
-        run: |
-          ls
-          pwd
-
-      - name: "run `lean-action` with on `lake ${{matrix.lake-init-command}}` with test: ${{ matrix.lake-test }}"
-        uses: ./
+      - uses: ./.github/functional_tests/lake_init
         with:
-          test: ${{ matrix.lake-test }}
-          use-github-cache: false
+          lake-init-arguments: ${{ matrix.lake-init-arguments}}
+  lake-test:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/functional_tests/lake_test