fix: Set test-args input correctly and improve functional tests

.github/functional_tests/lake_build_args/action.yml

@@ -1,10 +1,10 @@
 name: 'Lake Build Args'
-description: 'Run `lean-action` on with `build-args` input'
+description: 'Run `lean-action` with `build-args` input and verify args are passed through'
 inputs:
   toolchain:
     description: 'Toolchain to use for the test'
     required: true
-runs: 
+runs:
   using: 'composite'
   steps:
     # TODO: once `lean-action` supports just setup, use it here
@@ -15,32 +15,69 @@ runs:
         echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
       shell: bash
 
-    - name: create lake package with `lake init ${{ inputs.lake-init-arguments }}`
+    - name: create lake package with a warning-producing target
       run: |
         lake init buildargs .lean
         lake update
+        {
+          echo ""
+          echo "@[default_target]"
+          echo "lean_exe WarningExe"
+        } >> lakefile.lean
+        {
+          echo "#eval (do"
+          echo "  let buildArgs <- IO.getEnv \"BUILD_ARGS\""
+          echo "  let value := buildArgs.get!"
+          echo "  IO.FS.writeFile \"build_args_output.txt\" value : IO Unit)"
+          echo ""
+          echo "def incomplete : Nat := sorry"
+          echo "def main : IO Unit := pure ()"
+        } > WarningExe.lean
       shell: bash
 
-    - name: "run `lean-action` with build-args"
-      id: lean-action
+    - name: "run `lean-action` without build-args (should succeed despite warning)"
+      id: lean-action-no-args
       uses: ./
       with:
-        build-args: "--wfail"
         use-github-cache: false
 
-    - name: verify `lean-action` outcome success
+    - name: verify `lean-action` outcome success without build-args
       env:
-        OUTPUT_NAME: "lean-action.outcome"
+        OUTPUT_NAME: "lean-action-no-args.outcome"
         EXPECTED_VALUE: "success"
-        ACTUAL_VALUE: ${{ steps.lean-action.outcome }}
+        ACTUAL_VALUE: ${{ steps.lean-action-no-args.outcome }}
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
 
-    - name: verify `lake build` success
+    - name: verify `lake build` success without build-args
       env:
         OUTPUT_NAME: "build-status"
         EXPECTED_VALUE: "SUCCESS"
-        ACTUAL_VALUE: ${{ steps.lean-action.outputs.build-status }}
+        ACTUAL_VALUE: ${{ steps.lean-action-no-args.outputs.build-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: "run `lean-action` with build-args `--wfail` (should fail due to sorry warning)"
+      id: lean-action-wfail
+      uses: ./
+      continue-on-error: true
+      with:
+        build-args: "--wfail"
+        use-github-cache: false
+
+    - name: verify `lean-action` outcome failure with --wfail
+      env:
+        OUTPUT_NAME: "lean-action-wfail.outcome"
+        EXPECTED_VALUE: "failure"
+        ACTUAL_VALUE: ${{ steps.lean-action-wfail.outcome }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash
+
+    - name: verify `lake build` failure with --wfail
+      env:
+        OUTPUT_NAME: "build-status"
+        EXPECTED_VALUE: "FAILURE"
+        ACTUAL_VALUE: ${{ steps.lean-action-wfail.outputs.build-status }}
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
 
@@ -52,9 +89,9 @@ runs:
       id: lean-action-multiple-build-args
       uses: ./
       with:
-        build-args: "--log-level=warning --fail-level=warning"
+        build-args: "--log-level=warning --fail-level=error"
         use-github-cache: false
-    
+
     - name: verify `lean-action-multiple-build-args` outcome success
       env:
         OUTPUT_NAME: "lean-action-multiple-build-args.outcome"
@@ -63,10 +100,12 @@ runs:
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
 
-    - name: verify `lake build` success
+    - name: verify multiple build-args output
       env:
-        OUTPUT_NAME: "build-status"
-        EXPECTED_VALUE: "SUCCESS"
-        ACTUAL_VALUE: ${{ steps.lean-action-multiple-build-args.outputs.build-status }}
-      run: .github/functional_tests/test_helpers/verify_action_output.sh
+        OUTPUT_NAME: "build-args-output"
+        EXPECTED_VALUE: "--log-level=warning --fail-level=error"
+      run: |
+        ACTUAL_VALUE=$(cat build_args_output.txt)
+        export ACTUAL_VALUE
+        .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash

.github/functional_tests/lake_test_args/action.yml

@@ -1,10 +1,10 @@
 name: 'Lake Test Args'
-description: 'Run `lean-action` on with `test-args` input'
+description: 'Run `lean-action` with `test-args` input and verify args are passed through'
 inputs:
   toolchain:
     description: 'Toolchain to use for the test'
     required: true
-runs: 
+runs:
   using: 'composite'
   steps:
     # TODO: once `lean-action` supports just setup, use it here
@@ -15,23 +15,24 @@ runs:
         echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
       shell: bash
 
-    - name: create lake package with `lake init ${{ inputs.lake-init-arguments }}`
+    - name: create lake package
       run: |
         lake init buildargs .lean
         lake update
       shell: bash
 
-    - name: create successful dummy test
+    - name: create test that verifies TEST_ARGS is set
       run: |
         {
           echo "@[test_runner]"
           echo "script dummy_test do"
-          echo "  println! \"Running fake tests...\""
-          echo "  println! \"Fake tests passed!\""
-          echo "  return 0" 
+          echo "  let testArgs <- IO.getEnv \"TEST_ARGS\""
+          echo "  let value := testArgs.get!"
+          echo "  IO.FS.writeFile \"test_args_output.txt\" value"
+          echo "  return 0"
         } >> lakefile.lean
       shell: bash
-     
+
     - name: "run `lean-action` with test-args"
       id: lean-action
       uses: ./
@@ -48,12 +49,14 @@ runs:
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
 
-    - name: verify `lake test` success
+    - name: verify test-args output
       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
+        OUTPUT_NAME: "test-args-output"
+        EXPECTED_VALUE: "--wfail"
+      run: |
+        ACTUAL_VALUE=$(cat test_args_output.txt)
+        export ACTUAL_VALUE
+        .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
 
     - name: lake clean
@@ -67,7 +70,7 @@ runs:
         test: true
         test-args: "--log-level=warning --fail-level=warning"
         use-github-cache: false
-    
+
     - name: verify `lean-action-multiple-test-args` outcome success
       env:
         OUTPUT_NAME: "lean-action-multiple-test-args.outcome"
@@ -76,10 +79,12 @@ runs:
       run: .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash
 
-    - name: verify `lake test` success
+    - name: verify multiple test-args output
       env:
-        OUTPUT_NAME: "test-status"
-        EXPECTED_VALUE: "SUCCESS"
-        ACTUAL_VALUE: ${{ steps.lean-action-multiple-test-args.outputs.build-status }}
-      run: .github/functional_tests/test_helpers/verify_action_output.sh
+        OUTPUT_NAME: "test-args-output"
+        EXPECTED_VALUE: "--log-level=warning --fail-level=warning"
+      run: |
+        ACTUAL_VALUE=$(cat test_args_output.txt)
+        export ACTUAL_VALUE
+        .github/functional_tests/test_helpers/verify_action_output.sh
       shell: bash

action.yml

@@ -225,6 +225,8 @@ runs:
     - name: test ${{ github.repository }}
       id: test
       if: ${{ steps.config.outputs.run-lake-test == 'true'}}
+      env:
+          TEST_ARGS: ${{ inputs.test-args }}
       run: |
         : Lake Test
         ${GITHUB_ACTION_PATH}/scripts/lake_test.sh