From 76765c913c7b45330ce3bc01c899920ce630eff9 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 18 Aug 2024 12:22:59 -0700
Subject: [PATCH] test: Use `lake test`. Retired `Makefile`

---
 Makefile      | 20 --------------------
 README.md     | 11 ++++++++---
 lakefile.lean |  5 +++--
 3 files changed, 11 insertions(+), 25 deletions(-)
 delete mode 100644 Makefile

diff --git a/Makefile b/Makefile
deleted file mode 100644
index 86f9e5b..0000000
--- a/Makefile
+++ /dev/null
@@ -1,20 +0,0 @@
-LIB := ./.lake/build/lib/Pantograph.olean
-EXE := ./.lake/build/bin/pantograph
-SOURCE := $(wildcard *.lean Pantograph/*.lean Pantograph/**/*.lean) lean-toolchain
-
-TEST_EXE := ./.lake/build/bin/test
-TEST_SOURCE := $(wildcard Test/*.lean Test/**/*.lean)
-
-$(LIB) $(EXE): $(SOURCE)
-	lake build pantograph
-
-$(TEST_EXE): $(LIB) $(TEST_SOURCE)
-	lake build test
-
-test: $(TEST_EXE)
-	$(TEST_EXE)
-
-clean:
-	lake clean
-
-.PHONY: test clean
diff --git a/README.md b/README.md
index c136337..562f7ac 100644
--- a/README.md
+++ b/README.md
@@ -11,9 +11,9 @@ examine the symbol list of a Lean project for machine learning.
 
 For Nix based workflow, see below.
 
-Install `elan` and `lake`. Execute
+Install `elan` and `lake`, and run
 ``` sh
-make
+lake build
 ```
 This builds the executable in `.lake/build/bin/pantograph`.
 
@@ -146,7 +146,12 @@ A Lean development shell is provided in the Nix flake.
 
 The tests are based on `LSpec`. To run tests,
 ``` sh
-make test
+lake test
+```
+You can run an individual test by specifying a prefix
+
+``` sh
+lake test -- "Tactic/No Confuse"
 ```
 
 ## Nix based workflow
diff --git a/lakefile.lean b/lakefile.lean
index d7bc630..c68d0db 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -10,7 +10,7 @@ lean_lib Pantograph {
 @[default_target]
 lean_exe pantograph {
   root := `Main
-  -- Somehow solves the native symbol not found problem
+  -- Solves the native symbol not found problem
   supportInterpreter := true
 }
 
@@ -18,8 +18,9 @@ require LSpec from git
   "https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
 lean_lib Test {
 }
+@[test_driver]
 lean_exe test {
   root := `Test.Main
-  -- Somehow solves the native symbol not found problem
+  -- Solves the native symbol not found problem
   supportInterpreter := true
 }
-- 
2.44.1