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

---
 .github/workflows/functional_tests.yml |  3 +++
 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, 3 insertions(+), 27 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..7922410 100644
--- a/.github/workflows/functional_tests.yml
+++ b/.github/workflows/functional_tests.yml
@@ -3,6 +3,9 @@ name: Functional Tests
 on: 
   pull_request:
     branches: [main]
+    paths:
+      - 'scripts/**'
+      - 'action.yml'
   workflow_dispatch:
 
 jobs:
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