feat: Prograde tactics #83

Merged
aniva merged 24 commits from tactic/eval into dev 2024-08-31 20:04:39 -07:00
3 changed files with 11 additions and 25 deletions
Showing only changes of commit 0c529c5cd9 - Show all commits

View File

@ -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

View File

@ -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

View File

@ -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
}