From fef7f1e2f3b4f816d3d61794a2dfba8f1ab333b2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 13 Jan 2025 12:43:19 -0800 Subject: [PATCH 1/3] feat: Pickle constants in goal state --- Pantograph/Serial.lean | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index bd01169..c242713 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -59,6 +59,12 @@ and then add the new constants. def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit := Pantograph.pickle path (env.header.imports, env.constants.map₂) +def resurrectEnvironment + (imports : Array Import) + (map₂ : PHashMap Name ConstantInfo) + : IO Environment := do + let env ← importModules imports {} 0 + env.replay (Std.HashMap.ofList map₂.toList) /-- Unpickle an `Environment` from disk. @@ -68,8 +74,7 @@ and then replace the new constants. @[export pantograph_env_unpickle_m] def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path - let env ← importModules imports {} 0 - return (← env.replay (Std.HashMap.ofList map₂.toList), region) + return (← resurrectEnvironment imports map₂, region) open Lean.Core in @@ -88,7 +93,9 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit : savedState := { term := { meta := { - core, + core := { + env, nextMacroScope, ngen, .. + }, meta, } «elab», @@ -100,9 +107,10 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit : convMVar?, calcPrevRhs?, } := goalState - --let env := core.env Pantograph.pickle path ( - ({ core with } : CompactCoreState), + env.constants.map₂, + + ({ nextMacroScope, ngen } : CompactCoreState), meta, «elab», tactic, @@ -117,6 +125,8 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit : def goalStateUnpickle (path : System.FilePath) (env : Environment) : IO (GoalState × CompactedRegion) := unsafe do let (( + map₂, + compactCore, meta, «elab», @@ -127,6 +137,8 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment) convMVar?, calcPrevRhs?, ), region) ← Pantograph.unpickle ( + PHashMap Name ConstantInfo × + CompactCoreState × Meta.State × Elab.Term.State × @@ -137,6 +149,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment) Option (MVarId × MVarId × List MVarId) × Option (MVarId × Expr) ) path + let env ← env.replay (Std.HashMap.ofList map₂.toList) let goalState := { savedState := { term := { From 9d445783c29a2f6b567ffb46bdca0c724c62587f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 13 Jan 2025 12:50:25 -0800 Subject: [PATCH 2/3] feat: Draft tactic REPL interface --- Pantograph/Library.lean | 8 ++++++++ Pantograph/Protocol.lean | 1 + Repl.lean | 21 ++++++++++++--------- doc/repl.md | 12 +++++++----- 4 files changed, 28 insertions(+), 14 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index bb094b6..b5c3655 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -207,6 +207,14 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: Stri | .ok syn => pure syn | .error error => return .parseError error state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq) +@[export pantograph_goal_try_draft_m] +protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult := do + let expr ← match (← parseTermM expr) with + | .ok syn => pure syn + | .error error => return .parseError error + runTermElabM do + state.restoreElabM + state.tryTacticM goal (Tactic.evalDraft expr) @[export pantograph_goal_let_m] def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryLet goal binderName type diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 62f3f69..7faef01 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -237,6 +237,7 @@ structure GoalTactic where calc?: Option String := .none -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored. conv?: Option Bool := .none + draft?: Option String := .none -- In case of the `have` tactic, the new free variable name is provided here binderName?: Option String := .none diff --git a/Repl.lean b/Repl.lean index 1fd8266..3fb43be 100644 --- a/Repl.lean +++ b/Repl.lean @@ -145,24 +145,27 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let .some goal := goalState.goals.get? args.goalId | return .error $ errorIndex s!"Invalid goal index {args.goalId}" let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do - match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv? with - | .some tactic, .none, .none, .none, .none, .none => do + -- NOTE: Should probably use a macro to handle this... + match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?, args.draft? with + | .some tactic, .none, .none, .none, .none, .none, .none => do pure <| Except.ok <| ← goalState.tryTactic goal tactic - | .none, .some expr, .none, .none, .none, .none => do + | .none, .some expr, .none, .none, .none, .none, .none => do pure <| Except.ok <| ← goalState.tryAssign goal expr - | .none, .none, .some type, .none, .none, .none => do + | .none, .none, .some type, .none, .none, .none, .none => do let binderName := args.binderName?.getD "" pure <| Except.ok <| ← goalState.tryHave goal binderName type - | .none, .none, .none, .some type, .none, .none => do + | .none, .none, .none, .some type, .none, .none, .none => do let binderName := args.binderName?.getD "" pure <| Except.ok <| ← goalState.tryLet goal binderName type - | .none, .none, .none, .none, .some pred, .none => do + | .none, .none, .none, .none, .some pred, .none, .none => do pure <| Except.ok <| ← goalState.tryCalc goal pred - | .none, .none, .none, .none, .none, .some true => do + | .none, .none, .none, .none, .none, .some true, .none => do pure <| Except.ok <| ← goalState.conv goal - | .none, .none, .none, .none, .none, .some false => do + | .none, .none, .none, .none, .none, .some false, .none => do pure <| Except.ok <| ← goalState.convExit - | _, _, _, _, _, _ => + | .none, .none, .none, .none, .none, .none, .some draft => do + pure <| Except.ok <| ← goalState.tryDraft goal draft + | _, _, _, _, _, _, _ => let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied" pure $ Except.error $ error match nextGoalState? with diff --git a/doc/repl.md b/doc/repl.md index d332986..c7c6f3f 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -33,6 +33,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va to the previous `rhs`. - `{ "conv": }`: Enter or exit conversion tactic mode. In the case of exit, the goal id is ignored. + - `{ "draft": }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed. * `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: Execute continuation/resumption - `{ "branch": }`: Continue on branch state. The current state must have no goals. @@ -44,11 +45,12 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va state. The user is responsible to ensure the sender/receiver instances share the same environment. * `frontend.process { ["fileName": ,] ["file": ], invocations: - , sorrys: , newConstants: }`: Executes the Lean frontend on - a file, collecting the tactic invocations (`"invocations": true`), the - sorrys and type errors into goal states (`"sorrys": true`), and new constants - (`"newConstants": true`). In the case of `sorrys`, this command additionally - outputs the position of each captured `sorry`. + , sorrys: , typeErrorsAsGoals: , newConstants: }`: + Executes the Lean frontend on a file, collecting the tactic invocations + (`"invocations": true`), the sorrys and type errors into goal states + (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of + `sorrys`, this command additionally outputs the position of each captured + `sorry`. ## Errors From 62363cb9438d8f7875227a180bbf618865675141 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 14 Jan 2025 13:21:38 -0800 Subject: [PATCH 3/3] fix: Over-eager assertion of fvarId validity --- Pantograph/Frontend/MetaTranslate.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean index bd3568d..c6592d2 100644 --- a/Pantograph/Frontend/MetaTranslate.lean +++ b/Pantograph/Frontend/MetaTranslate.lean @@ -68,7 +68,8 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do match e with | .fvar fvarId => let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}" - assert! (← getLCtx).contains fvarId' + -- Delegating this to `Meta.check` later + --assert! (← getLCtx).contains fvarId' return .done $ .fvar fvarId' | .mvar mvarId => do -- Must not be assigned