From df07b53a7749d2f3c633de59e37b80fb27d13b7c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Mon, 17 Feb 2025 15:39:57 +0100 Subject: [PATCH 01/47] Report errors in import statements. --- REPL/Frontend.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean index 9cc09145..8643573c 100644 --- a/REPL/Frontend.lean +++ b/REPL/Frontend.lean @@ -19,8 +19,9 @@ def processCommandsWithInfoTrees (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do let commandState := { commandState with infoState.enabled := true } + let oldMessages := commandState.messages.toList let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState - pure (s, s.messages.toList, s.infoState.trees.toList) + pure (s, oldMessages ++ s.messages.toList, s.infoState.trees.toList) /-- Process some text input, with or without an existing command state. From a860ef86ee84f258d2d003621b5ff53fca3acb91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 21 Feb 2025 16:54:01 +0100 Subject: [PATCH 02/47] Integrate PaperProof.BetterParser to enable proof trees. --- REPL/JSON.lean | 8 +- REPL/Main.lean | 16 +- REPL/PaperProof/BetterParser.lean | 251 ++++++++++++++++++++++++++++++ 3 files changed, 272 insertions(+), 3 deletions(-) create mode 100644 REPL/PaperProof/BetterParser.lean diff --git a/REPL/JSON.lean b/REPL/JSON.lean index d5c5ba2d..7a3260f4 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -6,6 +6,7 @@ Authors: Scott Morrison import Lean.Data.Json import Lean.Message import Lean.Elab.InfoTree.Main +import REPL.PaperProof.BetterParser open Lean Elab InfoTree @@ -18,6 +19,7 @@ structure CommandOptions where Anything else is ignored. -/ infotree : Option String + proofTrees : Option Bool := none /-- Run Lean commands. If `env = none`, starts a new session (in which you can use `import`). @@ -125,6 +127,7 @@ structure CommandResponse where sorries : List Sorry := [] tactics : List Tactic := [] infotree : Option Json := none + proofTreeEdges : Option (List (List PaperProof.ProofStep)) := none deriving FromJson def Json.nonemptyList [ToJson α] (k : String) : List α → List (String × Json) @@ -137,7 +140,10 @@ instance : ToJson CommandResponse where Json.nonemptyList "messages" r.messages, Json.nonemptyList "sorries" r.sorries, Json.nonemptyList "tactics" r.tactics, - match r.infotree with | some j => [("infotree", j)] | none => [] + match r.infotree with | some j => [("infotree", j)] | none => [], + match r.proofTreeEdges with + | some edges => Json.nonemptyList "proofTreeEdges" edges + | none => [], ] /-- diff --git a/REPL/Main.lean b/REPL/Main.lean index a4b97c3e..2e3d752c 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -11,6 +11,7 @@ import REPL.Lean.Environment import REPL.Lean.InfoTree import REPL.Lean.InfoTree.ToJson import REPL.Snapshots +import REPL.PaperProof.BetterParser /-! # A REPL for Lean. @@ -125,6 +126,13 @@ def tactics (trees : List InfoTree) : M m (List Tactic) := let proofStateId ← proofState.mapM recordProofSnapshot return Tactic.of goals tactic pos endPos proofStateId ns +def proofTrees (infoTrees : List InfoTree) : M m (List (List PaperProof.ProofStep)) := do + infoTrees.mapM fun infoTree => do + let proofTree ← PaperProof.BetterParser infoTree + match proofTree with + | .some proofTree => return proofTree.steps + | .none => return [] + /-- Record a `ProofSnapshot` and generate a JSON response for it. -/ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnapshot := none) : M m ProofStepResponse := do @@ -207,6 +215,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do let tactics ← match s.allTactics with | some true => tactics trees | _ => pure [] + let proofTreeEdges ← match s.proofTrees with + | some true => some <$> proofTrees trees + | _ => pure none let cmdSnapshot := { cmdState cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD @@ -230,8 +241,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do { env, messages, sorries, - tactics - infotree } + tactics, + infotree, + proofTreeEdges } def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do try diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean new file mode 100644 index 00000000..10eecd6f --- /dev/null +++ b/REPL/PaperProof/BetterParser.lean @@ -0,0 +1,251 @@ +/- +MIT License + +Copyright (c) 2023 Anton Kovsharov + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. +-/ + +/- +Modified. +-/ + +import Lean +import Lean.Meta.Basic +import Lean.Meta.CollectMVars +import REPL.Lean.InfoTree.ToJson + +open Lean Elab Server + +namespace PaperProof + +structure Hypothesis where + username : String + type : String + value : Option String + -- unique identifier for the hypothesis, fvarId + id : String + isProof : String + deriving Inhabited, ToJson, FromJson + +structure GoalInfo where + username : String + type : String + hyps : List Hypothesis + -- unique identifier for the goal, mvarId + id : MVarId + deriving Inhabited, ToJson, FromJson + +instance : BEq GoalInfo where + beq g1 g2 := g1.id == g2.id + +instance : Hashable GoalInfo where + hash g := hash g.id + +structure ProofStep where + tacticString : String + goalBefore : GoalInfo + goalsAfter : List GoalInfo + tacticDependsOn : List String + spawnedGoals : List GoalInfo + start : Option Lean.Position + finish : Option Lean.Position + deriving Inhabited, ToJson, FromJson + +def stepGoalsAfter (step : ProofStep) : List GoalInfo := step.goalsAfter ++ step.spawnedGoals + +def noInEdgeGoals (allGoals : Std.HashSet GoalInfo) (steps : List ProofStep) : Std.HashSet GoalInfo := + -- Some of the orphaned goals might be matched by tactics in sibling subtrees, e.g. for tacticSeq. + (steps.bind stepGoalsAfter).foldl Std.HashSet.erase allGoals + +/- + Instead of doing parsing of what user wrote (it wouldn't work for linarith etc), + let's do the following. + We have assigned something to our goal in mctxAfter. + All the fvars used in these assignments are what was actually used instead of what was in syntax. +-/ +def findHypsUsedByTactic (goalId: MVarId) (goalDecl : MetavarDecl) (mctxAfter : MetavarContext) : MetaM (List String) := do + let some expr := mctxAfter.eAssignment.find? goalId + | return [] + + -- Need to instantiate it to get all fvars + let fullExpr ← instantiateExprMVars expr + let fvarIds := (collectFVars {} fullExpr).fvarIds + let fvars := fvarIds.filterMap goalDecl.lctx.find? + let proofFvars ← fvars.filterM (Meta.isProof ·.toExpr) + -- let pretty := proofFvars.map (fun x => x.userName) + -- dbg_trace s!"Used {pretty}" + return proofFvars.map (fun x => x.fvarId.name.toString) |>.toList + +-- This is used to match goalsBefore with goalsAfter to see what was assigned to what +def findMVarsAssigned (goalId : MVarId) (mctxAfter : MetavarContext) : MetaM (List MVarId) := do + let some expr := mctxAfter.eAssignment.find? goalId + | return [] + let (_, s) ← (Meta.collectMVars expr).run {} + return s.result.toList + +def mayBeProof (expr : Expr) : MetaM String := do + let type : Expr ← Lean.Meta.inferType expr + if ← Meta.isProof expr then + return "proof" + if type.isSort then + return "universe" + else + return "data" + +def printGoalInfo (printCtx : ContextInfo) (id : MVarId) : IO GoalInfo := do + let some decl := printCtx.mctx.findDecl? id + | panic! "printGoalInfo: goal not found in the mctx" + -- to get tombstones in name ✝ for unreachable hypothesis + let lctx := decl.lctx |>.sanitizeNames.run' {options := {}} + let ppContext := printCtx.toPPContext lctx + let hyps ← lctx.foldrM (init := []) (fun hypDecl acc => do + if hypDecl.isAuxDecl || hypDecl.isImplementationDetail then + return acc + let type ← liftM (ppExprWithInfos ppContext hypDecl.type) + let value ← liftM (hypDecl.value?.mapM (ppExprWithInfos ppContext)) + let isProof : String ← printCtx.runMetaM decl.lctx (mayBeProof hypDecl.toExpr) + return ({ + username := hypDecl.userName.toString, + type := type.fmt.pretty, + value := value.map (·.fmt.pretty), + id := hypDecl.fvarId.name.toString, + isProof := isProof + } : Hypothesis) :: acc) + return ⟨ decl.userName.toString, (← ppExprWithInfos ppContext decl.type).fmt.pretty, hyps, id⟩ + +-- Returns unassigned goals from the provided list of goals +def getUnassignedGoals (goals : List MVarId) (mctx : MetavarContext) : IO (List MVarId) := do + goals.filterMapM fun id => do + if let none := mctx.findDecl? id then + return none + if mctx.eAssignment.contains id || + mctx.dAssignment.contains id then + return none + return some id + +structure Result where + steps : List ProofStep + allGoals : Std.HashSet GoalInfo + +def getGoalsChange (ctx : ContextInfo) (tInfo : TacticInfo) : IO (List (List String × GoalInfo × List GoalInfo)) := do + -- We want to filter out `focus` like tactics which don't do any assignments + -- therefore we check all goals on whether they were assigned during the tactic + let goalMVars := tInfo.goalsBefore ++ tInfo.goalsAfter + -- For printing purposes we always need to use the latest mctx assignments. For example in + -- have h := by calc + -- 3 ≤ 4 := by trivial + -- 4 ≤ 5 := by trivial + -- at mctxBefore type of `h` is `?m.260`, but by the time calc is elaborated at mctxAfter + -- it's known to be `3 ≤ 5` + let printCtx := {ctx with mctx := tInfo.mctxAfter} + let mut goalsBefore ← getUnassignedGoals goalMVars tInfo.mctxBefore + let mut goalsAfter ← getUnassignedGoals goalMVars tInfo.mctxAfter + let commonGoals := goalsBefore.filter fun g => goalsAfter.contains g + goalsBefore := goalsBefore.filter (!commonGoals.contains ·) + goalsAfter := goalsAfter.filter (!commonGoals.contains ·) + -- We need to match them into (goalBefore, goalsAfter) pairs according to assignment. + let mut result : List (List String × GoalInfo × List GoalInfo) := [] + for goalBefore in goalsBefore do + if let some goalDecl := tInfo.mctxBefore.findDecl? goalBefore then + let assignedMVars ← ctx.runMetaM goalDecl.lctx (findMVarsAssigned goalBefore tInfo.mctxAfter) + let tacticDependsOn ← ctx.runMetaM goalDecl.lctx + (findHypsUsedByTactic goalBefore goalDecl tInfo.mctxAfter) + + result := ( + tacticDependsOn, + ← printGoalInfo printCtx goalBefore, + ← goalsAfter.filter assignedMVars.contains |>.mapM (printGoalInfo printCtx) + ) :: result + return result + +-- TODO: solve rw_mod_cast + +def prettifySteps (stx : Syntax) (steps : List ProofStep) : List ProofStep := Id.run do + let prettify (tStr : String) := + let res := tStr.trim.dropRightWhile (· == ',') + -- rw puts final rfl on the "]" token + if res == "]" then "rfl" else res + match stx with + | `(tactic| rw [$_,*] $(_)?) + | `(tactic| rewrite [$_,*] $(_)?) => + return steps.map fun a => { a with tacticString := s!"rw [{prettify a.tacticString}]" } + | `(tactic| rwa [$_,*] $(_)?) => + let rwSteps := steps.map fun a => { a with tacticString := s!"rw [{prettify a.tacticString}]" } + let assumptionSteps := (if rwSteps.isEmpty then [] else rwSteps.getLast!.goalsAfter).map fun g => + { tacticString := "assumption", goalBefore := g, goalsAfter := [], tacticDependsOn := [], spawnedGoals := [], start := none, finish := none } + return rwSteps ++ assumptionSteps + | _ => return steps + +-- Comparator for names, e.g. so that _uniq.34 and _uniq.102 go in the right order. +-- That's not completely right because it doesn't compare prefixes but +-- it's much shorter to write than correct version and serves the purpose. +def nameNumLt (n1 n2 : Name) : Bool := + match n1, n2 with + | .num _ n₁, .num _ n₂ => n₁ < n₂ + | .num _ _, _ => true + | _, _ => false + +partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree) (res : List (Option Result)) : IO Result := do + let res := res.filterMap id + let some ctx := i.updateContext? ctx + | panic! "unexpected context node" + let steps := res.map (fun r => r.steps) |>.join + let allSubGoals := Std.HashSet.empty.insertMany $ res.bind (·.allGoals.toList) + if let .ofTacticInfo tInfo := i then + -- shortcut if it's not a tactic user wrote + -- \n trim to avoid empty lines/comments until next tactic, + -- especially at the end of theorem it will capture comment for the next one + let some tacticString := tInfo.stx.getSubstring?.map + (·.toString |>.splitOn "\n" |>.head!.trim) + | return {steps, allGoals := allSubGoals} + + let steps := prettifySteps tInfo.stx steps + + let proofTreeEdges ← getGoalsChange ctx tInfo + let currentGoals := proofTreeEdges.map (fun ⟨ _, g₁, gs ⟩ => g₁ :: gs) |>.join + let allGoals := allSubGoals.insertMany $ currentGoals + -- It's like tacticDependsOn but unnamed mvars instead of hyps. + -- Important to sort for have := calc for example, e.g. calc 3 < 4 ... 4 < 5 ... + let orphanedGoals := currentGoals.foldl Std.HashSet.erase (noInEdgeGoals allGoals steps) + |>.toArray.insertionSort (nameNumLt ·.id.name ·.id.name) |>.toList + + let newSteps := proofTreeEdges.filterMap fun ⟨ tacticDependsOn, goalBefore, goalsAfter ⟩ => + -- Leave only steps which are not handled in the subtree. + if steps.map (·.goalBefore) |>.elem goalBefore then + none + else + let range := tInfo.stx.toRange ctx + some { + tacticString, + goalBefore, + goalsAfter, + tacticDependsOn, + spawnedGoals := orphanedGoals, + start := range.start, + finish := range.finish + } + + return { steps := newSteps ++ steps, allGoals } + else + return { steps, allGoals := allSubGoals } + +partial def BetterParser (i : InfoTree) := i.visitM (postNode := postNode) + +end PaperProof From 8bdb5dbf8fcd1222c36e6d5ded93f7a8fdd08a3f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 21 Feb 2025 16:55:28 +0100 Subject: [PATCH 03/47] Allow extraction of only top-level infotrees. --- REPL/Main.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/REPL/Main.lean b/REPL/Main.lean index 2e3d752c..b03ae162 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -232,6 +232,10 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do | some "tactics" => trees.flatMap InfoTree.retainTacticInfo | some "original" => trees.flatMap InfoTree.retainTacticInfo |>.flatMap InfoTree.retainOriginal | some "substantive" => trees.flatMap InfoTree.retainTacticInfo |>.flatMap InfoTree.retainSubstantive + | some "no_children" => trees.map fun t => match t with + | InfoTree.context _ _ => t + | InfoTree.node i _ => InfoTree.node i (PersistentArray.empty) + | InfoTree.hole _ => t | _ => [] let infotree ← if jsonTrees.isEmpty then pure none From 9eaf0e5e814a48a7197849c3f59387ac9279e6c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Mon, 24 Feb 2025 16:20:17 +0100 Subject: [PATCH 04/47] Fix no_children infotree strategy. --- REPL/Main.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index b03ae162..22241497 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -192,6 +192,12 @@ def unpickleProofSnapshot (n : UnpickleProofState) : M IO (ProofStepResponse ⊕ let (proofState, _) ← ProofSnapshot.unpickle n.unpickleProofStateFrom cmdSnapshot? Sum.inl <$> createProofStepReponse proofState +partial def removeChildren (t : InfoTree) : InfoTree := + match t with + | InfoTree.context ctx t' => InfoTree.context ctx (removeChildren t') + | InfoTree.node i _ => InfoTree.node i PersistentArray.empty + | InfoTree.hole _ => t + /-- Run a command, returning the id of the new environment, and any messages and sorries. -/ @@ -232,10 +238,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do | some "tactics" => trees.flatMap InfoTree.retainTacticInfo | some "original" => trees.flatMap InfoTree.retainTacticInfo |>.flatMap InfoTree.retainOriginal | some "substantive" => trees.flatMap InfoTree.retainTacticInfo |>.flatMap InfoTree.retainSubstantive - | some "no_children" => trees.map fun t => match t with - | InfoTree.context _ _ => t - | InfoTree.node i _ => InfoTree.node i (PersistentArray.empty) - | InfoTree.hole _ => t + | some "no_children" => trees.map removeChildren | _ => [] let infotree ← if jsonTrees.isEmpty then pure none From 961e261ec3b16e3deaf1dc9df282c7a75145b660 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Mon, 24 Feb 2025 17:28:20 +0100 Subject: [PATCH 05/47] Fix rw tactic spans computation. --- REPL/PaperProof/BetterParser.lean | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index 10eecd6f..6c5625e9 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -177,22 +177,35 @@ def getGoalsChange (ctx : ContextInfo) (tInfo : TacticInfo) : IO (List (List Str -- TODO: solve rw_mod_cast -def prettifySteps (stx : Syntax) (steps : List ProofStep) : List ProofStep := Id.run do +def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStep) : List ProofStep := Id.run do + let range := stx.toRange ctx let prettify (tStr : String) := let res := tStr.trim.dropRightWhile (· == ',') -- rw puts final rfl on the "]" token if res == "]" then "rfl" else res + -- Each part of rw is a separate step none of them include the initial 'rw [' and final ']'. + -- So we add these to the first and last steps. + let extractRwStep (steps : List ProofStep) : List ProofStep := Id.run do + let rwSteps := steps.map fun a => { a with tacticString := s!"rw [{prettify a.tacticString}]" } + match rwSteps with + | [] => [] + | [step] => [{ step with start := some range.start, finish := some range.finish }] + | steps => + let first := { steps.head! with start := some range.start } + let last := { steps.getLast! with finish := some range.finish } + let middle := steps.drop 1 |>.dropLast + return first :: middle ++ [last] + match stx with | `(tactic| rw [$_,*] $(_)?) | `(tactic| rewrite [$_,*] $(_)?) => - return steps.map fun a => { a with tacticString := s!"rw [{prettify a.tacticString}]" } + return extractRwStep steps | `(tactic| rwa [$_,*] $(_)?) => - let rwSteps := steps.map fun a => { a with tacticString := s!"rw [{prettify a.tacticString}]" } + let rwSteps := extractRwStep steps let assumptionSteps := (if rwSteps.isEmpty then [] else rwSteps.getLast!.goalsAfter).map fun g => { tacticString := "assumption", goalBefore := g, goalsAfter := [], tacticDependsOn := [], spawnedGoals := [], start := none, finish := none } return rwSteps ++ assumptionSteps | _ => return steps - -- Comparator for names, e.g. so that _uniq.34 and _uniq.102 go in the right order. -- That's not completely right because it doesn't compare prefixes but -- it's much shorter to write than correct version and serves the purpose. @@ -216,7 +229,7 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree (·.toString |>.splitOn "\n" |>.head!.trim) | return {steps, allGoals := allSubGoals} - let steps := prettifySteps tInfo.stx steps + let steps := prettifySteps tInfo.stx ctx steps let proofTreeEdges ← getGoalsChange ctx tInfo let currentGoals := proofTreeEdges.map (fun ⟨ _, g₁, gs ⟩ => g₁ :: gs) |>.join From 2b441e2aeb4d908418479f36b5c44954e8276a3d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 27 Feb 2025 14:20:28 +0100 Subject: [PATCH 06/47] Do not truncate tactic strings by the first newline. --- REPL/PaperProof/BetterParser.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index 6c5625e9..7e2ad945 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -225,8 +225,7 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree -- shortcut if it's not a tactic user wrote -- \n trim to avoid empty lines/comments until next tactic, -- especially at the end of theorem it will capture comment for the next one - let some tacticString := tInfo.stx.getSubstring?.map - (·.toString |>.splitOn "\n" |>.head!.trim) + let some tacticString := tInfo.stx.getSubstring?.map (·.toString) | return {steps, allGoals := allSubGoals} let steps := prettifySteps tInfo.stx ctx steps From 016da441b00df60a44a0a766a20309722601c0d3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 28 Feb 2025 15:43:42 +0100 Subject: [PATCH 07/47] Report raw InfoTrees. --- REPL/Lean/InfoTree/ToJson.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/REPL/Lean/InfoTree/ToJson.lean b/REPL/Lean/InfoTree/ToJson.lean index 6e3023c2..c7bc63b8 100644 --- a/REPL/Lean/InfoTree/ToJson.lean +++ b/REPL/Lean/InfoTree/ToJson.lean @@ -24,7 +24,7 @@ deriving ToJson structure Syntax.Json where pp : Option String - -- raw : String + raw : String range : Range deriving ToJson @@ -42,7 +42,7 @@ def _root_.Lean.Syntax.toJson (stx : Syntax) (ctx : ContextInfo) (lctx : LocalCo pp := match (← ctx.ppSyntax lctx stx).pretty with | "failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)" => none | pp => some pp - -- raw := toString stx + raw := toString stx range := stx.toRange ctx } structure TacticInfo.Json where @@ -58,7 +58,7 @@ def TacticInfo.toJson (i : TacticInfo) (ctx : ContextInfo) : IO TacticInfo.Json name := i.name? stx := { pp := Format.pretty (← i.pp ctx), - -- raw := toString i.info.stx, + raw := toString i.stx, range := i.stx.toRange ctx }, goalsBefore := (← i.goalState ctx).map Format.pretty, goalsAfter := (← i.goalStateAfter ctx).map Format.pretty } From 7e9d514dad0385154f40d146c921a7ab460c39a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 7 Mar 2025 13:28:14 +0100 Subject: [PATCH 08/47] Return a shallow infotree for each tactic invocation. --- REPL/PaperProof/BetterParser.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index 7e2ad945..5c1a4a67 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -60,6 +60,7 @@ instance : Hashable GoalInfo where structure ProofStep where tacticString : String + infoTree : Option Json goalBefore : GoalInfo goalsAfter : List GoalInfo tacticDependsOn : List String @@ -203,7 +204,7 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStep) : | `(tactic| rwa [$_,*] $(_)?) => let rwSteps := extractRwStep steps let assumptionSteps := (if rwSteps.isEmpty then [] else rwSteps.getLast!.goalsAfter).map fun g => - { tacticString := "assumption", goalBefore := g, goalsAfter := [], tacticDependsOn := [], spawnedGoals := [], start := none, finish := none } + { tacticString := "assumption", infoTree := none, goalBefore := g, goalsAfter := [], tacticDependsOn := [], spawnedGoals := [], start := none, finish := none } return rwSteps ++ assumptionSteps | _ => return steps -- Comparator for names, e.g. so that _uniq.34 and _uniq.102 go in the right order. @@ -228,6 +229,8 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree let some tacticString := tInfo.stx.getSubstring?.map (·.toString) | return {steps, allGoals := allSubGoals} + let infoTreeJson ← (InfoTree.node i PersistentArray.empty).toJson ctx + let steps := prettifySteps tInfo.stx ctx steps let proofTreeEdges ← getGoalsChange ctx tInfo @@ -251,7 +254,8 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree tacticDependsOn, spawnedGoals := orphanedGoals, start := range.start, - finish := range.finish + finish := range.finish, + infoTree := some infoTreeJson } return { steps := newSteps ++ steps, allGoals } From 0ddcb1cd7a9905572a256563defaa8056b1c73a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 7 Mar 2025 16:43:07 +0100 Subject: [PATCH 09/47] Report `at` clauses in `rw` tactics. --- REPL/PaperProof/BetterParser.lean | 37 ++++++++++++++++++++++--------- 1 file changed, 26 insertions(+), 11 deletions(-) diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index 5c1a4a67..dd833e57 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -178,19 +178,34 @@ def getGoalsChange (ctx : ContextInfo) (tInfo : TacticInfo) : IO (List (List Str -- TODO: solve rw_mod_cast -def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStep) : List ProofStep := Id.run do +def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStep) : IO (List ProofStep) := do let range := stx.toRange ctx let prettify (tStr : String) := let res := tStr.trim.dropRightWhile (· == ',') -- rw puts final rfl on the "]" token + -- TODO: is this correct for `rewrite`? if res == "]" then "rfl" else res -- Each part of rw is a separate step none of them include the initial 'rw [' and final ']'. -- So we add these to the first and last steps. - let extractRwStep (steps : List ProofStep) : List ProofStep := Id.run do - let rwSteps := steps.map fun a => { a with tacticString := s!"rw [{prettify a.tacticString}]" } + let extractRwStep (steps : List ProofStep) (atClause? : Option Syntax) : IO (List ProofStep) := do + -- If atClause is present, call toJson on it and retrieve the `pp` field. + let atClauseStr? ← match atClause? with + | some atClause => do + let j ← atClause.toJson ctx (LocalContext.mkEmpty ()) + pure j.pp + | none => + pure none + + -- Turn the `Option String` into a (possibly-empty) string so we can insert it. + let maybeAtClause := atClauseStr?.getD "" -- getD "" returns `""` if `atClauseStr?` is `none` + let rwSteps := steps.map fun a => + { a with tacticString := s!"rw [{prettify a.tacticString}]{maybeAtClause}" } + match rwSteps with - | [] => [] - | [step] => [{ step with start := some range.start, finish := some range.finish }] + | [] => + return [] + | [step] => + return [{ step with start := some range.start, finish := some range.finish }] | steps => let first := { steps.head! with start := some range.start } let last := { steps.getLast! with finish := some range.finish } @@ -198,11 +213,11 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStep) : return first :: middle ++ [last] match stx with - | `(tactic| rw [$_,*] $(_)?) - | `(tactic| rewrite [$_,*] $(_)?) => - return extractRwStep steps - | `(tactic| rwa [$_,*] $(_)?) => - let rwSteps := extractRwStep steps + | `(tactic| rw [$_,*] $(at_clause)?) + | `(tactic| rewrite [$_,*] $(at_clause)?) => + extractRwStep steps at_clause + | `(tactic| rwa [$_,*] $(at_clause)?) => + let rwSteps ← extractRwStep steps at_clause let assumptionSteps := (if rwSteps.isEmpty then [] else rwSteps.getLast!.goalsAfter).map fun g => { tacticString := "assumption", infoTree := none, goalBefore := g, goalsAfter := [], tacticDependsOn := [], spawnedGoals := [], start := none, finish := none } return rwSteps ++ assumptionSteps @@ -231,7 +246,7 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree let infoTreeJson ← (InfoTree.node i PersistentArray.empty).toJson ctx - let steps := prettifySteps tInfo.stx ctx steps + let steps ← prettifySteps tInfo.stx ctx steps let proofTreeEdges ← getGoalsChange ctx tInfo let currentGoals := proofTreeEdges.map (fun ⟨ _, g₁, gs ⟩ => g₁ :: gs) |>.join From 30aa12220f80174c2fb982ca4a718b88a0c4638f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Tue, 1 Apr 2025 18:45:55 +0200 Subject: [PATCH 10/47] Report metavariable context in each ProofStep. --- REPL/PaperProof/BetterParser.lean | 40 ++++++++++++++++++++++++++++++- 1 file changed, 39 insertions(+), 1 deletion(-) diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index dd833e57..ccb9f6b3 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -58,11 +58,33 @@ instance : BEq GoalInfo where instance : Hashable GoalInfo where hash g := hash g.id +structure MetavarDecl.Json where + mvarId : String + userName : String + type : String +deriving ToJson, FromJson + +structure MetavarContext.Json where + decls : Array MetavarDecl.Json +deriving ToJson, FromJson + +def MetavarContext.toJson (mctx : MetavarContext) (ctx : ContextInfo) : IO MetavarContext.Json := do + let mut decls := #[] + for (mvarId, decl) in mctx.decls do + decls := decls.push { + mvarId := toString mvarId.name + userName := toString decl.userName + type := (← ctx.ppExpr {} decl.type).pretty + } + return { decls } + structure ProofStep where tacticString : String infoTree : Option Json goalBefore : GoalInfo goalsAfter : List GoalInfo + mctxBefore : Option MetavarContext.Json + mctxAfter : Option MetavarContext.Json tacticDependsOn : List String spawnedGoals : List GoalInfo start : Option Lean.Position @@ -219,7 +241,18 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStep) : | `(tactic| rwa [$_,*] $(at_clause)?) => let rwSteps ← extractRwStep steps at_clause let assumptionSteps := (if rwSteps.isEmpty then [] else rwSteps.getLast!.goalsAfter).map fun g => - { tacticString := "assumption", infoTree := none, goalBefore := g, goalsAfter := [], tacticDependsOn := [], spawnedGoals := [], start := none, finish := none } + { + tacticString := "assumption", + infoTree := none, + goalBefore := g, + goalsAfter := [], + mctxBefore := none, + mctxAfter := none, + tacticDependsOn := [], + spawnedGoals := [], + start := none, + finish := none + } return rwSteps ++ assumptionSteps | _ => return steps -- Comparator for names, e.g. so that _uniq.34 and _uniq.102 go in the right order. @@ -256,6 +289,9 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree let orphanedGoals := currentGoals.foldl Std.HashSet.erase (noInEdgeGoals allGoals steps) |>.toArray.insertionSort (nameNumLt ·.id.name ·.id.name) |>.toList + let mctxBeforeJson ← MetavarContext.toJson tInfo.mctxBefore ctx + let mctxAfterJson ← MetavarContext.toJson tInfo.mctxAfter ctx + let newSteps := proofTreeEdges.filterMap fun ⟨ tacticDependsOn, goalBefore, goalsAfter ⟩ => -- Leave only steps which are not handled in the subtree. if steps.map (·.goalBefore) |>.elem goalBefore then @@ -266,6 +302,8 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree tacticString, goalBefore, goalsAfter, + mctxBefore := mctxBeforeJson, + mctxAfter := mctxAfterJson, tacticDependsOn, spawnedGoals := orphanedGoals, start := range.start, From 82c1a33c5942f469106f2520cadd2616d55120ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Wed, 2 Apr 2025 15:39:35 +0200 Subject: [PATCH 11/47] Report metavariable context (including assignment dependencies) and structured info about goals. --- REPL/JSON.lean | 103 +++++++++++++++++++++++++++++- REPL/Main.lean | 16 +++-- REPL/PaperProof/BetterParser.lean | 100 +++-------------------------- 3 files changed, 120 insertions(+), 99 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 7a3260f4..6c0eaacf 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -6,7 +6,9 @@ Authors: Scott Morrison import Lean.Data.Json import Lean.Message import Lean.Elab.InfoTree.Main -import REPL.PaperProof.BetterParser +import Lean.Meta.Basic +import Lean.Meta.CollectMVars +import REPL.Lean.InfoTree.ToJson open Lean Elab InfoTree @@ -117,6 +119,97 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : proofState, usedConstants } +structure Hypothesis where + username : String + type : String + value : Option String + -- unique identifier for the hypothesis, fvarId + id : String + isProof : String + deriving Inhabited, ToJson, FromJson + +structure GoalInfo where + username : String + type : String + hyps : List Hypothesis + -- unique identifier for the goal, mvarId + id : MVarId + deriving Inhabited, ToJson, FromJson + +private def mayBeProof (expr : Expr) : MetaM String := do + let type : Expr ← Lean.Meta.inferType expr + if ← Meta.isProof expr then + return "proof" + if type.isSort then + return "universe" + else + return "data" + +def printGoalInfo (printCtx : ContextInfo) (id : MVarId) : IO GoalInfo := do + let some decl := printCtx.mctx.findDecl? id + | panic! "printGoalInfo: goal not found in the mctx" + -- to get tombstones in name ✝ for unreachable hypothesis + let lctx := decl.lctx |>.sanitizeNames.run' {options := {}} + let ppContext := printCtx.toPPContext lctx + + let hyps ← lctx.foldrM (init := []) (fun hypDecl acc => do + if hypDecl.isAuxDecl || hypDecl.isImplementationDetail then + return acc + + let type ← liftM (ppExprWithInfos ppContext hypDecl.type) + let value ← liftM (hypDecl.value?.mapM (ppExprWithInfos ppContext)) + let isProof : String ← printCtx.runMetaM decl.lctx (mayBeProof hypDecl.toExpr) + return ({ + username := hypDecl.userName.toString, + type := type.fmt.pretty, + value := value.map (·.fmt.pretty), + id := hypDecl.fvarId.name.toString, + isProof := isProof, + } : Hypothesis) :: acc) + return ⟨ decl.userName.toString, (← ppExprWithInfos ppContext decl.type).fmt.pretty, hyps, id⟩ + + +instance : BEq GoalInfo where + beq g1 g2 := g1.id == g2.id + +instance : Hashable GoalInfo where + hash g := hash g.id +structure MetavarDecl.Json where + mvarId : String + userName : String + type : String + mvarsInType : List MVarId +deriving ToJson, FromJson + +structure MetavarContext.Json where + decls : Array MetavarDecl.Json +deriving ToJson, FromJson + +def MetavarContext.toJson (mctx : MetavarContext) (ctx : ContextInfo) : IO MetavarContext.Json := do + let mut decls := #[] + for (mvarId, decl) in mctx.decls do + let (_, typeMVars) ← ctx.runMetaM decl.lctx ((Meta.collectMVars decl.type).run {}) + decls := decls.push { + mvarId := toString mvarId.name + userName := toString decl.userName + type := (← ctx.ppExpr {} decl.type).pretty + mvarsInType := typeMVars.result.toList + } + return { decls } + +structure ProofStepInfo where + tacticString : String + infoTree : Option Json + goalBefore : GoalInfo + goalsAfter : List GoalInfo + mctxBefore : Option MetavarContext.Json + mctxAfter : Option MetavarContext.Json + tacticDependsOn : List String + spawnedGoals : List GoalInfo + start : Option Lean.Position + finish : Option Lean.Position + deriving Inhabited, ToJson, FromJson + /-- A response to a Lean command. `env` can be used in later calls, to build on the stored environment. @@ -127,7 +220,7 @@ structure CommandResponse where sorries : List Sorry := [] tactics : List Tactic := [] infotree : Option Json := none - proofTreeEdges : Option (List (List PaperProof.ProofStep)) := none + proofTreeEdges : Option (List (List ProofStepInfo)) := none deriving FromJson def Json.nonemptyList [ToJson α] (k : String) : List α → List (String × Json) @@ -156,6 +249,8 @@ structure ProofStepResponse where messages : List Message := [] sorries : List Sorry := [] traces : List String + goalInfos: List GoalInfo := [] + mctxAfter : Option MetavarContext.Json deriving ToJson, FromJson instance : ToJson ProofStepResponse where @@ -164,7 +259,9 @@ instance : ToJson ProofStepResponse where [("goals", toJson r.goals)], Json.nonemptyList "messages" r.messages, Json.nonemptyList "sorries" r.sorries, - Json.nonemptyList "traces" r.traces + Json.nonemptyList "traces" r.traces, + Json.nonemptyList "goalInfos" r.goalInfos, + match r.mctxAfter with | some mctxAfter => [("mctxAfter", toJson mctxAfter)] | none => [] ] /-- Json wrapper for an error. -/ diff --git a/REPL/Main.lean b/REPL/Main.lean index 22241497..37a15def 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -126,7 +126,7 @@ def tactics (trees : List InfoTree) : M m (List Tactic) := let proofStateId ← proofState.mapM recordProofSnapshot return Tactic.of goals tactic pos endPos proofStateId ns -def proofTrees (infoTrees : List InfoTree) : M m (List (List PaperProof.ProofStep)) := do +def proofTrees (infoTrees : List InfoTree) : M m (List (List ProofStepInfo)) := do infoTrees.mapM fun infoTree => do let proofTree ← PaperProof.BetterParser infoTree match proofTree with @@ -149,13 +149,21 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap -- For debugging purposes, sometimes we print out the trees here: -- trees.forM fun t => do IO.println (← t.format) let sorries ← sorries trees none - let id ← recordProofSnapshot proofState + let proofStateId ← recordProofSnapshot proofState + let (ctx, _) ← proofState.runMetaM do return { ← CommandContextInfo.save with } + let goalInfos ← proofState.tacticState.goals.mapM (fun mvarId => do + let goalInfo ← printGoalInfo ctx mvarId + return goalInfo) + let mctxAfterJson ← MetavarContext.toJson proofState.metaState.mctx ctx return { - proofState := id + proofState := proofStateId goals := (← proofState.ppGoals).map fun s => s!"{s}" messages sorries - traces } + traces + goalInfos + mctxAfter := mctxAfterJson + } /-- Pickle a `CommandSnapshot`, generating a JSON response. -/ def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Error) := do diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index ccb9f6b3..536669a6 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -30,70 +30,15 @@ import Lean import Lean.Meta.Basic import Lean.Meta.CollectMVars import REPL.Lean.InfoTree.ToJson +import REPL.JSON -open Lean Elab Server +open Lean Elab Server REPL namespace PaperProof -structure Hypothesis where - username : String - type : String - value : Option String - -- unique identifier for the hypothesis, fvarId - id : String - isProof : String - deriving Inhabited, ToJson, FromJson - -structure GoalInfo where - username : String - type : String - hyps : List Hypothesis - -- unique identifier for the goal, mvarId - id : MVarId - deriving Inhabited, ToJson, FromJson - -instance : BEq GoalInfo where - beq g1 g2 := g1.id == g2.id - -instance : Hashable GoalInfo where - hash g := hash g.id - -structure MetavarDecl.Json where - mvarId : String - userName : String - type : String -deriving ToJson, FromJson - -structure MetavarContext.Json where - decls : Array MetavarDecl.Json -deriving ToJson, FromJson - -def MetavarContext.toJson (mctx : MetavarContext) (ctx : ContextInfo) : IO MetavarContext.Json := do - let mut decls := #[] - for (mvarId, decl) in mctx.decls do - decls := decls.push { - mvarId := toString mvarId.name - userName := toString decl.userName - type := (← ctx.ppExpr {} decl.type).pretty - } - return { decls } - -structure ProofStep where - tacticString : String - infoTree : Option Json - goalBefore : GoalInfo - goalsAfter : List GoalInfo - mctxBefore : Option MetavarContext.Json - mctxAfter : Option MetavarContext.Json - tacticDependsOn : List String - spawnedGoals : List GoalInfo - start : Option Lean.Position - finish : Option Lean.Position - deriving Inhabited, ToJson, FromJson - -def stepGoalsAfter (step : ProofStep) : List GoalInfo := step.goalsAfter ++ step.spawnedGoals - -def noInEdgeGoals (allGoals : Std.HashSet GoalInfo) (steps : List ProofStep) : Std.HashSet GoalInfo := +def stepGoalsAfter (step : ProofStepInfo) : List GoalInfo := step.goalsAfter ++ step.spawnedGoals + +def noInEdgeGoals (allGoals : Std.HashSet GoalInfo) (steps : List ProofStepInfo) : Std.HashSet GoalInfo := -- Some of the orphaned goals might be matched by tactics in sibling subtrees, e.g. for tacticSeq. (steps.bind stepGoalsAfter).foldl Std.HashSet.erase allGoals @@ -123,35 +68,6 @@ def findMVarsAssigned (goalId : MVarId) (mctxAfter : MetavarContext) : MetaM (Li let (_, s) ← (Meta.collectMVars expr).run {} return s.result.toList -def mayBeProof (expr : Expr) : MetaM String := do - let type : Expr ← Lean.Meta.inferType expr - if ← Meta.isProof expr then - return "proof" - if type.isSort then - return "universe" - else - return "data" - -def printGoalInfo (printCtx : ContextInfo) (id : MVarId) : IO GoalInfo := do - let some decl := printCtx.mctx.findDecl? id - | panic! "printGoalInfo: goal not found in the mctx" - -- to get tombstones in name ✝ for unreachable hypothesis - let lctx := decl.lctx |>.sanitizeNames.run' {options := {}} - let ppContext := printCtx.toPPContext lctx - let hyps ← lctx.foldrM (init := []) (fun hypDecl acc => do - if hypDecl.isAuxDecl || hypDecl.isImplementationDetail then - return acc - let type ← liftM (ppExprWithInfos ppContext hypDecl.type) - let value ← liftM (hypDecl.value?.mapM (ppExprWithInfos ppContext)) - let isProof : String ← printCtx.runMetaM decl.lctx (mayBeProof hypDecl.toExpr) - return ({ - username := hypDecl.userName.toString, - type := type.fmt.pretty, - value := value.map (·.fmt.pretty), - id := hypDecl.fvarId.name.toString, - isProof := isProof - } : Hypothesis) :: acc) - return ⟨ decl.userName.toString, (← ppExprWithInfos ppContext decl.type).fmt.pretty, hyps, id⟩ -- Returns unassigned goals from the provided list of goals def getUnassignedGoals (goals : List MVarId) (mctx : MetavarContext) : IO (List MVarId) := do @@ -164,7 +80,7 @@ def getUnassignedGoals (goals : List MVarId) (mctx : MetavarContext) : IO (List return some id structure Result where - steps : List ProofStep + steps : List ProofStepInfo allGoals : Std.HashSet GoalInfo def getGoalsChange (ctx : ContextInfo) (tInfo : TacticInfo) : IO (List (List String × GoalInfo × List GoalInfo)) := do @@ -200,7 +116,7 @@ def getGoalsChange (ctx : ContextInfo) (tInfo : TacticInfo) : IO (List (List Str -- TODO: solve rw_mod_cast -def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStep) : IO (List ProofStep) := do +def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo) : IO (List ProofStepInfo) := do let range := stx.toRange ctx let prettify (tStr : String) := let res := tStr.trim.dropRightWhile (· == ',') @@ -209,7 +125,7 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStep) : if res == "]" then "rfl" else res -- Each part of rw is a separate step none of them include the initial 'rw [' and final ']'. -- So we add these to the first and last steps. - let extractRwStep (steps : List ProofStep) (atClause? : Option Syntax) : IO (List ProofStep) := do + let extractRwStep (steps : List ProofStepInfo) (atClause? : Option Syntax) : IO (List ProofStepInfo) := do -- If atClause is present, call toJson on it and retrieve the `pp` field. let atClauseStr? ← match atClause? with | some atClause => do From 835f383d2f34847dfa5c8a1bfb302fe5794d1025 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 3 Apr 2025 17:21:03 +0200 Subject: [PATCH 12/47] Report goalInfo in sorries. --- REPL/JSON.lean | 43 ++++++++++++++++++++++++------------------- REPL/Main.lean | 10 +++++++++- 2 files changed, 33 insertions(+), 20 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 6c0eaacf..0c22e915 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -74,11 +74,29 @@ def Message.of (m : Lean.Message) : IO Message := do pure <| | .error => .error, data := (← m.data.toString).trim } +structure HypothesisInfo where + username : String + type : String + value : Option String + -- unique identifier for the hypothesis, fvarId + id : String + isProof : String + deriving Inhabited, ToJson, FromJson + +structure GoalInfo where + username : String + type : String + hyps : List HypothesisInfo + -- unique identifier for the goal, mvarId + id : MVarId + deriving Inhabited, ToJson, FromJson + /-- A Lean `sorry`. -/ structure Sorry where pos : Pos endPos : Pos goal : String + goalInfo: Option GoalInfo /-- The index of the proof state at the sorry. You can use the `ProofStep` instruction to run a tactic at this state. @@ -89,16 +107,20 @@ deriving FromJson instance : ToJson Sorry where toJson r := Json.mkObj <| .flatten [ [("goal", r.goal)], + match r.goalInfo with + | some goalInfo => [("goalInfo", toJson goalInfo)] + | none => [], [("proofState", toJson r.proofState)], if r.pos.line ≠ 0 then [("pos", toJson r.pos)] else [], if r.endPos.line ≠ 0 then [("endPos", toJson r.endPos)] else [], ] /-- Construct the JSON representation of a Lean sorry. -/ -def Sorry.of (goal : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry := +def Sorry.of (goal : String) (goalInfo : Option GoalInfo) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry := { pos := ⟨pos.line, pos.column⟩, endPos := ⟨endPos.line, endPos.column⟩, goal, + goalInfo, proofState } structure Tactic where @@ -119,23 +141,6 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : proofState, usedConstants } -structure Hypothesis where - username : String - type : String - value : Option String - -- unique identifier for the hypothesis, fvarId - id : String - isProof : String - deriving Inhabited, ToJson, FromJson - -structure GoalInfo where - username : String - type : String - hyps : List Hypothesis - -- unique identifier for the goal, mvarId - id : MVarId - deriving Inhabited, ToJson, FromJson - private def mayBeProof (expr : Expr) : MetaM String := do let type : Expr ← Lean.Meta.inferType expr if ← Meta.isProof expr then @@ -165,7 +170,7 @@ def printGoalInfo (printCtx : ContextInfo) (id : MVarId) : IO GoalInfo := do value := value.map (·.fmt.pretty), id := hypDecl.fvarId.name.toString, isProof := isProof, - } : Hypothesis) :: acc) + } : HypothesisInfo) :: acc) return ⟨ decl.userName.toString, (← ppExprWithInfos ppContext decl.type).fmt.pretty, hyps, id⟩ diff --git a/REPL/Main.lean b/REPL/Main.lean index 38e50b26..97edbc12 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -109,7 +109,15 @@ def sorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorr pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) | .term _ none => unreachable! let proofStateId ← proofState.mapM recordProofSnapshot - return Sorry.of goal pos endPos proofStateId + let goalInfo : Option GoalInfo ← match proofState with + | some proofState => do + match proofState.tacticState.goals[0]? with + | some goalId => do + let info ← printGoalInfo ctx goalId + pure (some info) + | none => pure none + | none => pure none + return Sorry.of goal goalInfo pos endPos proofStateId def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := ctx.runMetaM {} try From 4161e2b3866fc0bd64461342c0de3f80882d145d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 4 Apr 2025 09:59:28 +0200 Subject: [PATCH 13/47] Fix: return goalInfos even when empty. --- REPL/JSON.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 0c22e915..8f11d0de 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -262,10 +262,10 @@ instance : ToJson ProofStepResponse where toJson r := Json.mkObj <| .flatten [ [("proofState", r.proofState)], [("goals", toJson r.goals)], + [("goalInfos", toJson r.goalInfos)], Json.nonemptyList "messages" r.messages, Json.nonemptyList "sorries" r.sorries, Json.nonemptyList "traces" r.traces, - Json.nonemptyList "goalInfos" r.goalInfos, match r.mctxAfter with | some mctxAfter => [("mctxAfter", toJson mctxAfter)] | none => [] ] From 6d9d79516b5a6e516b0d7d1fbed8eeed2092fbca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Wed, 9 Apr 2025 18:43:29 +0200 Subject: [PATCH 14/47] Add TODO. --- REPL/Main.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/REPL/Main.lean b/REPL/Main.lean index 97edbc12..d5487205 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -113,6 +113,7 @@ def sorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorr | some proofState => do match proofState.tacticState.goals[0]? with | some goalId => do + -- TODO: this does not work when it's just `sorry` instead of `by sorry` let info ← printGoalInfo ctx goalId pure (some info) | none => pure none From 1a8f085749533b0d4dd10446a8ecbc9412494aa9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 10 Apr 2025 19:08:26 +0200 Subject: [PATCH 15/47] Make `pf.hasSorry` the last check so that it can be safely ignored. --- REPL/Main.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index e279cc2d..210e4d8d 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -171,8 +171,6 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do | some pf => do let pf ← instantiateMVars pf let pft ← Meta.inferType pf >>= instantiateMVars - if pf.hasSorry then - return "Incomplete: contains sorry" if pf.hasExprMVar then return "Incomplete: contains metavariable(s)" @@ -189,6 +187,10 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do let _ ← addDecl decl catch ex => return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + + if pf.hasSorry then + return "Incomplete: contains sorry" + return "Completed" | _ => return "Not verified: more than one initial goal" From 6b3329ae0b22b98d24cde65ae10c85e80aaace1d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 11 Apr 2025 09:49:48 +0200 Subject: [PATCH 16/47] Revert "Make `pf.hasSorry` the last check so that it can be safely ignored." This reverts commit 1a8f085749533b0d4dd10446a8ecbc9412494aa9. --- REPL/Main.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 210e4d8d..e279cc2d 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -171,6 +171,8 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do | some pf => do let pf ← instantiateMVars pf let pft ← Meta.inferType pf >>= instantiateMVars + if pf.hasSorry then + return "Incomplete: contains sorry" if pf.hasExprMVar then return "Incomplete: contains metavariable(s)" @@ -187,10 +189,6 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do let _ ← addDecl decl catch ex => return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" - - if pf.hasSorry then - return "Incomplete: contains sorry" - return "Completed" | _ => return "Not verified: more than one initial goal" From d1995df431db7ad3be90b724dfea01febe60f978 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Wed, 16 Apr 2025 13:06:16 +0200 Subject: [PATCH 17/47] Proof step verification using kernel. --- REPL/JSON.lean | 4 ++- REPL/Main.lean | 98 +++++++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 100 insertions(+), 2 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index ef8271aa..bc52caae 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -258,6 +258,7 @@ structure ProofStepResponse where goalInfos: List GoalInfo := [] mctxAfter : Option MetavarContext.Json proofStatus : String + stepVerification : String deriving ToJson, FromJson instance : ToJson ProofStepResponse where @@ -269,7 +270,8 @@ instance : ToJson ProofStepResponse where Json.nonemptyList "sorries" r.sorries, Json.nonemptyList "traces" r.traces, match r.mctxAfter with | some mctxAfter => [("mctxAfter", toJson mctxAfter)] | none => [], - [("proofStatus", r.proofStatus)] + [("proofStatus", r.proofStatus)], + [("stepVerification", r.stepVerification)] ] /-- Json wrapper for an error. -/ diff --git a/REPL/Main.lean b/REPL/Main.lean index e5e9be95..304c9a72 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -246,6 +246,101 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do | _ => return "Incomplete: open goals remain" +/-- +Returns a list of pairs of metavariables and their assignments from a proof state. +Each pair contains the MVarId and its assigned Expr. +-/ +def getAssignedMVars (proofState : ProofSnapshot) : M m (List (MVarId × Expr)) := do + let (assignments, _) ← proofState.runMetaM do + let mut assignments := [] + for goalId in proofState.tacticState.goals do + match proofState.metaState.mctx.getExprAssignmentCore? goalId with + | none => continue + | some pf => do + let pf ← instantiateMVars pf + assignments := (goalId, pf) :: assignments + return assignments + return assignments + +/-- +Returns a list of newly assigned metavariables and their expressions, +comparing the current proof state with an optional old proof state. +If no old state is provided, returns all assigned MVars. +Returns assignments from both states, preferring new assignments in case of conflicts. +-/ +def getNewlyAssignedMVars (proofState : ProofSnapshot) (oldProofState? : Option ProofSnapshot := none) : + M m (List (MVarId × Expr)) := do + let newAssignments ← getAssignedMVars proofState + match oldProofState? with + | none => return newAssignments + | some oldState => do + let oldAssignments ← getAssignedMVars oldState + -- Get all assignments from both states, preferring new assignments + let mut result := [] + -- First add all new assignments + for assignment in newAssignments do + result := assignment :: result + -- Then add old assignments that don't have a corresponding new one + for (mvarId, expr) in oldAssignments do + if !newAssignments.any (·.1 == mvarId) then + result := (mvarId, expr) :: result + + return result + +/-- +Verifies that all assigned goals in the proof state have valid assignments that type check. +Returns either "OK" or an error message describing the first failing goal. +-/ +def verifyGoalAssignment (proofState : ProofSnapshot) (oldProofState? : Option ProofSnapshot := none) : + M m String := do + let mut allOk := true + let mut errorMsg := "" + + let assignments ← getNewlyAssignedMVars proofState oldProofState? + -- Print assignments for debugging + -- IO.println s!"Number of assignments: {assignments.length}" + -- for (goalId, pf) in assignments do + -- IO.println s!"Goal {goalId.name} := {pf}" + for (goalId, pf) in assignments do + let (res, _) ← proofState.runMetaM do + -- Check that proof has expected type + let pft ← Meta.inferType pf >>= instantiateMVars + let expectedType ← Meta.inferType (mkMVar goalId) >>= instantiateMVars + unless (← Meta.isDefEq pft expectedType) do + return s!"Error: proof has type {pft} but goal has type {expectedType}" + + let pf ← goalId.withContext $ abstractAllLambdaFVars pf + let pft ← Meta.inferType pf >>= instantiateMVars + + if pf.hasExprMVar then + return "Error: contains metavariable(s)" + + -- Find level parameters + let usedLevels := collectLevelParams {} pft + let usedLevels := collectLevelParams usedLevels pf + + let decl := Declaration.defnDecl { + name := Name.anonymous, + type := pft, + value := pf, + levelParams := usedLevels.params.toList, + hints := ReducibilityHints.opaque, + safety := DefinitionSafety.safe + } + + try + let _ ← addDecl decl + return "OK" + catch ex => + return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + + if res != "OK" then + allOk := false + errorMsg := res + break + + return if allOk then "OK" else errorMsg + /-- Record a `ProofSnapshot` and generate a JSON response for it. -/ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnapshot := none) : M m ProofStepResponse := do @@ -276,7 +371,8 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap traces goalInfos mctxAfter := mctxAfterJson - proofStatus := (← getProofStatus proofState) } + proofStatus := (← getProofStatus proofState) + stepVerification := (← verifyGoalAssignment proofState old?) } /-- Pickle a `CommandSnapshot`, generating a JSON response. -/ def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Error) := do From b9c90bf59e03e938ecb7b0dc836815b148fac0ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Wed, 16 Apr 2025 14:34:51 +0200 Subject: [PATCH 18/47] Proof step verification using kernel. #2 --- REPL/Main.lean | 42 +++++++++++++----------------------------- 1 file changed, 13 insertions(+), 29 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 304c9a72..553bb86f 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -247,13 +247,22 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do | _ => return "Incomplete: open goals remain" /-- -Returns a list of pairs of metavariables and their assignments from a proof state. -Each pair contains the MVarId and its assigned Expr. +Returns a list of newly assigned metavariables and their expressions, +comparing the current proof state with an optional old proof state. +If no old state is provided, returns all assigned MVars. -/ -def getAssignedMVars (proofState : ProofSnapshot) : M m (List (MVarId × Expr)) := do +def getNewlyAssignedMVars (proofState : ProofSnapshot) (oldProofState? : Option ProofSnapshot := none) : + M m (List (MVarId × Expr)) := do + -- Get all goals from both states + let allGoals := match oldProofState? with + | none => proofState.tacticState.goals + | some oldState => + (proofState.tacticState.goals ++ oldState.tacticState.goals).eraseDups + + -- Check which have assignments in new state let (assignments, _) ← proofState.runMetaM do let mut assignments := [] - for goalId in proofState.tacticState.goals do + for goalId in allGoals do match proofState.metaState.mctx.getExprAssignmentCore? goalId with | none => continue | some pf => do @@ -262,31 +271,6 @@ def getAssignedMVars (proofState : ProofSnapshot) : M m (List (MVarId × Expr)) return assignments return assignments -/-- -Returns a list of newly assigned metavariables and their expressions, -comparing the current proof state with an optional old proof state. -If no old state is provided, returns all assigned MVars. -Returns assignments from both states, preferring new assignments in case of conflicts. --/ -def getNewlyAssignedMVars (proofState : ProofSnapshot) (oldProofState? : Option ProofSnapshot := none) : - M m (List (MVarId × Expr)) := do - let newAssignments ← getAssignedMVars proofState - match oldProofState? with - | none => return newAssignments - | some oldState => do - let oldAssignments ← getAssignedMVars oldState - -- Get all assignments from both states, preferring new assignments - let mut result := [] - -- First add all new assignments - for assignment in newAssignments do - result := assignment :: result - -- Then add old assignments that don't have a corresponding new one - for (mvarId, expr) in oldAssignments do - if !newAssignments.any (·.1 == mvarId) then - result := (mvarId, expr) :: result - - return result - /-- Verifies that all assigned goals in the proof state have valid assignments that type check. Returns either "OK" or an error message describing the first failing goal. From c42b68df259850320879d2b673ab11eb3bd3b2ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Wed, 16 Apr 2025 15:49:27 +0200 Subject: [PATCH 19/47] Proof step verification using kernel. #3 --- REPL/Main.lean | 139 +++++++++++++++++++++++-------------------------- 1 file changed, 64 insertions(+), 75 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 553bb86f..e79fceb0 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -247,83 +247,72 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do | _ => return "Incomplete: open goals remain" /-- -Returns a list of newly assigned metavariables and their expressions, -comparing the current proof state with an optional old proof state. -If no old state is provided, returns all assigned MVars. --/ -def getNewlyAssignedMVars (proofState : ProofSnapshot) (oldProofState? : Option ProofSnapshot := none) : - M m (List (MVarId × Expr)) := do - -- Get all goals from both states - let allGoals := match oldProofState? with - | none => proofState.tacticState.goals - | some oldState => - (proofState.tacticState.goals ++ oldState.tacticState.goals).eraseDups - - -- Check which have assignments in new state - let (assignments, _) ← proofState.runMetaM do - let mut assignments := [] - for goalId in allGoals do - match proofState.metaState.mctx.getExprAssignmentCore? goalId with - | none => continue - | some pf => do - let pf ← instantiateMVars pf - assignments := (goalId, pf) :: assignments - return assignments - return assignments - -/-- -Verifies that all assigned goals in the proof state have valid assignments that type check. +Verifies that all goals from the old state are properly handled in the new state. Returns either "OK" or an error message describing the first failing goal. -/ -def verifyGoalAssignment (proofState : ProofSnapshot) (oldProofState? : Option ProofSnapshot := none) : +def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldProofState? : Option ProofSnapshot := none) : M m String := do - let mut allOk := true - let mut errorMsg := "" - - let assignments ← getNewlyAssignedMVars proofState oldProofState? - -- Print assignments for debugging - -- IO.println s!"Number of assignments: {assignments.length}" - -- for (goalId, pf) in assignments do - -- IO.println s!"Goal {goalId.name} := {pf}" - for (goalId, pf) in assignments do - let (res, _) ← proofState.runMetaM do - -- Check that proof has expected type - let pft ← Meta.inferType pf >>= instantiateMVars - let expectedType ← Meta.inferType (mkMVar goalId) >>= instantiateMVars - unless (← Meta.isDefEq pft expectedType) do - return s!"Error: proof has type {pft} but goal has type {expectedType}" - - let pf ← goalId.withContext $ abstractAllLambdaFVars pf - let pft ← Meta.inferType pf >>= instantiateMVars - - if pf.hasExprMVar then - return "Error: contains metavariable(s)" - - -- Find level parameters - let usedLevels := collectLevelParams {} pft - let usedLevels := collectLevelParams usedLevels pf - - let decl := Declaration.defnDecl { - name := Name.anonymous, - type := pft, - value := pf, - levelParams := usedLevels.params.toList, - hints := ReducibilityHints.opaque, - safety := DefinitionSafety.safe - } - - try - let _ ← addDecl decl - return "OK" - catch ex => - return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" - - if res != "OK" then - allOk := false - errorMsg := res - break - - return if allOk then "OK" else errorMsg + match oldProofState? with + | none => return "OK" -- Nothing to verify + | some oldState => do + let mut allOk := true + let mut errorMsg := "" + + for oldGoal in oldState.tacticState.goals do + -- If the goal is still present in the new proofState, we don't need to verify it yet. + if proofState.tacticState.goals.contains oldGoal then + continue + + let (res, _) ← proofState.runMetaM do + -- Check if goal is assigned in new state + match proofState.metaState.mctx.getExprAssignmentCore? oldGoal with + | none => return s!"Goal {oldGoal.name} was not solved" + | some pf => do + let pf ← instantiateMVars pf + + -- Check that all MVars in the proof are goals in new state + -- let mvars ← Meta.getMVars pf + let (_, mvars) ← ctx.runMetaM proofState.metaContext.lctx ((Meta.collectMVars pf).run {}) + IO.println s!"Goal {oldGoal.name} = {pf} ({mvars.result.map (·.name)})" + for mvar in mvars.result do + -- If the metavariable in the assignment is a new goal, it's fine. + unless proofState.tacticState.goals.contains mvar do + return s!"Goal {oldGoal.name} assignment contains metavariables" + + -- Check that proof has expected type + let pft ← Meta.inferType pf >>= instantiateMVars + let expectedType ← Meta.inferType (mkMVar oldGoal) >>= instantiateMVars + unless (← Meta.isDefEq pft expectedType) do + return s!"Error: proof has type {pft} but goal has type {expectedType}" + + let pf ← oldGoal.withContext $ abstractAllLambdaFVars pf + let pft ← Meta.inferType pf >>= instantiateMVars + + -- Find level parameters + let usedLevels := collectLevelParams {} pft + let usedLevels := collectLevelParams usedLevels pf + + let decl := Declaration.defnDecl { + name := Name.anonymous, + type := pft, + value := pf, + levelParams := usedLevels.params.toList, + hints := ReducibilityHints.opaque, + safety := DefinitionSafety.safe + } + + try + let _ ← addDecl decl + return "OK" + catch ex => + return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + + if res != "OK" then + allOk := false + errorMsg := res + break + + return if allOk then "OK" else errorMsg /-- Record a `ProofSnapshot` and generate a JSON response for it. -/ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnapshot := none) : @@ -356,7 +345,7 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap goalInfos mctxAfter := mctxAfterJson proofStatus := (← getProofStatus proofState) - stepVerification := (← verifyGoalAssignment proofState old?) } + stepVerification := (← verifyGoalAssignment ctx proofState old?) } /-- Pickle a `CommandSnapshot`, generating a JSON response. -/ def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Error) := do From 8870e1e3c3dde5baad844663ee6de7b33ec63397 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Wed, 16 Apr 2025 18:28:13 +0200 Subject: [PATCH 20/47] Proof step verification using kernel. #4 --- REPL/JSON.lean | 2 ++ REPL/Main.lean | 14 +++++++++++--- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index bc52caae..3fe7104b 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -185,6 +185,7 @@ structure MetavarDecl.Json where userName : String type : String mvarsInType : List MVarId + value : Option String deriving ToJson, FromJson structure MetavarContext.Json where @@ -200,6 +201,7 @@ def MetavarContext.toJson (mctx : MetavarContext) (ctx : ContextInfo) : IO Metav userName := toString decl.userName type := (← ctx.ppExpr {} decl.type).pretty mvarsInType := typeMVars.result.toList + value := (mctx.getExprAssignmentCore? mvarId).map toString } return { decls } diff --git a/REPL/Main.lean b/REPL/Main.lean index e79fceb0..68d113de 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -269,18 +269,26 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr | none => return s!"Goal {oldGoal.name} was not solved" | some pf => do let pf ← instantiateMVars pf + let pft ← Meta.inferType pf >>= instantiateMVars -- Check that all MVars in the proof are goals in new state - -- let mvars ← Meta.getMVars pf let (_, mvars) ← ctx.runMetaM proofState.metaContext.lctx ((Meta.collectMVars pf).run {}) - IO.println s!"Goal {oldGoal.name} = {pf} ({mvars.result.map (·.name)})" + -- IO.println s!"Goal {oldGoal.name} = {pf} ({mvars.result.map (·.name)})" + let mut pfWithSorries := pf for mvar in mvars.result do -- If the metavariable in the assignment is a new goal, it's fine. unless proofState.tacticState.goals.contains mvar do return s!"Goal {oldGoal.name} assignment contains metavariables" + -- If the metavariable is a new goal, replace it with sorry so that we can check the proof. + let sorryTerm ← Meta.mkSorry pft false + pfWithSorries ← pure $ pfWithSorries.replace ( + fun e => if e == mkMVar mvar then some sorryTerm else none + ) + let pf := pfWithSorries + -- IO.println s!"Goal with sorries {oldGoal.name} = {pf}" + -- Check that proof has expected type - let pft ← Meta.inferType pf >>= instantiateMVars let expectedType ← Meta.inferType (mkMVar oldGoal) >>= instantiateMVars unless (← Meta.isDefEq pft expectedType) do return s!"Error: proof has type {pft} but goal has type {expectedType}" From 4ac2b8959fd22e544c8fe091d04ebba58e8ec388 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 17 Apr 2025 12:35:09 +0200 Subject: [PATCH 21/47] Proof step verification using kernel. #5 --- REPL/Main.lean | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 68d113de..815db9dc 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -246,6 +246,18 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do | _ => return "Incomplete: open goals remain" +def replaceWithPrint (f? : Expr → Option Expr) (e : Expr) : MetaM Expr := do + IO.println s!"Processing expression: {e}" + match f? e with + | some eNew => return eNew + | none => match e with + | .forallE _ d b _ => let d ← replaceWithPrint f? d; let b ← replaceWithPrint f? b; return e.updateForallE! d b + | .lam _ d b _ => let d ← replaceWithPrint f? d; let b ← replaceWithPrint f? b; return e.updateLambdaE! d b + | .mdata _ b => let b ← replaceWithPrint f? b; return e.updateMData! b + | .letE _ t v b _ => let t ← replaceWithPrint f? t; let v ← replaceWithPrint f? v; let b ← replaceWithPrint f? b; return e.updateLet! t v b + | .app f a => let f ← replaceWithPrint f? f; let a ← replaceWithPrint f? a; return e.updateApp! f a + | .proj _ _ b => let b ← replaceWithPrint f? b; return e.updateProj! b + | e => return e /-- Verifies that all goals from the old state are properly handled in the new state. Returns either "OK" or an error message describing the first failing goal. @@ -265,6 +277,7 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr let (res, _) ← proofState.runMetaM do -- Check if goal is assigned in new state + -- TODO: maybe we need to check delayed assignment as well match proofState.metaState.mctx.getExprAssignmentCore? oldGoal with | none => return s!"Goal {oldGoal.name} was not solved" | some pf => do @@ -274,8 +287,23 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr -- Check that all MVars in the proof are goals in new state let (_, mvars) ← ctx.runMetaM proofState.metaContext.lctx ((Meta.collectMVars pf).run {}) -- IO.println s!"Goal {oldGoal.name} = {pf} ({mvars.result.map (·.name)})" + -- for mvar in mvars.result do + -- let assignment? ← getExprMVarAssignment? mvar + -- let delayedAssignment? ← getDelayedMVarAssignment? mvar + -- match assignment?, delayedAssignment? with + -- | some a, _ => IO.println s!"Assignment for {mvar.name}: {a}" + -- | _, some d => IO.println s!"Delayed assignment for {mvar.name}: {d.mvarIdPending.name}" + -- | none, none => IO.println s!"No assignment for {mvar.name}" + let mut pfWithSorries := pf for mvar in mvars.result do + let assigned ← mvar.isAssigned + let delayedAssigned ← mvar.isDelayedAssigned + -- We only care about the leaf metavariables. + -- TODO: verify this reasoning (especially for delayed assignments) + if assigned || delayedAssigned then + continue + -- If the metavariable in the assignment is a new goal, it's fine. unless proofState.tacticState.goals.contains mvar do return s!"Goal {oldGoal.name} assignment contains metavariables" @@ -285,8 +313,12 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr pfWithSorries ← pure $ pfWithSorries.replace ( fun e => if e == mkMVar mvar then some sorryTerm else none ) + -- pfWithSorries ← replaceWithPrint ( + -- fun e => if e == mkMVar mvar then some sorryTerm else none + -- ) pfWithSorries let pf := pfWithSorries - -- IO.println s!"Goal with sorries {oldGoal.name} = {pf}" + let pf ← instantiateMVars pf + IO.println s!"Goal with sorries {oldGoal.name} = {pf}" -- Check that proof has expected type let expectedType ← Meta.inferType (mkMVar oldGoal) >>= instantiateMVars From e6d40adf03d867d83e20d32d440420a97e70af33 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 17 Apr 2025 12:44:31 +0200 Subject: [PATCH 22/47] Disable potentially expensive operations. --- REPL/JSON.lean | 3 ++- REPL/Main.lean | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 3fe7104b..c90be06e 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -201,7 +201,8 @@ def MetavarContext.toJson (mctx : MetavarContext) (ctx : ContextInfo) : IO Metav userName := toString decl.userName type := (← ctx.ppExpr {} decl.type).pretty mvarsInType := typeMVars.result.toList - value := (mctx.getExprAssignmentCore? mvarId).map toString + -- value := (mctx.getExprAssignmentCore? mvarId).map toString + value := "N/A" } return { decls } diff --git a/REPL/Main.lean b/REPL/Main.lean index 815db9dc..a9936574 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -385,7 +385,8 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap goalInfos mctxAfter := mctxAfterJson proofStatus := (← getProofStatus proofState) - stepVerification := (← verifyGoalAssignment ctx proofState old?) } + -- stepVerification := (← verifyGoalAssignment ctx proofState old?) } + stepVerification := "N/A"} /-- Pickle a `CommandSnapshot`, generating a JSON response. -/ def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Error) := do From 47ecb6aadd12af198230804a63e80d018e6324e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 17 Apr 2025 15:52:03 +0200 Subject: [PATCH 23/47] Disable logs. --- REPL/Main.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index a9936574..da245805 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -318,7 +318,7 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr -- ) pfWithSorries let pf := pfWithSorries let pf ← instantiateMVars pf - IO.println s!"Goal with sorries {oldGoal.name} = {pf}" + -- IO.println s!"Goal with sorries {oldGoal.name} = {pf}" -- Check that proof has expected type let expectedType ← Meta.inferType (mkMVar oldGoal) >>= instantiateMVars From f2a8bb78d03eb3df69d5fa12ed708c6448c2f1ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Tue, 22 Apr 2025 17:00:46 +0200 Subject: [PATCH 24/47] Snapshot pruning. --- REPL/JSON.lean | 5 +++++ REPL/Main.lean | 21 +++++++++++++++++++++ 2 files changed, 26 insertions(+) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index c90be06e..4f1f2f70 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -38,6 +38,11 @@ structure File extends CommandOptions where path : System.FilePath deriving FromJson +structure PruneSnapshots where + cmdFromId : Option Nat + proofFromId : Option Nat +deriving ToJson, FromJson + /-- Run a tactic in a proof state. -/ diff --git a/REPL/Main.lean b/REPL/Main.lean index da245805..4d8e3708 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -95,6 +95,14 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do modify fun s => { s with proofStates := s.proofStates.push proofState } return id +/-- Delete all command snapshots with index >= id. -/ +def deleteCommandSnapshotsAfter (id : Nat) : M m Unit := do + modify fun s => { s with cmdStates := s.cmdStates.shrink id } + +/-- Delete all proof snapshots with index >= id. -/ +def deleteProofSnapshotsAfter (id : Nat) : M m Unit := do + modify fun s => { s with proofStates := s.proofStates.shrink id } + def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Option (List MVarId)) : M m (List Sorry) := trees.flatMap InfoTree.sorries |>.filter (fun t => match t.2.1 with @@ -423,6 +431,15 @@ def unpickleProofSnapshot (n : UnpickleProofState) : M IO (ProofStepResponse ⊕ let (proofState, _) ← ProofSnapshot.unpickle n.unpickleProofStateFrom cmdSnapshot? Sum.inl <$> createProofStepReponse proofState +def pruneSnapshots (n : PruneSnapshots) : M m String := do + match n.cmdFromId with + | some id => deleteCommandSnapshotsAfter id + | none => pure () + match n.proofFromId with + | some id => deleteProofSnapshotsAfter id + | none => pure () + return "OK" + partial def removeChildren (t : InfoTree) : InfoTree := match t with | InfoTree.context ctx t' => InfoTree.context ctx (removeChildren t') @@ -532,6 +549,7 @@ inductive Input | unpickleEnvironment : REPL.UnpickleEnvironment → Input | pickleProofSnapshot : REPL.PickleProofState → Input | unpickleProofSnapshot : REPL.UnpickleProofState → Input +| pruneSnapshots : REPL.PruneSnapshots → Input /-- Parse a user input string to an input command. -/ def parse (query : String) : IO Input := do @@ -553,6 +571,8 @@ def parse (query : String) : IO Input := do | .ok (r : REPL.Command) => return .command r | .error _ => match fromJson? j with | .ok (r : REPL.File) => return .file r + | .error _ => match fromJson? j with + | .ok (r : REPL.PruneSnapshots) => return .pruneSnapshots r | .error e => throw <| IO.userError <| toString <| toJson <| (⟨"Could not parse as a valid JSON command:\n" ++ e⟩ : Error) @@ -578,6 +598,7 @@ where loop : M IO Unit := do | .unpickleEnvironment r => return toJson (← unpickleCommandSnapshot r) | .pickleProofSnapshot r => return toJson (← pickleProofSnapshot r) | .unpickleProofSnapshot r => return toJson (← unpickleProofSnapshot r) + | .pruneSnapshots r => return toJson (← pruneSnapshots r) printFlush "\n" -- easier to parse the output if there are blank lines loop From ea69f10d2e30777007980e76f6865240744ea0e0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Wed, 23 Apr 2025 12:46:27 +0200 Subject: [PATCH 25/47] Extract goal assignment recursively. --- REPL/Main.lean | 52 +++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 43 insertions(+), 9 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 4d8e3708..e9105863 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -266,6 +266,39 @@ def replaceWithPrint (f? : Expr → Option Expr) (e : Expr) : MetaM Expr := do | .app f a => let f ← replaceWithPrint f? f; let a ← replaceWithPrint f? a; return e.updateApp! f a | .proj _ _ b => let b ← replaceWithPrint f? b; return e.updateProj! b | e => return e + +/-- + Given a metavar‐context `mctx` and a metavariable `mvarId`, + first lookup its "core" assignment or delayed assignment, + then recursively replace any immediate `?m` occurrences in that Expr + by their own core/delayed assignments. + Returns `none` if no assignment of either kind is found. +-/ +partial def getFullAssignment (mctx : MetavarContext) (mvarId : MVarId) : Option Expr := + goMVar mvarId + where + -- goExpr: traverse an Expr, inlining any mvars via goMVar + goExpr (e : Expr) : Expr := + match e with + | .mvar mid => + match goMVar mid with + | some e' => e' + | none => e + | .forallE nm ty bd bi => .forallE nm (goExpr ty) (goExpr bd) bi + | .lam nm ty bd bi => .lam nm (goExpr ty) (goExpr bd) bi + | .app f a => .app (goExpr f) (goExpr a) + | .letE nm ty v bd bi => .letE nm (goExpr ty) (goExpr v) (goExpr bd) bi + | .mdata md b => .mdata md (goExpr b) + | .proj s i b => .proj s i (goExpr b) + | other => other + goMVar (mid : MVarId) : Option Expr := + match mctx.getExprAssignmentCore? mid with + | some e => some (goExpr e) + | none => + match mctx.getDelayedMVarAssignmentCore? mid with + | some da => goMVar da.mvarIdPending + | none => none + /-- Verifies that all goals from the old state are properly handled in the new state. Returns either "OK" or an error message describing the first failing goal. @@ -284,17 +317,17 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr continue let (res, _) ← proofState.runMetaM do - -- Check if goal is assigned in new state - -- TODO: maybe we need to check delayed assignment as well - match proofState.metaState.mctx.getExprAssignmentCore? oldGoal with - | none => return s!"Goal {oldGoal.name} was not solved" - | some pf => do - let pf ← instantiateMVars pf + IO.println s!"Verifying goal {oldGoal.name}" + -- Check if goal is assigned in new state (now handling delayed assigns too) + match getFullAssignment proofState.metaState.mctx oldGoal with + | none => return s!"Goal {oldGoal.name} was not solved" + | some pfRaw => do + let pf ← instantiateMVars pfRaw let pft ← Meta.inferType pf >>= instantiateMVars -- Check that all MVars in the proof are goals in new state let (_, mvars) ← ctx.runMetaM proofState.metaContext.lctx ((Meta.collectMVars pf).run {}) - -- IO.println s!"Goal {oldGoal.name} = {pf} ({mvars.result.map (·.name)})" + IO.println s!"Goal {oldGoal.name} = {pf} ({mvars.result.map (·.name)})" -- for mvar in mvars.result do -- let assignment? ← getExprMVarAssignment? mvar -- let delayedAssignment? ← getDelayedMVarAssignment? mvar @@ -393,8 +426,9 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap goalInfos mctxAfter := mctxAfterJson proofStatus := (← getProofStatus proofState) - -- stepVerification := (← verifyGoalAssignment ctx proofState old?) } - stepVerification := "N/A"} + stepVerification := (← verifyGoalAssignment ctx proofState old?) + -- stepVerification := "N/A" + } /-- Pickle a `CommandSnapshot`, generating a JSON response. -/ def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Error) := do From b59028a9311f2a059d9ad8cbfb4116b660dfa95f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Wed, 23 Apr 2025 15:31:03 +0200 Subject: [PATCH 26/47] Logging to get insight into getFullAssignment. --- REPL/Main.lean | 58 +++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 55 insertions(+), 3 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index e9105863..3437ca7d 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -299,6 +299,49 @@ partial def getFullAssignment (mctx : MetavarContext) (mvarId : MVarId) : Option | some da => goMVar da.mvarIdPending | none => none +partial def getFullAssignment2 (mctx : MetavarContext) (mvarId : MVarId) : IO (Option Expr) := + goMVar mvarId +where + /-- Traverse an Expr, inlining any mvars via goMVar, but first print it. -/ + goExpr (e : Expr) : IO Expr := do + IO.println s!"[goExpr] ▶ {e}" + match e with + | .mvar mid => + -- try to inline that mvar + match (← goMVar mid) with + | some e' => pure e' + | none => pure e + | .forallE nm ty bd bi => + pure $ .forallE nm (← goExpr ty) (← goExpr bd) bi + | .lam nm ty bd bi => + pure $ .lam nm (← goExpr ty) (← goExpr bd) bi + | .app f a => + pure $ .app (← goExpr f) (← goExpr a) + | .letE nm ty v bd bi => + pure $ .letE nm (← goExpr ty) (← goExpr v) (← goExpr bd) bi + | .mdata md b => + pure $ .mdata md (← goExpr b) + | .proj s i b => + pure $ .proj s i (← goExpr b) + | other => + pure other + + /-- Lookup the “core” or delayed assignment of a mvar, printing the mvar first. -/ + goMVar (mid : MVarId) : IO (Option Expr) := do + IO.println s!"[goMVar] ▶ {mid.name}" + match mctx.getExprAssignmentCore? mid with + | some e => + -- directly assigned: inline and return + some <$> goExpr e + | none => + match mctx.getDelayedMVarAssignmentCore? mid with + | some da => + -- there’s a pending delayed assignment + goMVar da.mvarIdPending + | none => + -- not assigned at all + pure none + /-- Verifies that all goals from the old state are properly handled in the new state. Returns either "OK" or an error message describing the first failing goal. @@ -318,16 +361,21 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr let (res, _) ← proofState.runMetaM do IO.println s!"Verifying goal {oldGoal.name}" + -- let x ← getFullAssignment proofState.metaState.mctx oldGoal + -- IO.println s!"DONE {x}\n" -- Check if goal is assigned in new state (now handling delayed assigns too) match getFullAssignment proofState.metaState.mctx oldGoal with | none => return s!"Goal {oldGoal.name} was not solved" | some pfRaw => do + IO.println s!"pfRaw ▶ {pfRaw}\n" let pf ← instantiateMVars pfRaw - let pft ← Meta.inferType pf >>= instantiateMVars + IO.println s!"pf ▶ {pf}\n" + -- let pft ← Meta.inferType pf >>= instantiateMVars + -- IO.println s!"[verifyGoalAssignment] ▶ {pft}" -- Check that all MVars in the proof are goals in new state let (_, mvars) ← ctx.runMetaM proofState.metaContext.lctx ((Meta.collectMVars pf).run {}) - IO.println s!"Goal {oldGoal.name} = {pf} ({mvars.result.map (·.name)})" + IO.println s!"Goal {oldGoal.name} = {pf} ({mvars.result.map (·.name)})\n" -- for mvar in mvars.result do -- let assignment? ← getExprMVarAssignment? mvar -- let delayedAssignment? ← getDelayedMVarAssignment? mvar @@ -350,7 +398,8 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr return s!"Goal {oldGoal.name} assignment contains metavariables" -- If the metavariable is a new goal, replace it with sorry so that we can check the proof. - let sorryTerm ← Meta.mkSorry pft false + let mvarType ← Meta.inferType (.mvar mvar) + let sorryTerm ← Meta.mkSorry mvarType false pfWithSorries ← pure $ pfWithSorries.replace ( fun e => if e == mkMVar mvar then some sorryTerm else none ) @@ -359,6 +408,9 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr -- ) pfWithSorries let pf := pfWithSorries let pf ← instantiateMVars pf + IO.println s!"pf with sorries ▶ {pf}\n" + let pft ← Meta.inferType pf >>= instantiateMVars + IO.println s!"pft ▶ {pft}\n" -- IO.println s!"Goal with sorries {oldGoal.name} = {pf}" -- Check that proof has expected type From 39bc0dd76cdfecffb6305cb6b28deab0104640a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Wed, 23 Apr 2025 17:00:06 +0200 Subject: [PATCH 27/47] Simpler approach: check all mvars but replace only top-level ones. --- REPL/Main.lean | 106 +++++++++++++++++++++++++++++++++---------------- 1 file changed, 72 insertions(+), 34 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 3437ca7d..e32f83cf 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -267,6 +267,20 @@ def replaceWithPrint (f? : Expr → Option Expr) (e : Expr) : MetaM Expr := do | .proj _ _ b => let b ← replaceWithPrint f? b; return e.updateProj! b | e => return e +partial def replaceMVarsWithSorry (e : Expr) : MetaM Expr := do + match e with + | .mvar _ => do + let mvarType ← Meta.inferType e + let sorryTerm ← Meta.mkSorry mvarType false + return sorryTerm + | .forallE _ d b _ => let d ← replaceMVarsWithSorry d; let b ← replaceMVarsWithSorry b; return e.updateForallE! d b + | .lam _ d b _ => let d ← replaceMVarsWithSorry d; let b ← replaceMVarsWithSorry b; return e.updateLambdaE! d b + | .mdata _ b => let b ← replaceMVarsWithSorry b; return e.updateMData! b + | .letE _ t v b _ => let t ← replaceMVarsWithSorry t; let v ← replaceMVarsWithSorry v; let b ← replaceMVarsWithSorry b; return e.updateLet! t v b + | .app f a => let f ← replaceMVarsWithSorry f; let a ← replaceMVarsWithSorry a; return e.updateApp! f a + | .proj _ _ b => let b ← replaceMVarsWithSorry b; return e.updateProj! b + | e => return e + /-- Given a metavar‐context `mctx` and a metavariable `mvarId`, first lookup its "core" assignment or delayed assignment, @@ -299,7 +313,7 @@ partial def getFullAssignment (mctx : MetavarContext) (mvarId : MVarId) : Option | some da => goMVar da.mvarIdPending | none => none -partial def getFullAssignment2 (mctx : MetavarContext) (mvarId : MVarId) : IO (Option Expr) := +partial def getFullAssignmentIO (mctx : MetavarContext) (mvarId : MVarId) : IO (Option Expr) := goMVar mvarId where /-- Traverse an Expr, inlining any mvars via goMVar, but first print it. -/ @@ -342,6 +356,54 @@ where -- not assigned at all pure none +partial def getFullAssignmentLambda (mctx : MetavarContext) (mvarId : MVarId) : MetaM (Option Expr) := + goMVar mvarId + where + goExpr (e : Expr) : MetaM Expr := do + match e with + | .mvar mid => + match (← goMVar mid) with + | some e' => pure e' + | none => pure e + | .forallE nm ty bd bi => + pure $ .forallE nm (← goExpr ty) (← goExpr bd) bi + | .lam nm ty bd bi => + pure $ .lam nm (← goExpr ty) (← goExpr bd) bi + | .app f a => + pure $ .app (← goExpr f) (← goExpr a) + | .letE nm ty v bd bi => + pure $ .letE nm (← goExpr ty) (← goExpr v) (← goExpr bd) bi + | .mdata md b => + pure $ .mdata md (← goExpr b) + | .proj s i b => + pure $ .proj s i (← goExpr b) + | other => + pure other + goMVar (mid : MVarId) : MetaM (Option Expr) := do + match mctx.getExprAssignmentCore? mid with + | some e => pure $ some (← goExpr e) + | none => + match mctx.getDelayedMVarAssignmentCore? mid with + | some da => do + let e' ← goMVar da.mvarIdPending + match e' with + | some e' => + let e'' ← Meta.mkLambdaFVars da.fvars e' + return some e'' + | none => return none + | none => pure none + +/-- Does the expression `e` contain the metavariable `t`? -/ +private def findInExpr (t : MVarId) : Expr → Bool + | Expr.mvar mid => mid == t + | Expr.app f a => findInExpr t f || findInExpr t a + | Expr.lam _ ty bd _ => findInExpr t ty || findInExpr t bd + | Expr.forallE _ ty bd _ => findInExpr t ty || findInExpr t bd + | Expr.letE _ ty val bd _=> findInExpr t ty || findInExpr t val || findInExpr t bd + | Expr.proj _ _ e => findInExpr t e + | Expr.mdata _ e => findInExpr t e + | _ => false + /-- Verifies that all goals from the old state are properly handled in the new state. Returns either "OK" or an error message describing the first failing goal. @@ -361,35 +423,22 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr let (res, _) ← proofState.runMetaM do IO.println s!"Verifying goal {oldGoal.name}" - -- let x ← getFullAssignment proofState.metaState.mctx oldGoal - -- IO.println s!"DONE {x}\n" - -- Check if goal is assigned in new state (now handling delayed assigns too) - match getFullAssignment proofState.metaState.mctx oldGoal with + + match proofState.metaState.mctx.getExprAssignmentCore? oldGoal with | none => return s!"Goal {oldGoal.name} was not solved" | some pfRaw => do - IO.println s!"pfRaw ▶ {pfRaw}\n" let pf ← instantiateMVars pfRaw - IO.println s!"pf ▶ {pf}\n" - -- let pft ← Meta.inferType pf >>= instantiateMVars - -- IO.println s!"[verifyGoalAssignment] ▶ {pft}" - -- Check that all MVars in the proof are goals in new state let (_, mvars) ← ctx.runMetaM proofState.metaContext.lctx ((Meta.collectMVars pf).run {}) - IO.println s!"Goal {oldGoal.name} = {pf} ({mvars.result.map (·.name)})\n" - -- for mvar in mvars.result do - -- let assignment? ← getExprMVarAssignment? mvar - -- let delayedAssignment? ← getDelayedMVarAssignment? mvar - -- match assignment?, delayedAssignment? with - -- | some a, _ => IO.println s!"Assignment for {mvar.name}: {a}" - -- | _, some d => IO.println s!"Delayed assignment for {mvar.name}: {d.mvarIdPending.name}" - -- | none, none => IO.println s!"No assignment for {mvar.name}" - - let mut pfWithSorries := pf for mvar in mvars.result do + let assignment? := proofState.metaState.mctx.getExprAssignmentCore? mvar + if let some assignment := assignment? then + if findInExpr mvar assignment then + return s!"Goal {oldGoal.name} assignment is circular" + let assigned ← mvar.isAssigned let delayedAssigned ← mvar.isDelayedAssigned -- We only care about the leaf metavariables. - -- TODO: verify this reasoning (especially for delayed assignments) if assigned || delayedAssigned then continue @@ -397,21 +446,10 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr unless proofState.tacticState.goals.contains mvar do return s!"Goal {oldGoal.name} assignment contains metavariables" - -- If the metavariable is a new goal, replace it with sorry so that we can check the proof. - let mvarType ← Meta.inferType (.mvar mvar) - let sorryTerm ← Meta.mkSorry mvarType false - pfWithSorries ← pure $ pfWithSorries.replace ( - fun e => if e == mkMVar mvar then some sorryTerm else none - ) - -- pfWithSorries ← replaceWithPrint ( - -- fun e => if e == mkMVar mvar then some sorryTerm else none - -- ) pfWithSorries - let pf := pfWithSorries + let pf ← replaceMVarsWithSorry pf let pf ← instantiateMVars pf - IO.println s!"pf with sorries ▶ {pf}\n" + IO.println s!"pf with sorries ▶ {pf}" let pft ← Meta.inferType pf >>= instantiateMVars - IO.println s!"pft ▶ {pft}\n" - -- IO.println s!"Goal with sorries {oldGoal.name} = {pf}" -- Check that proof has expected type let expectedType ← Meta.inferType (mkMVar oldGoal) >>= instantiateMVars From 302997cbad466b89a26659e36e0c2f846e2b795b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Wed, 23 Apr 2025 18:41:32 +0200 Subject: [PATCH 28/47] Disable getProofStatus calculation. --- REPL/Main.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index e32f83cf..342298df 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -515,7 +515,8 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap traces goalInfos mctxAfter := mctxAfterJson - proofStatus := (← getProofStatus proofState) + -- proofStatus := (← getProofStatus proofState) + proofStatus := "N/A" stepVerification := (← verifyGoalAssignment ctx proofState old?) -- stepVerification := "N/A" } From 896390cd07115d38c3a043d1daa57f0adccd7091 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 24 Apr 2025 11:57:41 +0200 Subject: [PATCH 29/47] Remove redundant check, remove prints. --- REPL/Main.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 342298df..f682302c 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -422,8 +422,6 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr continue let (res, _) ← proofState.runMetaM do - IO.println s!"Verifying goal {oldGoal.name}" - match proofState.metaState.mctx.getExprAssignmentCore? oldGoal with | none => return s!"Goal {oldGoal.name} was not solved" | some pfRaw => do @@ -448,13 +446,6 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr let pf ← replaceMVarsWithSorry pf let pf ← instantiateMVars pf - IO.println s!"pf with sorries ▶ {pf}" - let pft ← Meta.inferType pf >>= instantiateMVars - - -- Check that proof has expected type - let expectedType ← Meta.inferType (mkMVar oldGoal) >>= instantiateMVars - unless (← Meta.isDefEq pft expectedType) do - return s!"Error: proof has type {pft} but goal has type {expectedType}" let pf ← oldGoal.withContext $ abstractAllLambdaFVars pf let pft ← Meta.inferType pf >>= instantiateMVars From cd2fcfd4609ae7c252fcd098b597105494878464 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 24 Apr 2025 14:02:14 +0200 Subject: [PATCH 30/47] Improve error messages. --- REPL/Main.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index f682302c..94ee91a0 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -417,13 +417,13 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr let mut errorMsg := "" for oldGoal in oldState.tacticState.goals do - -- If the goal is still present in the new proofState, we don't need to verify it yet. + -- If the goal is still present in the new proofState, we don't need to verify it yet since it will be taken care of later. if proofState.tacticState.goals.contains oldGoal then continue let (res, _) ← proofState.runMetaM do match proofState.metaState.mctx.getExprAssignmentCore? oldGoal with - | none => return s!"Goal {oldGoal.name} was not solved" + | none => return s!"Error: Goal {oldGoal.name} was not solved" | some pfRaw => do let pf ← instantiateMVars pfRaw -- Check that all MVars in the proof are goals in new state @@ -432,7 +432,7 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr let assignment? := proofState.metaState.mctx.getExprAssignmentCore? mvar if let some assignment := assignment? then if findInExpr mvar assignment then - return s!"Goal {oldGoal.name} assignment is circular" + return s!"Error: Goal {oldGoal.name} assignment is circular" let assigned ← mvar.isAssigned let delayedAssigned ← mvar.isDelayedAssigned @@ -442,7 +442,7 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr -- If the metavariable in the assignment is a new goal, it's fine. unless proofState.tacticState.goals.contains mvar do - return s!"Goal {oldGoal.name} assignment contains metavariables" + return s!"Error: Goal {oldGoal.name} assignment contains metavariables" let pf ← replaceMVarsWithSorry pf let pf ← instantiateMVars pf From df2e162fdc0cdf2cfc6913ad68e5500e25e4dc55 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 24 Apr 2025 14:25:57 +0200 Subject: [PATCH 31/47] Split verification into two functions. --- REPL/Main.lean | 55 +++++++++++++++++++++++++++++--------------------- 1 file changed, 32 insertions(+), 23 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 94ee91a0..ca1ffcc3 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -404,6 +404,29 @@ private def findInExpr (t : MVarId) : Expr → Bool | Expr.mdata _ e => findInExpr t e | _ => false + +def checkAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldGoal : MVarId) (pfRaw : Expr) : MetaM String := do + let pf ← instantiateMVars pfRaw + -- Check that all MVars in the proof are goals in new state + let (_, mvars) ← ctx.runMetaM proofState.metaContext.lctx ((Meta.collectMVars pf).run {}) + for mvar in mvars.result do + let assignment? := proofState.metaState.mctx.getExprAssignmentCore? mvar + if let some assignment := assignment? then + if findInExpr mvar assignment then + return s!"Error: Goal {oldGoal.name} assignment is circular" + + let assigned ← mvar.isAssigned + let delayedAssigned ← mvar.isDelayedAssigned + -- We only care about the leaf metavariables. + if assigned || delayedAssigned then + continue + + -- If the metavariable in the assignment is a new goal, it's fine. + unless proofState.tacticState.goals.contains mvar do + return s!"Error: Goal {oldGoal.name} assignment contains metavariables" + + return "OK" + /-- Verifies that all goals from the old state are properly handled in the new state. Returns either "OK" or an error message describing the first failing goal. @@ -425,29 +448,15 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr match proofState.metaState.mctx.getExprAssignmentCore? oldGoal with | none => return s!"Error: Goal {oldGoal.name} was not solved" | some pfRaw => do - let pf ← instantiateMVars pfRaw - -- Check that all MVars in the proof are goals in new state - let (_, mvars) ← ctx.runMetaM proofState.metaContext.lctx ((Meta.collectMVars pf).run {}) - for mvar in mvars.result do - let assignment? := proofState.metaState.mctx.getExprAssignmentCore? mvar - if let some assignment := assignment? then - if findInExpr mvar assignment then - return s!"Error: Goal {oldGoal.name} assignment is circular" - - let assigned ← mvar.isAssigned - let delayedAssigned ← mvar.isDelayedAssigned - -- We only care about the leaf metavariables. - if assigned || delayedAssigned then - continue - - -- If the metavariable in the assignment is a new goal, it's fine. - unless proofState.tacticState.goals.contains mvar do - return s!"Error: Goal {oldGoal.name} assignment contains metavariables" - - let pf ← replaceMVarsWithSorry pf - let pf ← instantiateMVars pf - - let pf ← oldGoal.withContext $ abstractAllLambdaFVars pf + let res ← checkAssignment ctx proofState oldGoal pfRaw + if res != "OK" then + return res + + let pfInCtx ← oldGoal.withContext do + let pf ← instantiateMVars pfRaw + let pf ← replaceMVarsWithSorry pf + instantiateMVars pf + let pf ← abstractAllLambdaFVars pfInCtx let pft ← Meta.inferType pf >>= instantiateMVars -- Find level parameters From 2aea4f821463b43eeb51d3191623d102542dfebf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 25 Apr 2025 11:03:15 +0200 Subject: [PATCH 32/47] Better circular assignment check. --- REPL/JSON.lean | 4 +-- REPL/Main.lean | 78 ++++++++++++++++++++++++++++++-------------------- 2 files changed, 49 insertions(+), 33 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 4f1f2f70..6490058e 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -206,8 +206,8 @@ def MetavarContext.toJson (mctx : MetavarContext) (ctx : ContextInfo) : IO Metav userName := toString decl.userName type := (← ctx.ppExpr {} decl.type).pretty mvarsInType := typeMVars.result.toList - -- value := (mctx.getExprAssignmentCore? mvarId).map toString - value := "N/A" + value := (mctx.getExprAssignmentCore? mvarId).map toString + -- value := "N/A" } return { decls } diff --git a/REPL/Main.lean b/REPL/Main.lean index ca1ffcc3..14732e5e 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -405,25 +405,37 @@ private def findInExpr (t : MVarId) : Expr → Bool | _ => false +/-- +Given a metavariable `mvar` and a candidate assignment `val`, returns +`true` precisely when assigning `mvar := val` would be _circular_. +-/ +def isCircularAssignment (mvar : MVarId) (val : Expr) : MetaM Bool := do + -- `occursCheck mvar val` returns `true` if *no* occurrence of `mvar` is found, + -- so we negate it to detect a circular reference. + let ok ← Lean.occursCheck mvar val + pure (!ok) + + def checkAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldGoal : MVarId) (pfRaw : Expr) : MetaM String := do let pf ← instantiateMVars pfRaw -- Check that all MVars in the proof are goals in new state let (_, mvars) ← ctx.runMetaM proofState.metaContext.lctx ((Meta.collectMVars pf).run {}) for mvar in mvars.result do - let assignment? := proofState.metaState.mctx.getExprAssignmentCore? mvar - if let some assignment := assignment? then - if findInExpr mvar assignment then - return s!"Error: Goal {oldGoal.name} assignment is circular" + -- If the metavariable in the assignment is a new goal, it's fine. + if proofState.tacticState.goals.contains mvar then + continue + + let isCircular ← isCircularAssignment mvar pf + if isCircular then + return s!"Error: Goal {oldGoal.name} assignment is circular" let assigned ← mvar.isAssigned let delayedAssigned ← mvar.isDelayedAssigned - -- We only care about the leaf metavariables. + -- We only care about the leaf metavariables, so we skip assigned ones. if assigned || delayedAssigned then continue - -- If the metavariable in the assignment is a new goal, it's fine. - unless proofState.tacticState.goals.contains mvar do - return s!"Error: Goal {oldGoal.name} assignment contains metavariables" + return s!"Error: Goal {oldGoal.name} assignment contains unassigned metavariables" return "OK" @@ -452,31 +464,35 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr if res != "OK" then return res - let pfInCtx ← oldGoal.withContext do + -- let pf ← instantiateMVars pfRaw + -- let pf ← replaceMVarsWithSorry pf + -- try + -- _ ← Lean.Meta.check pf + -- return "OK" + -- catch ex => + -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + + let x ← oldGoal.withContext do let pf ← instantiateMVars pfRaw let pf ← replaceMVarsWithSorry pf - instantiateMVars pf - let pf ← abstractAllLambdaFVars pfInCtx - let pft ← Meta.inferType pf >>= instantiateMVars - - -- Find level parameters - let usedLevels := collectLevelParams {} pft - let usedLevels := collectLevelParams usedLevels pf - - let decl := Declaration.defnDecl { - name := Name.anonymous, - type := pft, - value := pf, - levelParams := usedLevels.params.toList, - hints := ReducibilityHints.opaque, - safety := DefinitionSafety.safe - } - - try - let _ ← addDecl decl - return "OK" - catch ex => - return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + IO.println s!"pf ▶ {pf}" + try + _ ← Lean.Meta.check pf + return "OK" + catch ex => + return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + return x + + -- let pf ← oldGoal.withContext do + -- let pf ← instantiateMVars pfRaw + -- let pf ← replaceMVarsWithSorry pf + -- return pf + -- IO.println s!"pf ▶ {pf}" + -- try + -- _ ← Lean.Meta.check pf + -- return "OK" + -- catch ex => + -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" if res != "OK" then allOk := false From a6f722559e61ff5ba016806b4e71d5d1de9623ae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 25 Apr 2025 14:37:04 +0200 Subject: [PATCH 33/47] Add declaration instead of simple type check. --- REPL/Main.lean | 59 ++++++++++++++++++++++++++++++++++---------------- 1 file changed, 40 insertions(+), 19 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 14732e5e..0bb17275 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -418,21 +418,22 @@ def isCircularAssignment (mvar : MVarId) (val : Expr) : MetaM Bool := do def checkAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldGoal : MVarId) (pfRaw : Expr) : MetaM String := do let pf ← instantiateMVars pfRaw + + let occursCheck ← Lean.occursCheck oldGoal pf + if !occursCheck then + return s!"Error: Goal {oldGoal.name} assignment is syntactically circular" + -- Check that all MVars in the proof are goals in new state let (_, mvars) ← ctx.runMetaM proofState.metaContext.lctx ((Meta.collectMVars pf).run {}) + -- Loop through all unassigned metavariables (note that delayed assigned ones are included). for mvar in mvars.result do - -- If the metavariable in the assignment is a new goal, it's fine. - if proofState.tacticState.goals.contains mvar then + let delayedAssigned ← mvar.isDelayedAssigned + -- We only care about the leaf metavariables, so we skip delayed assigned ones. + if delayedAssigned then continue - let isCircular ← isCircularAssignment mvar pf - if isCircular then - return s!"Error: Goal {oldGoal.name} assignment is circular" - - let assigned ← mvar.isAssigned - let delayedAssigned ← mvar.isDelayedAssigned - -- We only care about the leaf metavariables, so we skip assigned ones. - if assigned || delayedAssigned then + -- If the metavariable in the assignment is a new goal, it's fine. + if proofState.tacticState.goals.contains mvar then continue return s!"Error: Goal {oldGoal.name} assignment contains unassigned metavariables" @@ -464,25 +465,45 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr if res != "OK" then return res - -- let pf ← instantiateMVars pfRaw - -- let pf ← replaceMVarsWithSorry pf - -- try - -- _ ← Lean.Meta.check pf - -- return "OK" - -- catch ex => - -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" let x ← oldGoal.withContext do let pf ← instantiateMVars pfRaw let pf ← replaceMVarsWithSorry pf - IO.println s!"pf ▶ {pf}" + let pft ← Meta.inferType pf >>= instantiateMVars + + let usedLevels := collectLevelParams {} pft + let usedLevels := collectLevelParams usedLevels pf + + let freshName ← mkFreshId + let decl := Declaration.defnDecl { + name := freshName, + type := pft, + value := pf, + levelParams := usedLevels.params.toList, + hints := ReducibilityHints.opaque, + safety := DefinitionSafety.safe + } + try - _ ← Lean.Meta.check pf + -- This check the declaration type, but also detects cycles. + let _ ← addDecl decl return "OK" catch ex => return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + return x + -- let x ← oldGoal.withContext do + -- let pf ← instantiateMVars pfRaw + -- let pf ← replaceMVarsWithSorry pf + -- IO.println s!"pf ▶ {pf}" + -- try + -- _ ← Lean.Meta.check pf + -- return "OK" + -- catch ex => + -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + -- return x + -- let pf ← oldGoal.withContext do -- let pf ← instantiateMVars pfRaw -- let pf ← replaceMVarsWithSorry pf From 69e41c105a746439ee051cda3c654e435fc0076c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Sat, 26 Apr 2025 11:32:46 +0200 Subject: [PATCH 34/47] Bring back addDecl. --- REPL/Main.lean | 133 ++++++++++++++++++++++++------------------------- 1 file changed, 66 insertions(+), 67 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 0bb17275..3feddee2 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -254,10 +254,12 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do | _ => return "Incomplete: open goals remain" -def replaceWithPrint (f? : Expr → Option Expr) (e : Expr) : MetaM Expr := do +def replaceWithPrint (f? : Expr → MetaM (Option Expr)) (e : Expr) : MetaM Expr := do IO.println s!"Processing expression: {e}" - match f? e with - | some eNew => return eNew + match ← f? e with + | some eNew => do + IO.println s!"Replaced with: {eNew}" + return eNew | none => match e with | .forallE _ d b _ => let d ← replaceWithPrint f? d; let b ← replaceWithPrint f? b; return e.updateForallE! d b | .lam _ d b _ => let d ← replaceWithPrint f? d; let b ← replaceWithPrint f? b; return e.updateLambdaE! d b @@ -267,7 +269,7 @@ def replaceWithPrint (f? : Expr → Option Expr) (e : Expr) : MetaM Expr := do | .proj _ _ b => let b ← replaceWithPrint f? b; return e.updateProj! b | e => return e -partial def replaceMVarsWithSorry (e : Expr) : MetaM Expr := do +def replaceMVarsWithSorry (e : Expr) : MetaM Expr := do match e with | .mvar _ => do let mvarType ← Meta.inferType e @@ -281,6 +283,17 @@ partial def replaceMVarsWithSorry (e : Expr) : MetaM Expr := do | .proj _ _ b => let b ← replaceMVarsWithSorry b; return e.updateProj! b | e => return e +def replaceMVarsWithSorryPrint (e : Expr) : MetaM Expr := do + let mkSorryForMVar (e : Expr) : MetaM (Option Expr) := do + if e.isMVar then + let mvarType ← Meta.inferType e + let sorryTerm ← Meta.mkSorry mvarType false + return some sorryTerm + else + return none + replaceWithPrint mkSorryForMVar e + + /-- Given a metavar‐context `mctx` and a metavariable `mvarId`, first lookup its "core" assignment or delayed assignment, @@ -447,80 +460,66 @@ Returns either "OK" or an error message describing the first failing goal. def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldProofState? : Option ProofSnapshot := none) : M m String := do match oldProofState? with - | none => return "OK" -- Nothing to verify - | some oldState => do - let mut allOk := true + | none => return "OK" -- Nothing to verify + | some oldSt => do let mut errorMsg := "" - - for oldGoal in oldState.tacticState.goals do - -- If the goal is still present in the new proofState, we don't need to verify it yet since it will be taken care of later. + for oldGoal in oldSt.tacticState.goals do + -- skip goals that are still open if proofState.tacticState.goals.contains oldGoal then continue + -- run checks and build closed declaration inside the goal's local context let (res, _) ← proofState.runMetaM do match proofState.metaState.mctx.getExprAssignmentCore? oldGoal with - | none => return s!"Error: Goal {oldGoal.name} was not solved" - | some pfRaw => do - let res ← checkAssignment ctx proofState oldGoal pfRaw - if res != "OK" then - return res - - - let x ← oldGoal.withContext do - let pf ← instantiateMVars pfRaw - let pf ← replaceMVarsWithSorry pf - let pft ← Meta.inferType pf >>= instantiateMVars - - let usedLevels := collectLevelParams {} pft - let usedLevels := collectLevelParams usedLevels pf - - let freshName ← mkFreshId - let decl := Declaration.defnDecl { - name := freshName, - type := pft, - value := pf, - levelParams := usedLevels.params.toList, - hints := ReducibilityHints.opaque, - safety := DefinitionSafety.safe - } - - try - -- This check the declaration type, but also detects cycles. - let _ ← addDecl decl - return "OK" - catch ex => - return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" - - return x - - -- let x ← oldGoal.withContext do - -- let pf ← instantiateMVars pfRaw - -- let pf ← replaceMVarsWithSorry pf - -- IO.println s!"pf ▶ {pf}" - -- try - -- _ ← Lean.Meta.check pf - -- return "OK" - -- catch ex => - -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" - -- return x - - -- let pf ← oldGoal.withContext do - -- let pf ← instantiateMVars pfRaw - -- let pf ← replaceMVarsWithSorry pf - -- return pf - -- IO.println s!"pf ▶ {pf}" - -- try - -- _ ← Lean.Meta.check pf - -- return "OK" - -- catch ex => - -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + | none => return s!"Error: Goal {oldGoal.name} was not solved" + | some pfRaw => do + -- preliminary user check + let chk ← checkAssignment ctx proofState oldGoal pfRaw + if chk != "OK" then return chk + + -- switch to the local context of the goal + -- oldGoal.withContext do + + let pfInst ← instantiateMVars pfRaw + let pfLam ← abstractAllLambdaFVars pfInst + let pfClosed ← replaceMVarsWithSorryPrint pfInst + + -- infer its type (it already includes the same Pi over locals) + let pftRaw ← Meta.inferType pfLam + let pftClosed ← instantiateMVars pftRaw + + -- collect universe levels + let usedLvls := + let l1 := collectLevelParams {} pftClosed + collectLevelParams l1 pfClosed + + IO.println s!"pfClosed: {pfClosed}" + IO.println s!"pftClosed: {pftClosed}" + IO.println s!"usedLvls: {usedLvls.params.toList}" + + -- build the declaration + let freshName ← mkFreshId + let decl := Declaration.defnDecl { + name := freshName, + type := pftClosed, + value := pfClosed, + levelParams := usedLvls.params.toList, + hints := ReducibilityHints.opaque, + safety := DefinitionSafety.safe + } + + -- add and check + try + let _ ← addDecl decl + return "OK" + catch ex => + return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" if res != "OK" then - allOk := false errorMsg := res break - return if allOk then "OK" else errorMsg + return if errorMsg == "" then "OK" else errorMsg /-- Record a `ProofSnapshot` and generate a JSON response for it. -/ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnapshot := none) : From 3536196e56b79f8806027795ffcd4044d4ea369c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Sat, 26 Apr 2025 18:10:00 +0200 Subject: [PATCH 35/47] Revert to simple type-check. --- REPL/Main.lean | 94 +++++++++++++++++++++++++++----------------------- 1 file changed, 51 insertions(+), 43 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index 3feddee2..1ecbbf9f 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -429,17 +429,17 @@ def isCircularAssignment (mvar : MVarId) (val : Expr) : MetaM Bool := do pure (!ok) -def checkAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldGoal : MVarId) (pfRaw : Expr) : MetaM String := do +def checkAssignment (proofState : ProofSnapshot) (oldGoal : MVarId) (pfRaw : Expr) : MetaM String := do let pf ← instantiateMVars pfRaw let occursCheck ← Lean.occursCheck oldGoal pf if !occursCheck then - return s!"Error: Goal {oldGoal.name} assignment is syntactically circular" + return s!"Error: Goal {oldGoal.name} assignment is circular" -- Check that all MVars in the proof are goals in new state - let (_, mvars) ← ctx.runMetaM proofState.metaContext.lctx ((Meta.collectMVars pf).run {}) + let mvars ← Meta.getMVars pf -- Loop through all unassigned metavariables (note that delayed assigned ones are included). - for mvar in mvars.result do + for mvar in mvars do let delayedAssigned ← mvar.isDelayedAssigned -- We only care about the leaf metavariables, so we skip delayed assigned ones. if delayedAssigned then @@ -457,7 +457,7 @@ def checkAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldGoal : Verifies that all goals from the old state are properly handled in the new state. Returns either "OK" or an error message describing the first failing goal. -/ -def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldProofState? : Option ProofSnapshot := none) : +def verifyGoalAssignment (proofState : ProofSnapshot) (oldProofState? : Option ProofSnapshot := none) : M m String := do match oldProofState? with | none => return "OK" -- Nothing to verify @@ -470,50 +470,58 @@ def verifyGoalAssignment (ctx : ContextInfo) (proofState : ProofSnapshot) (oldPr -- run checks and build closed declaration inside the goal's local context let (res, _) ← proofState.runMetaM do - match proofState.metaState.mctx.getExprAssignmentCore? oldGoal with + match ← getExprMVarAssignment? oldGoal with | none => return s!"Error: Goal {oldGoal.name} was not solved" | some pfRaw => do - -- preliminary user check - let chk ← checkAssignment ctx proofState oldGoal pfRaw + let chk ← checkAssignment proofState oldGoal pfRaw if chk != "OK" then return chk -- switch to the local context of the goal -- oldGoal.withContext do + oldGoal.withContext do + let pf ← instantiateMVars pfRaw + let pf ← replaceMVarsWithSorry pf + try + _ ← Lean.Meta.check pf + return "OK" + catch ex => + return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" - let pfInst ← instantiateMVars pfRaw - let pfLam ← abstractAllLambdaFVars pfInst - let pfClosed ← replaceMVarsWithSorryPrint pfInst - - -- infer its type (it already includes the same Pi over locals) - let pftRaw ← Meta.inferType pfLam - let pftClosed ← instantiateMVars pftRaw - - -- collect universe levels - let usedLvls := - let l1 := collectLevelParams {} pftClosed - collectLevelParams l1 pfClosed - - IO.println s!"pfClosed: {pfClosed}" - IO.println s!"pftClosed: {pftClosed}" - IO.println s!"usedLvls: {usedLvls.params.toList}" - - -- build the declaration - let freshName ← mkFreshId - let decl := Declaration.defnDecl { - name := freshName, - type := pftClosed, - value := pfClosed, - levelParams := usedLvls.params.toList, - hints := ReducibilityHints.opaque, - safety := DefinitionSafety.safe - } - - -- add and check - try - let _ ← addDecl decl - return "OK" - catch ex => - return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + -- let pfInst ← instantiateMVars pfRaw + -- let pfLam ← abstractAllLambdaFVars pfInst + -- let pfClosed ← replaceMVarsWithSorryPrint pfInst + + -- -- infer its type (it already includes the same Pi over locals) + -- let pftRaw ← Meta.inferType pfLam + -- let pftClosed ← instantiateMVars pftRaw + + -- -- collect universe levels + -- let usedLvls := + -- let l1 := collectLevelParams {} pftClosed + -- collectLevelParams l1 pfClosed + + -- IO.println s!"pfClosed: {pfClosed}" + -- IO.println s!"pftClosed: {pftClosed}" + -- IO.println s!"usedLvls: {usedLvls.params.toList}" + + -- -- build the declaration + -- let freshName ← mkFreshId + -- let decl := Declaration.defnDecl { + -- name := freshName, + -- type := pftClosed, + -- value := pfClosed, + -- levelParams := usedLvls.params.toList, + -- hints := ReducibilityHints.opaque, + -- safety := DefinitionSafety.safe + -- } + + -- -- add and check + -- try + -- -- TODO: isn't this memory leak + -- let _ ← addDecl decl + -- return "OK" + -- catch ex => + -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" if res != "OK" then errorMsg := res @@ -553,7 +561,7 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap mctxAfter := mctxAfterJson -- proofStatus := (← getProofStatus proofState) proofStatus := "N/A" - stepVerification := (← verifyGoalAssignment ctx proofState old?) + stepVerification := (← verifyGoalAssignment proofState old?) -- stepVerification := "N/A" } From cce6249cfc4551160d49537df3b2f15c0df786e2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 2 May 2025 16:49:03 +0200 Subject: [PATCH 36/47] Implement getFullMVars. --- REPL/JSON.lean | 4 ++-- REPL/Main.lean | 45 ++++++++++++++++++++++++++++++++------------- 2 files changed, 34 insertions(+), 15 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 6490058e..4f1f2f70 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -206,8 +206,8 @@ def MetavarContext.toJson (mctx : MetavarContext) (ctx : ContextInfo) : IO Metav userName := toString decl.userName type := (← ctx.ppExpr {} decl.type).pretty mvarsInType := typeMVars.result.toList - value := (mctx.getExprAssignmentCore? mvarId).map toString - -- value := "N/A" + -- value := (mctx.getExprAssignmentCore? mvarId).map toString + value := "N/A" } return { decls } diff --git a/REPL/Main.lean b/REPL/Main.lean index 1ecbbf9f..cb851782 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -326,6 +326,36 @@ partial def getFullAssignment (mctx : MetavarContext) (mvarId : MVarId) : Option | some da => goMVar da.mvarIdPending | none => none +/-- + Given a metavar‐context `mctx` and a metavariable `mvarId`, + follow its core or delayed assignments recursively, + and collect the names of all metavariables reachable. + Returns a `NameSet` of metavariable names. +-/ +partial def getFullMvars (mctx : MetavarContext) (mvarId : MVarId) : NameSet := + goMVar mvarId NameSet.empty +where + /-- Handle a metavariable: inline its assignment if any, otherwise record it. -/ + goMVar (mid : MVarId) (acc : NameSet) : NameSet := + match mctx.getExprAssignmentCore? mid with + | some e => goExpr e acc + | none => + match mctx.getDelayedMVarAssignmentCore? mid with + | some da => goMVar da.mvarIdPending acc + | none => acc.insert mid.name + + /-- Traverse an `Expr`, collecting any metavars it contains. -/ + goExpr : Expr → NameSet → NameSet + | Expr.mvar mid, acc => goMVar mid acc + | Expr.app f a, acc => goExpr a (goExpr f acc) + | Expr.lam _ ty body _, acc => goExpr body (goExpr ty acc) + | Expr.forallE _ ty bd _, acc => goExpr bd (goExpr ty acc) + | Expr.letE _ ty val bd _,acc => goExpr bd (goExpr val (goExpr ty acc)) + | Expr.mdata _ b, acc => goExpr b acc + | Expr.proj _ _ b, acc => goExpr b acc + | _, acc => acc + + partial def getFullAssignmentIO (mctx : MetavarContext) (mvarId : MVarId) : IO (Option Expr) := goMVar mvarId where @@ -417,18 +447,6 @@ private def findInExpr (t : MVarId) : Expr → Bool | Expr.mdata _ e => findInExpr t e | _ => false - -/-- -Given a metavariable `mvar` and a candidate assignment `val`, returns -`true` precisely when assigning `mvar := val` would be _circular_. --/ -def isCircularAssignment (mvar : MVarId) (val : Expr) : MetaM Bool := do - -- `occursCheck mvar val` returns `true` if *no* occurrence of `mvar` is found, - -- so we negate it to detect a circular reference. - let ok ← Lean.occursCheck mvar val - pure (!ok) - - def checkAssignment (proofState : ProofSnapshot) (oldGoal : MVarId) (pfRaw : Expr) : MetaM String := do let pf ← instantiateMVars pfRaw @@ -438,7 +456,8 @@ def checkAssignment (proofState : ProofSnapshot) (oldGoal : MVarId) (pfRaw : Exp -- Check that all MVars in the proof are goals in new state let mvars ← Meta.getMVars pf - -- Loop through all unassigned metavariables (note that delayed assigned ones are included). + + -- Loop through all unassigned metavariables recursively (note that delayed assigned ones are included). for mvar in mvars do let delayedAssigned ← mvar.isDelayedAssigned -- We only care about the leaf metavariables, so we skip delayed assigned ones. From 46c0871a695afd444e08a2a832dcf5a701a507db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Sat, 3 May 2025 09:56:56 +0200 Subject: [PATCH 37/47] Revert to addDecl --- REPL/Main.lean | 77 +++++++++++++++++++++++++------------------------- 1 file changed, 39 insertions(+), 38 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index cb851782..bef10101 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -497,50 +497,51 @@ def verifyGoalAssignment (proofState : ProofSnapshot) (oldProofState? : Option P -- switch to the local context of the goal -- oldGoal.withContext do - oldGoal.withContext do - let pf ← instantiateMVars pfRaw - let pf ← replaceMVarsWithSorry pf - try - _ ← Lean.Meta.check pf - return "OK" - catch ex => - return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" - - -- let pfInst ← instantiateMVars pfRaw - -- let pfLam ← abstractAllLambdaFVars pfInst - -- let pfClosed ← replaceMVarsWithSorryPrint pfInst - - -- -- infer its type (it already includes the same Pi over locals) - -- let pftRaw ← Meta.inferType pfLam - -- let pftClosed ← instantiateMVars pftRaw + -- oldGoal.withContext do + -- let pf ← instantiateMVars pfRaw + -- let pf ← replaceMVarsWithSorry pf + -- try + -- _ ← Lean.Meta.check pf + -- return "OK" + -- catch ex => + -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + + let pfInst ← instantiateMVars pfRaw + let pfLam ← abstractAllLambdaFVars pfInst + let pfClosed ← replaceMVarsWithSorry pfLam + let pfClosed ← abstractAllLambdaFVars pfClosed + + -- infer its type (it already includes the same Pi over locals) + let pftRaw ← Meta.inferType pfClosed + let pftClosed ← instantiateMVars pftRaw -- -- collect universe levels - -- let usedLvls := - -- let l1 := collectLevelParams {} pftClosed - -- collectLevelParams l1 pfClosed + let usedLvls := + let l1 := collectLevelParams {} pftClosed + collectLevelParams l1 pfClosed - -- IO.println s!"pfClosed: {pfClosed}" - -- IO.println s!"pftClosed: {pftClosed}" + IO.println s!"pfClosed: {pfClosed}" + IO.println s!"pftClosed: {pftClosed}" -- IO.println s!"usedLvls: {usedLvls.params.toList}" -- -- build the declaration - -- let freshName ← mkFreshId - -- let decl := Declaration.defnDecl { - -- name := freshName, - -- type := pftClosed, - -- value := pfClosed, - -- levelParams := usedLvls.params.toList, - -- hints := ReducibilityHints.opaque, - -- safety := DefinitionSafety.safe - -- } - - -- -- add and check - -- try - -- -- TODO: isn't this memory leak - -- let _ ← addDecl decl - -- return "OK" - -- catch ex => - -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + let freshName ← mkFreshId + let decl := Declaration.defnDecl { + name := freshName, + type := pftClosed, + value := pfClosed, + levelParams := usedLvls.params.toList, + hints := ReducibilityHints.opaque, + safety := DefinitionSafety.safe + } + + -- add and check + try + -- TODO: isn't this memory leak + let _ ← addDecl decl + return "OK" + catch ex => + return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" if res != "OK" then errorMsg := res From f54ffd7cf00a121bfd3576a20f2e76de13aac56e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Sat, 3 May 2025 16:43:13 +0200 Subject: [PATCH 38/47] More robust type check. --- REPL/Main.lean | 100 ++++++++++++++++++++++++++----------------------- 1 file changed, 53 insertions(+), 47 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index bef10101..df3c4799 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -447,9 +447,7 @@ private def findInExpr (t : MVarId) : Expr → Bool | Expr.mdata _ e => findInExpr t e | _ => false -def checkAssignment (proofState : ProofSnapshot) (oldGoal : MVarId) (pfRaw : Expr) : MetaM String := do - let pf ← instantiateMVars pfRaw - +def checkAssignment (proofState : ProofSnapshot) (oldGoal : MVarId) (pf : Expr) : MetaM String := do let occursCheck ← Lean.occursCheck oldGoal pf if !occursCheck then return s!"Error: Goal {oldGoal.name} assignment is circular" @@ -489,60 +487,68 @@ def verifyGoalAssignment (proofState : ProofSnapshot) (oldProofState? : Option P -- run checks and build closed declaration inside the goal's local context let (res, _) ← proofState.runMetaM do + -- switch to the local context of the goal + oldGoal.withContext do match ← getExprMVarAssignment? oldGoal with | none => return s!"Error: Goal {oldGoal.name} was not solved" | some pfRaw => do - let chk ← checkAssignment proofState oldGoal pfRaw + let pf ← instantiateMVars pfRaw + -- First check that the proof has the expected type + let pft ← Meta.inferType pf >>= instantiateMVars + let expectedType ← Meta.inferType (mkMVar oldGoal) >>= instantiateMVars + unless (← Meta.isDefEq pft expectedType) do + return s!"Error: step assignment has type {pft} but goal has type {expectedType}" + + let chk ← checkAssignment proofState oldGoal pf if chk != "OK" then return chk - -- switch to the local context of the goal - -- oldGoal.withContext do - -- oldGoal.withContext do - -- let pf ← instantiateMVars pfRaw - -- let pf ← replaceMVarsWithSorry pf - -- try - -- _ ← Lean.Meta.check pf - -- return "OK" - -- catch ex => - -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" - - let pfInst ← instantiateMVars pfRaw - let pfLam ← abstractAllLambdaFVars pfInst - let pfClosed ← replaceMVarsWithSorry pfLam - let pfClosed ← abstractAllLambdaFVars pfClosed - - -- infer its type (it already includes the same Pi over locals) - let pftRaw ← Meta.inferType pfClosed - let pftClosed ← instantiateMVars pftRaw - - -- -- collect universe levels - let usedLvls := - let l1 := collectLevelParams {} pftClosed - collectLevelParams l1 pfClosed - - IO.println s!"pfClosed: {pfClosed}" - IO.println s!"pftClosed: {pftClosed}" - -- IO.println s!"usedLvls: {usedLvls.params.toList}" - - -- -- build the declaration - let freshName ← mkFreshId - let decl := Declaration.defnDecl { - name := freshName, - type := pftClosed, - value := pfClosed, - levelParams := usedLvls.params.toList, - hints := ReducibilityHints.opaque, - safety := DefinitionSafety.safe - } - - -- add and check + let pf ← instantiateMVars pfRaw + let pf ← replaceMVarsWithSorry pf try - -- TODO: isn't this memory leak - let _ ← addDecl decl + _ ← Lean.Meta.check pf return "OK" catch ex => return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + -- let pf ← instantiateMVars pfRaw + -- let pf ← abstractAllLambdaFVars pf + -- let pf ← instantiateMVars pf + -- -- let pf ← abstractAllLambdaFVars pf + -- let pf ← replaceMVarsWithSorry pf + -- -- let pf ← abstractAllLambdaFVars pf + + -- -- infer its type (it already includes the same Pi over locals) + -- let pftRaw ← Meta.inferType pf + -- let pftClosed ← instantiateMVars pftRaw + + -- -- collect universe levels + -- let usedLvls := + -- let l1 := collectLevelParams {} pftClosed + -- collectLevelParams l1 pf + + -- IO.println s!"pf: {pf}" + -- IO.println s!"pftClosed: {pftClosed}" + -- -- IO.println s!"usedLvls: {usedLvls.params.toList}" + + -- -- -- build the declaration + -- let freshName ← mkFreshId + -- let decl := Declaration.defnDecl { + -- name := freshName, + -- type := pftClosed, + -- value := pf, + -- levelParams := usedLvls.params.toList, + -- hints := ReducibilityHints.opaque, + -- safety := DefinitionSafety.safe + -- } + + -- -- add and check + -- try + -- -- TODO: isn't this memory leak + -- let _ ← addDecl decl + -- return "OK" + -- catch ex => + -- return s!"Error: kernel type check failed: {← ex.toMessageData.toString}" + if res != "OK" then errorMsg := res break From 60a4ae0d9ff726b03ace5bccda945a6ad9cde57a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Tue, 13 May 2025 22:39:22 +0200 Subject: [PATCH 39/47] Disable problematic sorry detection. --- REPL/Main.lean | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index df3c4799..c1fd44a4 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -122,15 +122,17 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) | .term _ none => unreachable! let proofStateId ← proofState.mapM recordProofSnapshot - let goalInfo : Option GoalInfo ← match proofState with - | some proofState => do - match proofState.tacticState.goals[0]? with - | some goalId => do - -- TODO: this does not work when it's just `sorry` instead of `by sorry` - allow printGoalInfo to return none - let info ← printGoalInfo ctx goalId - pure (some info) - | none => pure none - | none => pure none + -- let goalInfo : Option GoalInfo ← match proofState with + -- | some proofState => do + -- match proofState.tacticState.goals[0]? with + -- | some goalId => do + -- -- TODO: this does not work when it's just `sorry` instead of `by sorry` - allow printGoalInfo to return none + -- let info ← printGoalInfo ctx goalId + -- pure (some info) + -- | none => pure none + -- | none => pure none + -- TODO + let goalInfo : Option GoalInfo := none return Sorry.of goal goalInfo pos endPos proofStateId def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := From 3620b47f098e7db22a9330bbc66c6a3611b8e4f4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 15 May 2025 21:53:57 +0200 Subject: [PATCH 40/47] Revert "Disable problematic sorry detection." This reverts commit 60a4ae0d9ff726b03ace5bccda945a6ad9cde57a. --- REPL/Main.lean | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/REPL/Main.lean b/REPL/Main.lean index c1fd44a4..df3c4799 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -122,17 +122,15 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) | .term _ none => unreachable! let proofStateId ← proofState.mapM recordProofSnapshot - -- let goalInfo : Option GoalInfo ← match proofState with - -- | some proofState => do - -- match proofState.tacticState.goals[0]? with - -- | some goalId => do - -- -- TODO: this does not work when it's just `sorry` instead of `by sorry` - allow printGoalInfo to return none - -- let info ← printGoalInfo ctx goalId - -- pure (some info) - -- | none => pure none - -- | none => pure none - -- TODO - let goalInfo : Option GoalInfo := none + let goalInfo : Option GoalInfo ← match proofState with + | some proofState => do + match proofState.tacticState.goals[0]? with + | some goalId => do + -- TODO: this does not work when it's just `sorry` instead of `by sorry` - allow printGoalInfo to return none + let info ← printGoalInfo ctx goalId + pure (some info) + | none => pure none + | none => pure none return Sorry.of goal goalInfo pos endPos proofStateId def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := From 05b2e777e491894923b6d465c94d4c9541c83152 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 23 May 2025 11:42:48 +0200 Subject: [PATCH 41/47] Bump version to v4.19.0 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 9565de32..7aca1d8a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.19.0-rc2 +leanprover/lean4:v4.19.0 From 25ee5fcde2b708e0c5b32157f00bf2d9fcd21882 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 19 Jun 2025 21:43:47 +0200 Subject: [PATCH 42/47] Handle simp_rw. --- REPL/PaperProof/BetterParser.lean | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index 536669a6..16584acb 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -116,16 +116,21 @@ def getGoalsChange (ctx : ContextInfo) (tInfo : TacticInfo) : IO (List (List Str -- TODO: solve rw_mod_cast +open Parser.Tactic (optConfig rwRuleSeq location getConfigItems) + +elab s:"simp_rw " cfg:optConfig rws:rwRuleSeq g:(location)? : tactic => pure () + def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo) : IO (List ProofStepInfo) := do let range := stx.toRange ctx let prettify (tStr : String) := let res := tStr.trim.dropRightWhile (· == ',') -- rw puts final rfl on the "]" token -- TODO: is this correct for `rewrite`? - if res == "]" then "rfl" else res + -- if res == "]" then "rfl" else res + res -- Each part of rw is a separate step none of them include the initial 'rw [' and final ']'. -- So we add these to the first and last steps. - let extractRwStep (steps : List ProofStepInfo) (atClause? : Option Syntax) : IO (List ProofStepInfo) := do + let extractRwStep (steps : List ProofStepInfo) (tactic : String) (atClause? : Option Syntax) : IO (List ProofStepInfo) := do -- If atClause is present, call toJson on it and retrieve the `pp` field. let atClauseStr? ← match atClause? with | some atClause => do @@ -137,7 +142,7 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo -- Turn the `Option String` into a (possibly-empty) string so we can insert it. let maybeAtClause := atClauseStr?.getD "" -- getD "" returns `""` if `atClauseStr?` is `none` let rwSteps := steps.map fun a => - { a with tacticString := s!"rw [{prettify a.tacticString}]{maybeAtClause}" } + { a with tacticString := s!"{tactic} [{prettify a.tacticString}]{maybeAtClause}" } match rwSteps with | [] => @@ -153,9 +158,9 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo match stx with | `(tactic| rw [$_,*] $(at_clause)?) | `(tactic| rewrite [$_,*] $(at_clause)?) => - extractRwStep steps at_clause + extractRwStep steps "rw" at_clause | `(tactic| rwa [$_,*] $(at_clause)?) => - let rwSteps ← extractRwStep steps at_clause + let rwSteps ← extractRwStep steps "rw" at_clause let assumptionSteps := (if rwSteps.isEmpty then [] else rwSteps.getLast!.goalsAfter).map fun g => { tacticString := "assumption", @@ -170,6 +175,8 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo finish := none } return rwSteps ++ assumptionSteps + | `(tactic| simp_rw [$_,*] $(at_clause)?) => + extractRwStep steps "simp only" at_clause | _ => return steps -- Comparator for names, e.g. so that _uniq.34 and _uniq.102 go in the right order. -- That's not completely right because it doesn't compare prefixes but From 78ce2d8c680c94ff7ee48513eb760f58a9ae0e12 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Thu, 19 Jun 2025 22:03:17 +0200 Subject: [PATCH 43/47] dbg prints --- REPL/PaperProof/BetterParser.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index 16584acb..be7012f9 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -118,7 +118,9 @@ def getGoalsChange (ctx : ContextInfo) (tInfo : TacticInfo) : IO (List (List Str open Parser.Tactic (optConfig rwRuleSeq location getConfigItems) +namespace Mathlib.Tactic elab s:"simp_rw " cfg:optConfig rws:rwRuleSeq g:(location)? : tactic => pure () +end Mathlib.Tactic def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo) : IO (List ProofStepInfo) := do let range := stx.toRange ctx @@ -155,6 +157,7 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo let middle := steps.drop 1 |>.dropLast return first :: middle ++ [last] + -- dbg_trace s!"Tactic syntax: {stx}" match stx with | `(tactic| rw [$_,*] $(at_clause)?) | `(tactic| rewrite [$_,*] $(at_clause)?) => @@ -176,6 +179,7 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo } return rwSteps ++ assumptionSteps | `(tactic| simp_rw [$_,*] $(at_clause)?) => + -- dbg_trace s!"simp_rw!" extractRwStep steps "simp only" at_clause | _ => return steps -- Comparator for names, e.g. so that _uniq.34 and _uniq.102 go in the right order. From 32c009159fc0017bad38d39e92146552af2c13a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 20 Jun 2025 10:24:03 +0200 Subject: [PATCH 44/47] Report stringified syntax of each tactic. --- REPL/JSON.lean | 1 + REPL/PaperProof/BetterParser.lean | 14 ++++++++------ 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 4f1f2f70..dd2df731 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -213,6 +213,7 @@ def MetavarContext.toJson (mctx : MetavarContext) (ctx : ContextInfo) : IO Metav structure ProofStepInfo where tacticString : String + syntaxString: String infoTree : Option Json goalBefore : GoalInfo goalsAfter : List GoalInfo diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index be7012f9..31ee4817 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -118,9 +118,9 @@ def getGoalsChange (ctx : ContextInfo) (tInfo : TacticInfo) : IO (List (List Str open Parser.Tactic (optConfig rwRuleSeq location getConfigItems) -namespace Mathlib.Tactic -elab s:"simp_rw " cfg:optConfig rws:rwRuleSeq g:(location)? : tactic => pure () -end Mathlib.Tactic +-- namespace Mathlib.Tactic +-- elab s:"simp_rw " cfg:optConfig rws:rwRuleSeq g:(location)? : tactic => pure () +-- end Mathlib.Tactic def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo) : IO (List ProofStepInfo) := do let range := stx.toRange ctx @@ -167,6 +167,7 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo let assumptionSteps := (if rwSteps.isEmpty then [] else rwSteps.getLast!.goalsAfter).map fun g => { tacticString := "assumption", + syntaxString := "assumption", infoTree := none, goalBefore := g, goalsAfter := [], @@ -178,9 +179,9 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo finish := none } return rwSteps ++ assumptionSteps - | `(tactic| simp_rw [$_,*] $(at_clause)?) => + -- | `(tactic| simp_rw [$_,*] $(at_clause)?) => -- dbg_trace s!"simp_rw!" - extractRwStep steps "simp only" at_clause + -- extractRwStep steps "simp only" at_clause | _ => return steps -- Comparator for names, e.g. so that _uniq.34 and _uniq.102 go in the right order. -- That's not completely right because it doesn't compare prefixes but @@ -206,7 +207,7 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree let infoTreeJson ← (InfoTree.node i PersistentArray.empty).toJson ctx - let steps ← prettifySteps tInfo.stx ctx steps + -- let steps ← prettifySteps tInfo.stx ctx steps let proofTreeEdges ← getGoalsChange ctx tInfo let currentGoals := proofTreeEdges.map (fun ⟨ _, g₁, gs ⟩ => g₁ :: gs) |>.join @@ -227,6 +228,7 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree let range := tInfo.stx.toRange ctx some { tacticString, + syntaxString := tInfo.stx.formatStx.pretty, goalBefore, goalsAfter, mctxBefore := mctxBeforeJson, From 466e121f321ef74b2419fc5ceb6020bdc6ddc13a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 20 Jun 2025 15:23:29 +0200 Subject: [PATCH 45/47] Do not break down simp_rw. --- REPL/JSON.lean | 1 - REPL/PaperProof/BetterParser.lean | 32 ++++++++++++++----------------- 2 files changed, 14 insertions(+), 19 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index dd2df731..4f1f2f70 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -213,7 +213,6 @@ def MetavarContext.toJson (mctx : MetavarContext) (ctx : ContextInfo) : IO Metav structure ProofStepInfo where tacticString : String - syntaxString: String infoTree : Option Json goalBefore : GoalInfo goalsAfter : List GoalInfo diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index 31ee4817..db593453 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -118,10 +118,6 @@ def getGoalsChange (ctx : ContextInfo) (tInfo : TacticInfo) : IO (List (List Str open Parser.Tactic (optConfig rwRuleSeq location getConfigItems) --- namespace Mathlib.Tactic --- elab s:"simp_rw " cfg:optConfig rws:rwRuleSeq g:(location)? : tactic => pure () --- end Mathlib.Tactic - def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo) : IO (List ProofStepInfo) := do let range := stx.toRange ctx let prettify (tStr : String) := @@ -157,17 +153,16 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo let middle := steps.drop 1 |>.dropLast return first :: middle ++ [last] - -- dbg_trace s!"Tactic syntax: {stx}" match stx with - | `(tactic| rw [$_,*] $(at_clause)?) - | `(tactic| rewrite [$_,*] $(at_clause)?) => + | `(tactic| rw [$_,*] $(at_clause)?) => extractRwStep steps "rw" at_clause + | `(tactic| rewrite [$_,*] $(at_clause)?) => + extractRwStep steps "rewrite" at_clause | `(tactic| rwa [$_,*] $(at_clause)?) => let rwSteps ← extractRwStep steps "rw" at_clause let assumptionSteps := (if rwSteps.isEmpty then [] else rwSteps.getLast!.goalsAfter).map fun g => { tacticString := "assumption", - syntaxString := "assumption", infoTree := none, goalBefore := g, goalsAfter := [], @@ -179,10 +174,8 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo finish := none } return rwSteps ++ assumptionSteps - -- | `(tactic| simp_rw [$_,*] $(at_clause)?) => - -- dbg_trace s!"simp_rw!" - -- extractRwStep steps "simp only" at_clause | _ => return steps + -- Comparator for names, e.g. so that _uniq.34 and _uniq.102 go in the right order. -- That's not completely right because it doesn't compare prefixes but -- it's much shorter to write than correct version and serves the purpose. @@ -196,7 +189,7 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree let res := res.filterMap id let some ctx := i.updateContext? ctx | panic! "unexpected context node" - let steps := res.map (fun r => r.steps) |>.join + let mut steps := res.map (fun r => r.steps) |>.join let allSubGoals := Std.HashSet.empty.insertMany $ res.bind (·.allGoals.toList) if let .ofTacticInfo tInfo := i then -- shortcut if it's not a tactic user wrote @@ -207,8 +200,6 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree let infoTreeJson ← (InfoTree.node i PersistentArray.empty).toJson ctx - -- let steps ← prettifySteps tInfo.stx ctx steps - let proofTreeEdges ← getGoalsChange ctx tInfo let currentGoals := proofTreeEdges.map (fun ⟨ _, g₁, gs ⟩ => g₁ :: gs) |>.join let allGoals := allSubGoals.insertMany $ currentGoals @@ -220,15 +211,17 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree let mctxBeforeJson ← MetavarContext.toJson tInfo.mctxBefore ctx let mctxAfterJson ← MetavarContext.toJson tInfo.mctxAfter ctx + let isSimpRw := tInfo.stx.getKind.toString == "Mathlib.Tactic.tacticSimp_rw___" + let newSteps := proofTreeEdges.filterMap fun ⟨ tacticDependsOn, goalBefore, goalsAfter ⟩ => - -- Leave only steps which are not handled in the subtree. - if steps.map (·.goalBefore) |>.elem goalBefore then + -- Leave only steps which are not handled in the subtree. + -- Additionally, simp_rw is not broken down since we are not able to properly transform it's rw steps. + if (steps.map (·.goalBefore) |>.elem goalBefore) && !isSimpRw then none else let range := tInfo.stx.toRange ctx some { tacticString, - syntaxString := tInfo.stx.formatStx.pretty, goalBefore, goalsAfter, mctxBefore := mctxBeforeJson, @@ -240,7 +233,10 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree infoTree := some infoTreeJson } - return { steps := newSteps ++ steps, allGoals } + if isSimpRw then + return { steps := newSteps, allGoals } + else + return { steps := newSteps ++ steps, allGoals } else return { steps, allGoals := allSubGoals } From 89fc83b50785b47855f6078e41734d6d518cbead Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 20 Jun 2025 15:48:47 +0200 Subject: [PATCH 46/47] fix: call prettifySteps. --- REPL/PaperProof/BetterParser.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index db593453..9cf4739e 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -200,6 +200,8 @@ partial def postNode (ctx : ContextInfo) (i : Info) (_: PersistentArray InfoTree let infoTreeJson ← (InfoTree.node i PersistentArray.empty).toJson ctx + steps ← prettifySteps tInfo.stx ctx steps + let proofTreeEdges ← getGoalsChange ctx tInfo let currentGoals := proofTreeEdges.map (fun ⟨ _, g₁, gs ⟩ => g₁ :: gs) |>.join let allGoals := allSubGoals.insertMany $ currentGoals From ad321545a8f07a3b0ef476403f239f687f406b27 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mat=C4=9Bj=20Kripner?= Date: Fri, 20 Jun 2025 17:47:01 +0200 Subject: [PATCH 47/47] Small rw fix. --- REPL/PaperProof/BetterParser.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/REPL/PaperProof/BetterParser.lean b/REPL/PaperProof/BetterParser.lean index 9cf4739e..491dc0f9 100644 --- a/REPL/PaperProof/BetterParser.lean +++ b/REPL/PaperProof/BetterParser.lean @@ -123,9 +123,7 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo let prettify (tStr : String) := let res := tStr.trim.dropRightWhile (· == ',') -- rw puts final rfl on the "]" token - -- TODO: is this correct for `rewrite`? - -- if res == "]" then "rfl" else res - res + if res == "]" then "rfl" else res -- Each part of rw is a separate step none of them include the initial 'rw [' and final ']'. -- So we add these to the first and last steps. let extractRwStep (steps : List ProofStepInfo) (tactic : String) (atClause? : Option Syntax) : IO (List ProofStepInfo) := do @@ -139,8 +137,12 @@ def prettifySteps (stx : Syntax) (ctx : ContextInfo) (steps : List ProofStepInfo -- Turn the `Option String` into a (possibly-empty) string so we can insert it. let maybeAtClause := atClauseStr?.getD "" -- getD "" returns `""` if `atClauseStr?` is `none` - let rwSteps := steps.map fun a => - { a with tacticString := s!"{tactic} [{prettify a.tacticString}]{maybeAtClause}" } + -- rw puts final rfl on the "]" token + -- let rwSteps := (steps.filter (·.tacticString.trim.dropWhile (· == ' ') != "]")).map + -- fun a => { a with tacticString := s!"{tactic} [{prettify a.tacticString}]{maybeAtClause}" } + let rwSteps := steps.map + fun a => { a with tacticString := s!"{tactic} [{prettify a.tacticString}]{maybeAtClause}" } + match rwSteps with | [] =>