diff --git a/Main.lean b/Main.lean index 28b8126..c08014d 100644 --- a/Main.lean +++ b/Main.lean @@ -110,7 +110,10 @@ def execute (command: Command): Subroutine Lean.Json := do | .ok expr => do try let format ← Lean.Meta.ppExpr (← Lean.Meta.inferType expr) - return Lean.toJson <| ({ type := toString format }: ExprTypeResult) + return Lean.toJson <| ({ + type := toString format, + roundTrip := toString <| (← Lean.Meta.ppExpr expr) + }: ExprTypeResult) catch exception => return errorI "typing" (← exception.toMessageData.toString) proof_start (args: ProofStart): Subroutine Lean.Json := do diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index b6442c4..4ad79b5 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -52,6 +52,7 @@ structure ExprType where deriving Lean.FromJson structure ExprTypeResult where type: String + roundTrip: String deriving Lean.ToJson structure ProofStart where diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 4b1c620..0d1c2d6 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -20,7 +20,7 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax := (fileName := "") -def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do +def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do try let expr ← Elab.Term.elabType syn -- Immediately synthesise all metavariables if we need to leave the elaboration context. @@ -29,6 +29,15 @@ def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do let expr ← instantiateMVars expr return .ok expr catch ex => return .error (← ex.toMessageData.toString) +def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do + try + let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none) + -- Immediately synthesise all metavariables if we need to leave the elaboration context. + -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070 + --Elab.Term.synthesizeSyntheticMVarsNoPostponing + let expr ← instantiateMVars expr + return .ok expr + catch ex => return .error (← ex.toMessageData.toString) structure BoundExpression where binders: Array (String × String) diff --git a/README.md b/README.md index ff4b8e1..68ea647 100644 --- a/README.md +++ b/README.md @@ -2,20 +2,23 @@ An interaction system for Lean 4. +![Pantograph](doc/icon.svg) + ## Installation Install `elan` and `lean4`. Then, execute ``` sh lake build ``` -In order to use `mathlib`, its binary must also be built +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`, ``` sh -lake build Qq -lake build aesop -lake build std -lake build mathlib +LIB="../lib" +LIB_MATHLIB="$LIB/mathlib4/lake-packages" +export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib" + +LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ ``` -In a future version, the dependencies of mathlib will be removed and the user will be responsible for adding such library paths to `LEAN_PATH`. +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 @@ -42,7 +45,7 @@ $ build/bin/Pantograph Init catalog inspect {"name": "Nat.le_add_left"} ``` -Example with `mathlib` (~90k symbols) +Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting) ``` $ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm catalog @@ -59,6 +62,17 @@ proof.printTree {"treeId": 0} ``` where the application of `assumption` should lead to a failure. +## Commands + +See `Pantograph/Commands.lean` for a description of the parameters and return values in Json. +- `catalog`: Display a list of all safe Lean symbols in the current context +- `inspect {"name": }`: Show the type and package of a given symbol +- `clear`: Delete all cached expressions and proof trees +- `expr.type {"expr": }`: Determine the type of an expression and round-trip it +- `proof.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new proof state from a given expression or symbol +- `proof.tactic {"treeId": , "stateId": , "goalId": , "tactic": string}`: Execute a tactic on a given proof state +- `proof.printTree {"treeId": }`: Print the topological structure of a proof tree + ## Troubleshooting If lean encounters stack overflow problems when printing catalog, execute this before running lean: diff --git a/doc/icon.svg b/doc/icon.svg new file mode 100644 index 0000000..394b412 --- /dev/null +++ b/doc/icon.svg @@ -0,0 +1,73 @@ + + + + diff --git a/lakefile.lean b/lakefile.lean index 458c2ac..f0832e2 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -3,11 +3,7 @@ open Lake DSL package pantograph -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "8e5a00a8afc8913c0584cb85f37951995275fd87" - lean_lib Pantograph { - -- add library configuration options here } @[default_target] @@ -20,11 +16,9 @@ lean_exe pantograph { require LSpec from git "https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41" lean_lib Test { - -- add library configuration options here } lean_exe test { root := `Test.Main -- Somehow solves the native symbol not found problem supportInterpreter := true - }