From f9dc2fb408cf319aa2f20511c28cf44c50ca40dd Mon Sep 17 00:00:00 2001 From: Auguste Poiroux Date: Fri, 3 Jan 2025 01:42:11 +0100 Subject: [PATCH] Add a `rootGoals` option to instantiate synthetic sorries from declarations root goal - Useful for people experimenting with automated provers. Example usage: run a lean file from the MiniF2F benchmark, and get sorries even if there already exist proofs. Similar to LeanDojo, but without having to trace the project. - Fix: add rootGoals for proof states extracted by the `tactics` method --- REPL/JSON.lean | 1 + REPL/Lean/InfoTree.lean | 51 ++++++++++++++++++++---- REPL/Main.lean | 29 +++++++++----- REPL/Snapshots.lean | 12 +++--- test/root_goals.expected.out | 20 ++++++++++ test/root_goals.in | 6 +++ test/self_proof_apply_check.expected.out | 25 ++++++++++++ test/self_proof_apply_check.in | 5 +++ test/self_proof_check.expected.out | 14 ++++--- test/self_proof_check.in | 5 ++- test/self_proof_exact_check.expected.out | 14 +++---- test/self_proof_exact_check.in | 5 +-- 12 files changed, 145 insertions(+), 42 deletions(-) create mode 100644 test/root_goals.expected.out create mode 100644 test/root_goals.in create mode 100644 test/self_proof_apply_check.expected.out create mode 100644 test/self_proof_apply_check.in diff --git a/REPL/JSON.lean b/REPL/JSON.lean index 5398c4e..24db840 100644 --- a/REPL/JSON.lean +++ b/REPL/JSON.lean @@ -13,6 +13,7 @@ namespace REPL structure CommandOptions where allTactics : Option Bool := none + rootGoals : Option Bool := none /-- Should be "full", "tactics", "original", or "substantive". Anything else is ignored. diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean index 88ec289..6f9ce86 100644 --- a/REPL/Lean/InfoTree.lean +++ b/REPL/Lean/InfoTree.lean @@ -164,16 +164,44 @@ partial def findAllInfo (t : InfoTree) (ctx? : Option ContextInfo) (p : Info → info ++ rest | _ => [] +/-- Analogue of `Lean.Elab.InfoTree.findAllInfo` but specialized to `TacticInfo` to return root goals. -/ +partial def findAllInfoTactics (t : InfoTree) (ctx? : Option ContextInfo) (rootGoals : List MVarId) : + List (Info × Option ContextInfo × List MVarId) := + match t with + | .context ctx t => t.findAllInfoTactics (ctx.mergeIntoOuter? ctx?) rootGoals + | .node info ts => + let tInfo := match info with + | .ofTacticInfo i => + if info.isOriginal && i.isSubstantive then + let rootGoals := if rootGoals.isEmpty then i.goalsBefore else rootGoals + [(info, ctx?, rootGoals)] + else + [] + | _ => [] + tInfo ++ ts.toList.flatMap (fun t => t.findAllInfoTactics ctx? rootGoals) + | _ => [] + /-- Return all `TacticInfo` nodes in an `InfoTree` with "original" syntax, each equipped with its relevant `ContextInfo`. -/ -def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo) := - let infos := t.findAllInfo none fun i => match i with - | .ofTacticInfo i' => i.isOriginal && i'.isSubstantive - | _ => false +def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo × List MVarId) := + let infos := t.findAllInfoTactics none [] infos.filterMap fun p => match p with - | (.ofTacticInfo i, some ctx) => (i, ctx) + | (.ofTacticInfo i, some ctx, rootGoals) => (i, ctx, rootGoals) | _ => none +partial def findRootGoals (t : InfoTree) (ctx? : Option ContextInfo := none) : + List (TacticInfo × ContextInfo × List MVarId) := + match t with + | .context ctx t => t.findRootGoals (ctx.mergeIntoOuter? ctx?) + | .node info ts => + match info with + | .ofTacticInfo i => + match ctx? with + | some ctx => [(i, ctx, i.goalsBefore)] + | _ => [] + | _ => ts.toList.flatMap (fun t => t.findRootGoals ctx?) + | _ => [] + /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to explicit invocations of the `sorry` tactic, each equipped with its relevant `ContextInfo`. -/ @@ -216,17 +244,24 @@ def sorries (t : InfoTree) : List (ContextInfo × SorryType × Position × Posit (t.findSorryTermNodes.map fun ⟨i, ctx⟩ => (ctx, .term i.lctx i.expectedType?, stxRange ctx.fileMap i.stx)) -def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × Position × Position × Array Name) := +def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × List MVarId × Position × Position × Array Name) := -- HACK: creating a child ngen - t.findTacticNodes.map fun ⟨i, ctx⟩ => + t.findTacticNodes.map fun ⟨i, ctx, rootGoals⟩ => let range := stxRange ctx.fileMap i.stx ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, i.stx, + rootGoals, i.goalsBefore, range.fst, range.snd, i.getUsedConstantsAsSet.toArray ) +def rootGoals (t : InfoTree) : List (ContextInfo × List MVarId × Position) := + t.findRootGoals.map fun ⟨i, ctx, rootGoals⟩ => + let range := stxRange ctx.fileMap i.stx + ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, + rootGoals, + range.fst ) end Lean.Elab.InfoTree @@ -281,7 +316,7 @@ namespace Lean.Elab.InfoTree Finds all tactic invocations in an `InfoTree`, ignoring structuring tactics (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/ -def substantiveTactics (t : InfoTree) : List (TacticInfo × ContextInfo) := +def substantiveTactics (t : InfoTree) : List (TacticInfo × ContextInfo × List MVarId) := t.findTacticNodes.filter fun i => i.1.isSubstantive end Lean.Elab.InfoTree diff --git a/REPL/Main.lean b/REPL/Main.lean index ca05d94..aa11588 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -94,7 +94,7 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do modify fun s => { s with proofStates := s.proofStates.push proofState } return id -def sorries (trees : List InfoTree) (env? : Option Environment) (initGoals? : Option (List MVarId)) +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 | .term _ none => false @@ -102,10 +102,10 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (initGoals? : Op fun ⟨ctx, g, pos, endPos⟩ => do let (goal, proofState) ← match g with | .tactic g => do - let s ← ProofSnapshot.create ctx none env? [g] initGoals? + let s ← ProofSnapshot.create ctx none env? [g] rootGoals? pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) | .term lctx (some t) => do - let s ← ProofSnapshot.create ctx lctx env? [] initGoals? [t] + let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t] pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s) | .term _ none => unreachable! let proofStateId ← proofState.mapM recordProofSnapshot @@ -119,19 +119,27 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format := def tactics (trees : List InfoTree) : M m (List Tactic) := trees.flatMap InfoTree.tactics |>.mapM - fun ⟨ctx, stx, goals, pos, endPos, ns⟩ => do - let proofState := some (← ProofSnapshot.create ctx none none goals) + fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do + let proofState := some (← ProofSnapshot.create ctx none none goals rootGoals) let goals := s!"{(← ctx.ppGoals goals)}".trim let tactic := Format.pretty (← ppTactic ctx stx) let proofStateId ← proofState.mapM recordProofSnapshot return Tactic.of goals tactic pos endPos proofStateId ns -/-- Inspired from LeanDojo REPL. -/ +def rootGoals (trees : List InfoTree) : M m (List Sorry) := do + trees.flatMap InfoTree.rootGoals |>.mapM + fun ⟨ctx, goals, pos⟩ => do + let proofState := some (← ProofSnapshot.create ctx none none goals goals) + let goals := s!"{(← ctx.ppGoals goals)}".trim + let proofStateId ← proofState.mapM recordProofSnapshot + return Sorry.of goals pos pos proofStateId + +/-- Get the status of the whole proof up to this point. Inspired from LeanDojo REPL. -/ def getProofStatus (proofState : ProofSnapshot) : M m String := do match proofState.tacticState.goals with | [] => let res := proofState.runMetaM do - match proofState.initialGoals with + match proofState.rootGoals with | [goalId] => match proofState.metaState.mctx.getExprAssignmentCore? goalId with | none => return "Error: Goal not assigned" @@ -147,7 +155,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do name := Name.anonymous, type := pft, value := pf, - levelParams := [], + levelParams := (collectLevelParams {} pft).params.toList, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe }) @@ -178,7 +186,7 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap | none => pure trees -- For debugging purposes, sometimes we print out the trees here: -- trees.forM fun t => do IO.println (← t.format) - let sorries ← sorries trees none (some proofState.initialGoals) + let sorries ← sorries trees none (some proofState.rootGoals) let id ← recordProofSnapshot proofState return { proofState := id @@ -243,6 +251,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do -- For debugging purposes, sometimes we print out the trees here: -- trees.forM fun t => do IO.println (← t.format) let sorries ← sorries trees (initialCmdState?.map (·.env)) none + let sorries ← match s.rootGoals with + | some true => pure (sorries ++ (← rootGoals trees)) + | _ => pure sorries let tactics ← match s.allTactics with | some true => tactics trees | _ => pure [] diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index bed5521..1cb991f 100644 --- a/REPL/Snapshots.lean +++ b/REPL/Snapshots.lean @@ -108,7 +108,7 @@ structure ProofSnapshot where termContext : Term.Context tacticState : Tactic.State tacticContext : Tactic.Context - initialGoals : List MVarId + rootGoals : List MVarId namespace ProofSnapshot @@ -192,7 +192,7 @@ For convenience, we also allow a list of `Expr`s, and these are appended to the as fresh metavariables with the given types. -/ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment) - (goals : List MVarId) (initGoals? : Option (List MVarId)) (types : List Expr := []) + (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := []) : IO ProofSnapshot := do ctx.runMetaM (lctx?.getD {}) do let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t)) @@ -209,7 +209,7 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Envi termContext := {} tacticState := { goals } tacticContext := { elaborator := .anonymous } - initialGoals := match initGoals? with + rootGoals := match rootGoals? with | none => goals | some gs => gs } @@ -276,7 +276,7 @@ def pickle (p : ProofSnapshot) (path : FilePath) : IO Unit := do ({ p'.termContext with } : CompactableTermContext), p'.tacticState, p'.tacticContext, - p'.initialGoals) + p'.rootGoals) /-- Unpickle a `ProofSnapshot`. @@ -284,7 +284,7 @@ Unpickle a `ProofSnapshot`. def unpickle (path : FilePath) (cmd? : Option CommandSnapshot) : IO (ProofSnapshot × CompactedRegion) := unsafe do let ((imports, map₂, coreState, coreContext, metaState, metaContext, termState, termContext, - tacticState, tacticContext, initialGoals), region) ← + tacticState, tacticContext, rootGoals), region) ← _root_.unpickle (Array Import × PHashMap Name ConstantInfo × CompactableCoreState × Core.Context × Meta.State × CompactableMetaContext × Term.State × CompactableTermContext × Tactic.State × Tactic.Context × List MVarId) path @@ -303,7 +303,7 @@ def unpickle (path : FilePath) (cmd? : Option CommandSnapshot) : termContext := { termContext with } tacticState tacticContext - initialGoals } + rootGoals } let (_, p'') ← p'.runCoreM do for o in ← getOpenDecls do if let .simple ns _ := o then diff --git a/test/root_goals.expected.out b/test/root_goals.expected.out new file mode 100644 index 0000000..053aeea --- /dev/null +++ b/test/root_goals.expected.out @@ -0,0 +1,20 @@ +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 17}, + "goal": "⊢ 1 = 1", + "endPos": {"line": 1, "column": 17}}, + {"proofState": 1, + "pos": {"line": 5, "column": 22}, + "goal": "⊢ 1 + 1 = 2", + "endPos": {"line": 5, "column": 22}}], + "messages": + [{"severity": "info", + "pos": {"line": 3, "column": 2}, + "endPos": {"line": 3, "column": 8}, + "data": "Try this: exact rfl"}], + "env": 0} + +{"proofStatus": "Completed", "proofState": 2, "goals": []} + +{"proofStatus": "Completed", "proofState": 3, "goals": []} + diff --git a/test/root_goals.in b/test/root_goals.in new file mode 100644 index 0000000..487ad72 --- /dev/null +++ b/test/root_goals.in @@ -0,0 +1,6 @@ +{"cmd": "example : 1=1 := by\n skip\n exact?\n\ntheorem bb : 1+1=2 := by rfl", "rootGoals": true} + +{"proofState" : 0, "tactic": "rfl"} + +{"proofState" : 1, "tactic": "exact rfl"} + diff --git a/test/self_proof_apply_check.expected.out b/test/self_proof_apply_check.expected.out new file mode 100644 index 0000000..ba526f4 --- /dev/null +++ b/test/self_proof_apply_check.expected.out @@ -0,0 +1,25 @@ +{"messages": + [{"severity": "error", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 10}, + "data": + "fail to show termination for\n ex\nwith errors\nfailed to infer structural recursion:\nno parameters suitable for structural recursion\n\nwell-founded recursion cannot be used, 'ex' does not take any (non-fixed) arguments"}], + "env": 0} + +{"sorries": + [{"proofState": 0, + "pos": {"line": 1, "column": 22}, + "goal": "⊢ False", + "endPos": {"line": 1, "column": 27}}], + "messages": + [{"severity": "warning", + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 10}, + "data": "declaration uses 'sorry'"}], + "env": 1} + +{"proofStatus": + "Error: kernel type check failed: (kernel) declaration has free variables '[anonymous]'", + "proofState": 1, + "goals": []} + diff --git a/test/self_proof_apply_check.in b/test/self_proof_apply_check.in new file mode 100644 index 0000000..f01ccc4 --- /dev/null +++ b/test/self_proof_apply_check.in @@ -0,0 +1,5 @@ +{"cmd": "theorem ex : False := by apply ex"} + +{"cmd": "theorem ex : False := sorry"} + +{"proofState": 0, "tactic": "apply ex"} diff --git a/test/self_proof_check.expected.out b/test/self_proof_check.expected.out index ba526f4..aaa3965 100644 --- a/test/self_proof_check.expected.out +++ b/test/self_proof_check.expected.out @@ -1,9 +1,9 @@ {"messages": [{"severity": "error", - "pos": {"line": 1, "column": 8}, - "endPos": {"line": 1, "column": 10}, + "pos": {"line": 1, "column": 25}, + "endPos": {"line": 1, "column": 31}, "data": - "fail to show termination for\n ex\nwith errors\nfailed to infer structural recursion:\nno parameters suitable for structural recursion\n\nwell-founded recursion cannot be used, 'ex' does not take any (non-fixed) arguments"}], + "`exact?` could not close the goal. Try `apply?` to see partial suggestions."}], "env": 0} {"sorries": @@ -18,8 +18,12 @@ "data": "declaration uses 'sorry'"}], "env": 1} -{"proofStatus": - "Error: kernel type check failed: (kernel) declaration has free variables '[anonymous]'", +{"proofStatus": "Incomplete: contains sorry", "proofState": 1, + "messages": + [{"severity": "info", + "pos": {"line": 0, "column": 0}, + "endPos": {"line": 0, "column": 0}, + "data": "`exact?` could not close the goal. Try `apply?` to see partial suggestions."}], "goals": []} diff --git a/test/self_proof_check.in b/test/self_proof_check.in index aa1dac4..3a76200 100644 --- a/test/self_proof_check.in +++ b/test/self_proof_check.in @@ -1,5 +1,6 @@ -{"cmd": "theorem ex : False := by exact ex"} +{"cmd": "theorem ex : False := by exact?"} {"cmd": "theorem ex : False := sorry"} -{"proofState": 0, "tactic": "exact ex"} +{"proofState": 0, "tactic": "exact?"} + diff --git a/test/self_proof_exact_check.expected.out b/test/self_proof_exact_check.expected.out index aaa3965..ba526f4 100644 --- a/test/self_proof_exact_check.expected.out +++ b/test/self_proof_exact_check.expected.out @@ -1,9 +1,9 @@ {"messages": [{"severity": "error", - "pos": {"line": 1, "column": 25}, - "endPos": {"line": 1, "column": 31}, + "pos": {"line": 1, "column": 8}, + "endPos": {"line": 1, "column": 10}, "data": - "`exact?` could not close the goal. Try `apply?` to see partial suggestions."}], + "fail to show termination for\n ex\nwith errors\nfailed to infer structural recursion:\nno parameters suitable for structural recursion\n\nwell-founded recursion cannot be used, 'ex' does not take any (non-fixed) arguments"}], "env": 0} {"sorries": @@ -18,12 +18,8 @@ "data": "declaration uses 'sorry'"}], "env": 1} -{"proofStatus": "Incomplete: contains sorry", +{"proofStatus": + "Error: kernel type check failed: (kernel) declaration has free variables '[anonymous]'", "proofState": 1, - "messages": - [{"severity": "info", - "pos": {"line": 0, "column": 0}, - "endPos": {"line": 0, "column": 0}, - "data": "`exact?` could not close the goal. Try `apply?` to see partial suggestions."}], "goals": []} diff --git a/test/self_proof_exact_check.in b/test/self_proof_exact_check.in index 3a76200..aa1dac4 100644 --- a/test/self_proof_exact_check.in +++ b/test/self_proof_exact_check.in @@ -1,6 +1,5 @@ -{"cmd": "theorem ex : False := by exact?"} +{"cmd": "theorem ex : False := by exact ex"} {"cmd": "theorem ex : False := sorry"} -{"proofState": 0, "tactic": "exact?"} - +{"proofState": 0, "tactic": "exact ex"}