test: add functional test for lean4checker in subdirectory (#138)

Co-authored-by: Austin Letson <austin.letson@axiomatic-ai.com>

Author: austinletson

.github/functional_tests/subdirectory_lake_package_lean_checker/action.yml

@@ -0,0 +1,52 @@
+name: 'Subdirectory Lake Package using lean4checker 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.
+
+  Also run lean4checker
+inputs:
+  toolchain:
+    description: 'Toolchain to use for the test'
+    required: true
+runs: 
+  using: 'composite'
+  steps:
+    # TODO: once `lean-action` supports just setup, use it here
+    - name: install elan
+      run: |
+        set -o pipefail
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain ${{ inputs.toolchain }}
+        echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      shell: bash
+
+    - name: create Lake package in a_subdirectory
+      run: |
+        mkdir a_subdirectory
+        cd a_subdirectory
+        lake init subdirpackage
+        lake update
+      shell: bash
+
+    - name: "run `lean-action`" 
+      id: lean-action
+      uses: ./
+      with:
+        use-github-cache: false
+        lake-package-directory: "a_subdirectory"
+        lean4checker: true
+
+    - 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: ""
+        ACTUAL_VALUE: ${{ steps.lean-action.outputs.test-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash

.github/workflows/functional_tests.yml

@@ -133,6 +133,14 @@ jobs:
       - uses: ./.github/functional_tests/subdirectory_lake_package
         with:
           toolchain: ${{ env.toolchain }}
+  
+  subdirectory-lake-package-lean-checker:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+      - uses: ./.github/functional_tests/subdirectory_lake_package_lean_checker
+        with:
+          toolchain: ${{ env.toolchain }}
 
   reinstall-transient-toolchain:
     runs-on: ubuntu-latest