fix: use eval to expand lake build arguments (#109)

Fix the `lake_build.sh` script to expand the arguments to `lake build`
with the `eval` command.

Previously, passing multiple arguments to `lake build` via the
`build-args` configuration input caused errors
because the `lake_build.sh` script passed all the arguments as one
string.

Add functional test for `build-args` input with case for single and
multiple arguments to lake build.

Closes #108

.github/functional_tests/lake_build_args/action.yml

@@ -0,0 +1,72 @@
+name: 'Lake Build Args'
+description: 'Run `lean-action` on with `build-args` input'
+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 with `lake init ${{ inputs.lake-init-arguments }}`
+      run: |
+        lake init buildargs .lean
+        lake update
+      shell: bash
+
+    - name: "run `lean-action` with build-args"
+      id: lean-action
+      uses: ./
+      with:
+        build-args: "--wfail"
+        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: lake clean
+      run: lake clean
+      shell: bash
+
+    - name: "run `lean-action` with multiple build args"
+      id: lean-action-multiple-build-args
+      uses: ./
+      with:
+        build-args: "--log-level=warning --fail-level=warning"
+        use-github-cache: false
+
+    - name: verify `lean-action-multiple-build-args` outcome success
+      env:
+        OUTPUT_NAME: "lean-action-multiple-build-args.outcome"
+        EXPECTED_VALUE: "success"
+        ACTUAL_VALUE: ${{ steps.lean-action-multiple-build-args.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-multiple-build-args.outputs.build-status }}
+      run: .github/functional_tests/test_helpers/verify_action_output.sh
+      shell: bash

.github/workflows/functional_tests.yml

@@ -62,6 +62,14 @@ jobs:
         with:
           toolchain: ${{ env.toolchain }}
 
+  lake-build-args:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: ./.github/functional_tests/lake_build_args
+        with:
+          toolchain: ${{ env.toolchain }}
+
   detect-mathlib:
     runs-on: ubuntu-latest
     steps:

scripts/lake_build.sh

@@ -21,4 +21,5 @@ handle_exit() {
 
 trap handle_exit EXIT
 
-lake build "$BUILD_ARGS"
+# use eval to ensure build arguments are expanded
+eval "lake build $BUILD_ARGS"