From 2c3a7adb61d4e1922d99744fda483a2063f3e3b5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 2 Oct 2023 10:26:19 -0700 Subject: [PATCH] Use makefile instead of ad-hoc script --- Makefile | 17 +++++++++++++++++ README.md | 19 +++++++++---------- Test/all.sh | 3 --- 3 files changed, 26 insertions(+), 13 deletions(-) create mode 100644 Makefile delete mode 100755 Test/all.sh diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..c201842 --- /dev/null +++ b/Makefile @@ -0,0 +1,17 @@ +LIB := build/lib/Pantograph.olean +EXE := build/bin/pantograph +SOURCE := $(wildcard Pantograph/*.lean) Main.lean Pantograph.lean + +TEST_EXE := build/bin/test +TEST_SOURCE := $(wildcard Test/*.lean) + +$(LIB) $(EXE): $(SOURCE) + lake build + +$(TEST_EXE): $(LIB) $(TEST_SOURCE) + lake build test + +test: $(TEST_EXE) + lake env $(TEST_EXE) + +.PHONY: test diff --git a/README.md b/README.md index 273e865..b8e0868 100644 --- a/README.md +++ b/README.md @@ -6,11 +6,11 @@ An interaction system for Lean 4. ## Installation -Install `elan` and `lean4`. Then, execute +Install `elan` and `lake`. Execute ``` sh -lake build +make build/bin/pantograph ``` -Then, setup the `LEAN_PATH` environment variable so it contains the library path of lean libraries. The libraries must be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`, +setup the `LEAN_PATH` environment variable so it contains the library path of lean libraries. The libraries must be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`, ``` sh LIB="../lib" LIB_MATHLIB="$LIB/mathlib4/lake-packages" @@ -18,12 +18,11 @@ export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATH LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ ``` -Note that `lean-toolchain` must be present in the `$PWD` in order to run Pantograph! This is because Pantograph taps into Lean's internals. ## Usage ``` sh -build/bin/pantograph MODULES|LEAN_OPTIONS +pantograph MODULES|LEAN_OPTIONS ``` The REPL loop accepts commands as single-line JSON inputs and outputs either an @@ -36,23 +35,23 @@ command { ... } The list of available commands can be found in `Pantograph/Commands.lean` and below. An empty command aborts the REPL. -The `Pantograph` executable must be run with a list of modules to import. It can +The `pantograph` executable must be run with a list of modules to import. It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. Example: (~5k symbols) ``` -$ build/bin/Pantograph Init +$ pantograph Init lib.catalog lib.inspect {"name": "Nat.le_add_left"} ``` Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting) ``` -$ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm +$ pantograph Mathlib.Analysis.Seminorm lib.catalog ``` Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof ``` -$ env build/bin/Pantograph Init +$ pantograph Init goal.start {"expr": "∀ (n m : Nat), n + m = m + n"} goal.tactic {"goalId": 0, "tactic": "intro n m"} goal.tactic {"goalId": 1, "tactic": "assumption"} @@ -106,5 +105,5 @@ ulimit -s unlimited The tests are based on `LSpec`. To run tests, ``` sh -test/all.sh +make test ``` diff --git a/Test/all.sh b/Test/all.sh deleted file mode 100755 index 9d940bd..0000000 --- a/Test/all.sh +++ /dev/null @@ -1,3 +0,0 @@ -#!/bin/bash - -lake build test && lake env build/bin/test