From 76765c913c7b45330ce3bc01c899920ce630eff9 Mon Sep 17 00:00:00 2001 From: Leni Aniva 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