From 256a617677b34ccbb8065269beb166a75a7c24d5 Mon Sep 17 00:00:00 2001
From: austinletson <waustinletson@gmail.com>
Date: Mon, 20 May 2024 07:14:29 -0400
Subject: [PATCH 1/5] test: add workflow to run basic functional tests

Add functional test for,
- basic `lake init`
- basic `lake init` with basic `lake test`
- `lake init` with `math` template
- `lake init` with `math` template and basic `lake test`
---
 .github/workflows/functional_tests.yml | 48 ++++++++++++++++++++++++++
 tests/standalone/.gitignore            |  1 +
 tests/standalone/Main.lean             |  4 +++
 tests/standalone/Standalone.lean       |  3 ++
 tests/standalone/Standalone/Basic.lean |  1 +
 tests/standalone/lake-manifest.json    |  5 +++
 tests/standalone/lakefile.lean         | 12 +++++++
 tests/standalone/lean-toolchain        |  1 +
 8 files changed, 75 insertions(+)
 create mode 100644 .github/workflows/functional_tests.yml
 create mode 100644 tests/standalone/.gitignore
 create mode 100644 tests/standalone/Main.lean
 create mode 100644 tests/standalone/Standalone.lean
 create mode 100644 tests/standalone/Standalone/Basic.lean
 create mode 100644 tests/standalone/lake-manifest.json
 create mode 100644 tests/standalone/lakefile.lean
 create mode 100644 tests/standalone/lean-toolchain

diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml
new file mode 100644
index 0000000..9f5f77b
--- /dev/null
+++ b/.github/workflows/functional_tests.yml
@@ -0,0 +1,48 @@
+name: Functional Tests
+
+on: [push, 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]" >> lakefile.lean
+          echo "script dummy_test do" >> lakefile.lean
+          echo "  println! \"Running fake tests...\"" >> lakefile.lean
+          echo "  println! \"Fake tests passed!\"" >> lakefile.lean
+          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 }}
\ No newline at end of file
diff --git a/tests/standalone/.gitignore b/tests/standalone/.gitignore
new file mode 100644
index 0000000..bfb30ec
--- /dev/null
+++ b/tests/standalone/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/tests/standalone/Main.lean b/tests/standalone/Main.lean
new file mode 100644
index 0000000..cba7dab
--- /dev/null
+++ b/tests/standalone/Main.lean
@@ -0,0 +1,4 @@
+import «Standalone»
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/tests/standalone/Standalone.lean b/tests/standalone/Standalone.lean
new file mode 100644
index 0000000..2faa4fa
--- /dev/null
+++ b/tests/standalone/Standalone.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Standalone` library.
+-- Import modules here that should be built as part of the library.
+import «Standalone».Basic
\ No newline at end of file
diff --git a/tests/standalone/Standalone/Basic.lean b/tests/standalone/Standalone/Basic.lean
new file mode 100644
index 0000000..e99d3a6
--- /dev/null
+++ b/tests/standalone/Standalone/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"
\ No newline at end of file
diff --git a/tests/standalone/lake-manifest.json b/tests/standalone/lake-manifest.json
new file mode 100644
index 0000000..2571267
--- /dev/null
+++ b/tests/standalone/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "standalone",
+ "lakeDir": ".lake"}
diff --git a/tests/standalone/lakefile.lean b/tests/standalone/lakefile.lean
new file mode 100644
index 0000000..6c506fd
--- /dev/null
+++ b/tests/standalone/lakefile.lean
@@ -0,0 +1,12 @@
+import Lake
+open Lake DSL
+
+package «standalone» where
+  -- add package configuration options here
+
+lean_lib «Standalone» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «standalone» where
+  root := `Main
diff --git a/tests/standalone/lean-toolchain b/tests/standalone/lean-toolchain
new file mode 100644
index 0000000..d8a6d7e
--- /dev/null
+++ b/tests/standalone/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.8.0-rc1

From c7c0fd6265def5884279d298b49d1abe5aca2c5a Mon Sep 17 00:00:00 2001
From: austinletson <waustinletson@gmail.com>
Date: Mon, 20 May 2024 18:56:46 -0400
Subject: [PATCH 2/5] test: update workflow trigger to PRs to main

---
 .github/workflows/functional_tests.yml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml
index 9f5f77b..75a8723 100644
--- a/.github/workflows/functional_tests.yml
+++ b/.github/workflows/functional_tests.yml
@@ -1,6 +1,9 @@
 name: Functional Tests
 
-on: [push, workflow_dispatch]
+on: 
+  pull_request:
+    branches: [main]
+  workflow_dispatch:
 
 jobs:
   no-lake-test:

From 040e545ffd20e1841d5dfd38a00aca957fd94aa3 Mon Sep 17 00:00:00 2001
From: austinletson <waustinletson@gmail.com>
Date: Mon, 20 May 2024 18:59:49 -0400
Subject: [PATCH 3/5] fix: actionlint

---
 .github/workflows/functional_tests.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml
index 75a8723..f75b27e 100644
--- a/.github/workflows/functional_tests.yml
+++ b/.github/workflows/functional_tests.yml
@@ -21,7 +21,7 @@ jobs:
           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
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
       
       - uses: actions/checkout@v4

From 775e656e7aa791c6262f526c1a86abcd8cd405b9 Mon Sep 17 00:00:00 2001
From: austinletson <waustinletson@gmail.com>
Date: Mon, 20 May 2024 19:02:10 -0400
Subject: [PATCH 4/5] fix: actionlint

---
 .github/workflows/functional_tests.yml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml
index f75b27e..acf583a 100644
--- a/.github/workflows/functional_tests.yml
+++ b/.github/workflows/functional_tests.yml
@@ -34,11 +34,13 @@ jobs:
       - name: create dummy test
         if: ${{ matrix.lake-test == 'true' }}
         run: |
-          echo "@[test_runner]" >> lakefile.lean
-          echo "script dummy_test do" >> lakefile.lean
-          echo "  println! \"Running fake tests...\"" >> lakefile.lean
-          echo "  println! \"Fake tests passed!\"" >> lakefile.lean
-          echo "  return 0" >> lakefile.lean
+          {
+            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: |

From 8ab59d14d07c6f5cdef316b0ddc465b416168fcf Mon Sep 17 00:00:00 2001
From: austinletson <waustinletson@gmail.com>
Date: Mon, 20 May 2024 19:11:04 -0400
Subject: [PATCH 5/5] test: add paths to functional_tests.yml

---
 .github/workflows/functional_tests.yml |  9 ++++++---
 tests/standalone/.gitignore            |  1 -
 tests/standalone/Main.lean             |  4 ----
 tests/standalone/Standalone.lean       |  3 ---
 tests/standalone/Standalone/Basic.lean |  1 -
 tests/standalone/lake-manifest.json    |  5 -----
 tests/standalone/lakefile.lean         | 12 ------------
 tests/standalone/lean-toolchain        |  1 -
 8 files changed, 6 insertions(+), 30 deletions(-)
 delete mode 100644 tests/standalone/.gitignore
 delete mode 100644 tests/standalone/Main.lean
 delete mode 100644 tests/standalone/Standalone.lean
 delete mode 100644 tests/standalone/Standalone/Basic.lean
 delete mode 100644 tests/standalone/lake-manifest.json
 delete mode 100644 tests/standalone/lakefile.lean
 delete mode 100644 tests/standalone/lean-toolchain

diff --git a/.github/workflows/functional_tests.yml b/.github/workflows/functional_tests.yml
index acf583a..49c2849 100644
--- a/.github/workflows/functional_tests.yml
+++ b/.github/workflows/functional_tests.yml
@@ -1,8 +1,12 @@
 name: Functional Tests
 
-on: 
+on:
   pull_request:
     branches: [main]
+    paths:
+      - "scripts/**"
+      - "action.yml"
+      - ".github/workflows/functional_tests.yml"
   workflow_dispatch:
 
 jobs:
@@ -23,7 +27,6 @@ jobs:
           ./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
@@ -50,4 +53,4 @@ jobs:
       - name: "run `lean-action` with on `lake ${{matrix.lake-init-command}}` with test: ${{ matrix.lake-test }}"
         uses: ./
         with:
-          test: ${{ matrix.lake-test }}
\ No newline at end of file
+          test: ${{ matrix.lake-test }}
diff --git a/tests/standalone/.gitignore b/tests/standalone/.gitignore
deleted file mode 100644
index bfb30ec..0000000
--- a/tests/standalone/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/.lake
diff --git a/tests/standalone/Main.lean b/tests/standalone/Main.lean
deleted file mode 100644
index cba7dab..0000000
--- a/tests/standalone/Main.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-import «Standalone»
-
-def main : IO Unit :=
-  IO.println s!"Hello, {hello}!"
diff --git a/tests/standalone/Standalone.lean b/tests/standalone/Standalone.lean
deleted file mode 100644
index 2faa4fa..0000000
--- a/tests/standalone/Standalone.lean
+++ /dev/null
@@ -1,3 +0,0 @@
--- This module serves as the root of the `Standalone` library.
--- Import modules here that should be built as part of the library.
-import «Standalone».Basic
\ No newline at end of file
diff --git a/tests/standalone/Standalone/Basic.lean b/tests/standalone/Standalone/Basic.lean
deleted file mode 100644
index e99d3a6..0000000
--- a/tests/standalone/Standalone/Basic.lean
+++ /dev/null
@@ -1 +0,0 @@
-def hello := "world"
\ No newline at end of file
diff --git a/tests/standalone/lake-manifest.json b/tests/standalone/lake-manifest.json
deleted file mode 100644
index 2571267..0000000
--- a/tests/standalone/lake-manifest.json
+++ /dev/null
@@ -1,5 +0,0 @@
-{"version": 7,
- "packagesDir": ".lake/packages",
- "packages": [],
- "name": "standalone",
- "lakeDir": ".lake"}
diff --git a/tests/standalone/lakefile.lean b/tests/standalone/lakefile.lean
deleted file mode 100644
index 6c506fd..0000000
--- a/tests/standalone/lakefile.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-import Lake
-open Lake DSL
-
-package «standalone» where
-  -- add package configuration options here
-
-lean_lib «Standalone» where
-  -- add library configuration options here
-
-@[default_target]
-lean_exe «standalone» where
-  root := `Main
diff --git a/tests/standalone/lean-toolchain b/tests/standalone/lean-toolchain
deleted file mode 100644
index d8a6d7e..0000000
--- a/tests/standalone/lean-toolchain
+++ /dev/null
@@ -1 +0,0 @@
-leanprover/lean4:v4.8.0-rc1