Makefile

@@ -0,0 +1,20 @@
+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

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`, and run
+Install `elan` and `lake`. Execute
 ``` sh
-lake build
+make
 ```
 This builds the executable in `.lake/build/bin/pantograph`.
 
@@ -146,12 +146,7 @@ A Lean development shell is provided in the Nix flake.
 
 The tests are based on `LSpec`. To run tests,
 ``` sh
-lake test
+make test
-```
-You can run an individual test by specifying a prefix
-
-``` sh
-lake test -- "Tactic/No Confuse"
 ```
 
 ## Nix based workflow

lakefile.lean

@@ -10,7 +10,7 @@ lean_lib Pantograph {
 @[default_target]
 lean_exe pantograph {
   root := `Main
-  -- Solves the native symbol not found problem
+  -- Somehow solves the native symbol not found problem
   supportInterpreter := true
 }
 
@@ -18,9 +18,8 @@ require LSpec from git
   "https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
 lean_lib Test {
 }
-@[test_driver]
 lean_exe test {
   root := `Test.Main
-  -- Solves the native symbol not found problem
+  -- Somehow solves the native symbol not found problem
   supportInterpreter := true
 }