refactor: use lake test driver

leanprover · Jul 3, 2024 · 3982567 · 3982567
1 parent 4334dd9
commit 3982567
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 8 deletions.
diff --git a/GNUmakefile b/GNUmakefile
@@ -1,21 +1,15 @@
 # Ensure that panics actually cause the tests to fail
 export LEAN_ABORT_ON_PANIC=1
 
-.PHONY: all build test lint eval
+.PHONY: all build test eval
 
 all: build test
 
 build:
 	lake build
 
 test:
-	lake build Test
-
-%.run: build
-	lake env lean $(@:.run=.lean)
-
-lint: build
-	lake exe runLinter Sat
+	lake test
 
 eval:
 	bash check_eval.bash
diff --git a/lakefile.lean b/lakefile.lean
@@ -8,7 +8,9 @@ package LeanSAT {
   moreGlobalServerArgs := #["--tstack=32000"]
 }
 
+@[test_driver]
 lean_lib Test
+
 lean_lib Eval
 
 @[default_target]