test: add workflow to run basic functional tests

.github/workflows/functional_tests.yml

@@ -0,0 +1,56 @@
+name: Functional Tests
+
+on:
+  pull_request:
+    branches: [main]
+    paths:
+      - "scripts/**"
+      - "action.yml"
+      - ".github/workflows/functional_tests.yml"
+  workflow_dispatch:
+
+jobs:
+  no-lake-test:
+    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"]
+    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: ./
+        with:
+          test: ${{ matrix.lake-test }}