From fef7f1e2f3b4f816d3d61794a2dfba8f1ab333b2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 13 Jan 2025 12:43:19 -0800 Subject: [PATCH 1/7] 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/7] 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/7] 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 From 4f5ffc1ffbc00a0b21fe0f12514a75fc925701b3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 15 Jan 2025 21:02:04 -0800 Subject: [PATCH 4/7] feat: Protocol for module access --- Pantograph/Protocol.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 62f3f69..c73e791 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -112,6 +112,24 @@ structure ExprEchoResult where type: Expression deriving Lean.ToJson +-- Describe the current state of the environment +structure EnvDescribe where + deriving Lean.FromJson +structure EnvDescribeResult where + imports : Array String + modules : Array String + deriving Lean.ToJson + +-- Describe a module +structure EnvModule where + module : String + deriving Lean.FromJson +structure EnvModuleResult where + imports: Array String + constNames: Array String + extraConstNames: Array String + deriving Lean.ToJson + -- Print all symbols in environment structure EnvCatalog where deriving Lean.FromJson From c9f524b9aea1c475dc3085bd109fbd7ea9f4187a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 15 Jan 2025 21:20:05 -0800 Subject: [PATCH 5/7] feat: Implement `env.describe` and `env.module_read` --- Pantograph/Environment.lean | 16 ++++++++++++++++ Pantograph/Protocol.lean | 4 ++-- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index c48414a..6bd3f76 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -43,6 +43,22 @@ def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String := if isNameInternal n || info.isUnsafe then Option.none else Option.some <| toCompactSymbolName n info +def describe (_: Protocol.EnvDescribe): CoreM Protocol.EnvDescribeResult := do + let env ← Lean.MonadEnv.getEnv + return { + imports := env.header.imports.map toString, + modules := env.header.moduleNames.map (·.toString), + } +def moduleRead (args: Protocol.EnvModuleRead): CoreM (Protocol.CR Protocol.EnvModuleReadResult) := do + let env ← Lean.MonadEnv.getEnv + let .some i := env.header.moduleNames.findIdx? (· == args.module.toName) | + return .error $ Protocol.errorIndex s!"Module not found {args.module}" + let data := env.header.moduleData[i]! + return .ok { + imports := data.imports.map toString, + constNames := data.constNames.map (·.toString), + extraConstNames := data.extraConstNames.map (·.toString), + } def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do let env ← Lean.MonadEnv.getEnv let names := env.constants.fold (init := #[]) (λ acc name info => diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index c73e791..cab288c 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -121,10 +121,10 @@ structure EnvDescribeResult where deriving Lean.ToJson -- Describe a module -structure EnvModule where +structure EnvModuleRead where module : String deriving Lean.FromJson -structure EnvModuleResult where +structure EnvModuleReadResult where imports: Array String constNames: Array String extraConstNames: Array String From bc4bf47c8b8c5e9c8d39ef7675fca7c7b942e152 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 15 Jan 2025 21:23:37 -0800 Subject: [PATCH 6/7] feat: Implement repl interfaces --- Repl.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Repl.lean b/Repl.lean index 1fd8266..aebb738 100644 --- a/Repl.lean +++ b/Repl.lean @@ -48,6 +48,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | "reset" => run reset | "stat" => run stat | "expr.echo" => run expr_echo + | "env.describe" => run env_describe + | "env.module_read" => run env_module_read | "env.catalog" => run env_catalog | "env.inspect" => run env_inspect | "env.add" => run env_add @@ -85,6 +87,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get let nGoals := state.goalStates.size return .ok { nGoals } + env_describe (args: Protocol.EnvDescribe): MainM (CR Protocol.EnvDescribeResult) := do + let result ← Environment.describe args + return .ok result + env_module_read (args: Protocol.EnvModuleRead): MainM (CR Protocol.EnvModuleReadResult) := do + Environment.moduleRead args env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do let result ← Environment.catalog args return .ok result From be8dee6731f23462895484a91c815edcb70c116e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 24 Jan 2025 15:00:35 -0800 Subject: [PATCH 7/7] test: Add test for module read --- Test/Environment.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Test/Environment.lean b/Test/Environment.lean index b646279..c49cbae 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -110,6 +110,9 @@ def test_symbol_location : TestT IO Unit := do checkTrue "file" result.sourceUri?.isNone checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0 checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88 + let .ok { imports, constNames, extraConstNames } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ | fail "Module read failed" + checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"] + checkTrue "constNames" $ constNames.contains "Nat.succ_add" def suite: List (String × IO LSpec.TestSeq) := [