From 1b6572726fe2418266c5205bda4f0d5573e20229 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 27 Sep 2024 12:00:59 -0700 Subject: [PATCH] feat: have autoparams report parameter/field on failure (#5474) Adds a mechanism where when an autoparam tactic fails to synthesize a parameter, the associated parameter name or field name for the autoparam is reported in an error. Examples: ```text could not synthesize default value for parameter 'h' using tactics could not synthesize default value for field 'inv' of 'S' using tactics ``` Notes: * Autoparams now run their tactics without any error recovery or error-to-sorry enabled. This enables catching the error and reporting the contextual information. This is justified on the grounds that autoparams are not interactive. * Autoparams for applications now cleanup the autoParam annotation, bringing it in line with autoparams for structure fields. * This preserves the old behavior that autoparams leave terminfo, but we will revisit this after some imminent improvements to the unused variable linter. Closes #2950 --- src/Lean/Elab/App.lean | 8 +++-- src/Lean/Elab/BuiltinTerm.lean | 18 +--------- src/Lean/Elab/StructInst.lean | 7 +++- src/Lean/Elab/SyntheticMVars.lean | 27 +++++++++++---- src/Lean/Elab/Tactic/Simp.lean | 2 +- src/Lean/Elab/Term.lean | 31 ++++++++++++++++- tests/lean/interactive/4880.lean.expected.out | 20 +++++++++++ tests/lean/run/autoparam.lean | 33 +++++++++++++++++++ tests/lean/run/mergeSort.lean | 4 +++ 9 files changed, 122 insertions(+), 28 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 373e029f98..d7caaa78c3 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -584,7 +584,6 @@ mutual match evalSyntaxConstant env opts tacticDecl with | Except.error err => throwError err | Except.ok tacticSyntax => - -- TODO(Leo): does this work correctly for tactic sequences? let tacticBlock ← `(by $(⟨tacticSyntax⟩)) /- We insert position information from the current ref into `stx` everywhere, simulating this being @@ -596,7 +595,12 @@ mutual -/ let info := (← getRef).getHeadInfo let tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info) - let argNew := Arg.stx tacticBlock + let mvar ← mkTacticMVar argType.consumeTypeAnnotations tacticBlock (.autoParam argName) + -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`. + -- We should look into removing this since terminfo for synthetic syntax is suspect, + -- but we noted it was necessary to preserve the behavior of the unused variable linter. + addTermInfo' tacticBlock mvar + let argNew := Arg.expr mvar propagateExpectedType argNew elabAndAddNewArg argName argNew main diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index d33a54bb40..38fd868b00 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/src/Lean/Elab/BuiltinTerm.lean @@ -150,26 +150,10 @@ private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do elabTerm b expectedType? | _ => throwUnsupportedSyntax -private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do - let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque - let mvarId := mvar.mvarId! - let ref ← getRef - registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext) - return mvar - -register_builtin_option debug.byAsSorry : Bool := { - defValue := false - group := "debug" - descr := "replace `by ..` blocks with `sorry` IF the expected type is a proposition" -} - @[builtin_term_elab byTactic] def elabByTactic : TermElab := fun stx expectedType? => do match expectedType? with | some expectedType => - if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp expectedType then - mkSorry expectedType false - else - mkTacticMVar expectedType stx + mkTacticMVar expectedType stx .term | none => tryPostpone throwError ("invalid 'by' tactic, expected type has not been provided") diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 220d7b8e91..861d04dd08 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -682,7 +682,12 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term -- We add info to get reliable positions for messages from evaluating the tactic script. let info := field.ref.getHeadInfo let stx := stx.raw.rewriteBottomUp (·.setInfo info) - cont (← elabTermEnsuringType stx (d.getArg! 0).consumeTypeAnnotations) field + let type := (d.getArg! 0).consumeTypeAnnotations + let mvar ← mkTacticMVar type stx (.fieldAutoParam fieldName s.structName) + -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`. + -- (See the aformentioned `processExplicitArg` for a comment about this.) + addTermInfo' stx mvar + cont mvar field | _ => if bi == .instImplicit then let val ← withRef field.ref <| mkFreshExprMVar d .synthetic diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index a5378133af..3e5e25223c 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -316,6 +316,18 @@ def PostponeBehavior.ofBool : Bool → PostponeBehavior | true => .yes | false => .no +private def TacticMVarKind.logError (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Unit := do + match kind with + | term => pure () + | autoParam argName => logErrorAt tacticCode m!"could not synthesize default value for parameter '{argName}' using tactics" + | fieldAutoParam fieldName structName => logErrorAt tacticCode m!"could not synthesize default value for field '{fieldName}' of '{structName}' using tactics" + +private def TacticMVarKind.maybeWithoutRecovery (kind : TacticMVarKind) (m : TacticM α) : TacticM α := do + if kind matches .autoParam .. | .fieldAutoParam .. then + withoutErrToSorry <| Tactic.withoutRecover <| m + else + m + mutual /-- @@ -325,7 +337,7 @@ mutual If `report := false`, then `runTactic` will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions. -/ - partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do + partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (kind : TacticMVarKind) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do instantiateMVarDeclMVars mvarId /- TODO: consider using `runPendingTacticsAt` at `mvarId` local context and target type. @@ -342,7 +354,7 @@ mutual in more complicated scenarios. -/ tryCatchRuntimeEx - (do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do + (do let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId <| kind.maybeWithoutRecovery do withTacticInfoContext tacticCode do -- also put an info node on the `by` keyword specifically -- the token may be `canonical` and thus shown in the info -- view even though it is synthetic while a node like `tacticCode` never is (#1990) @@ -354,10 +366,13 @@ mutual synthesizeSyntheticMVars (postpone := .no) unless remainingGoals.isEmpty do if report then + kind.logError tacticCode reportUnsolvedGoals remainingGoals else throwError "unsolved goals\n{goalsToMessageData remainingGoals}") fun ex => do + if report then + kind.logError tacticCode if report && (← read).errToSorry then for mvarId in (← getMVars (mkMVar mvarId)) do mvarId.admit @@ -385,10 +400,10 @@ mutual return false -- NOTE: actual processing at `synthesizeSyntheticMVarsAux` | .postponed savedContext => resumePostponed savedContext mvarSyntheticDecl.stx mvarId postponeOnError - | .tactic tacticCode savedContext => + | .tactic tacticCode savedContext kind => withSavedContext savedContext do if runTactics then - runTactic mvarId tacticCode + runTactic mvarId tacticCode kind return true else return false @@ -529,9 +544,9 @@ the result of a tactic block. def runPendingTacticsAt (e : Expr) : TermElabM Unit := do for mvarId in (← getMVars e) do let mvarId ← getDelayedMVarRoot mvarId - if let some { kind := .tactic tacticCode savedContext, .. } ← getSyntheticMVarDecl? mvarId then + if let some { kind := .tactic tacticCode savedContext kind, .. } ← getSyntheticMVarDecl? mvarId then withSavedContext savedContext do - runTactic mvarId tacticCode + runTactic mvarId tacticCode kind markAsResolved mvarId builtin_initialize diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 2ac90f8935..eca414db66 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -47,7 +47,7 @@ def tacticToDischarge (tacticCode : Syntax) : TacticM (IO.Ref Term.State × Simp -/ withoutModifyingStateWithInfoAndMessages do Term.withSynthesize (postpone := .no) do - Term.runTactic (report := false) mvar.mvarId! tacticCode + Term.runTactic (report := false) mvar.mvarId! tacticCode .term let result ← instantiateMVars mvar if result.hasExprMVar then return none diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index d04bab8342..78593be5d0 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -29,6 +29,15 @@ structure SavedContext where errToSorry : Bool levelNames : List Name +/-- The kind of a tactic metavariable, used for additional error reporting. -/ +inductive TacticMVarKind + /-- Standard tactic metavariable, arising from `by ...` syntax. -/ + | term + /-- Tactic metavariable arising from an autoparam for a function application. -/ + | autoParam (argName : Name) + /-- Tactic metavariable arising from an autoparam for a structure field. -/ + | fieldAutoParam (fieldName structName : Name) + /-- We use synthetic metavariables as placeholders for pending elaboration steps. -/ inductive SyntheticMVarKind where /-- @@ -43,7 +52,7 @@ inductive SyntheticMVarKind where Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/ | coe (header? : Option String) (expectedType : Expr) (e : Expr) (f? : Option Expr) /-- Use tactic to synthesize value for metavariable. -/ - | tactic (tacticCode : Syntax) (ctx : SavedContext) + | tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind) /-- Metavariable represents a hole whose elaboration has been postponed. -/ | postponed (ctx : SavedContext) deriving Inhabited @@ -1191,6 +1200,26 @@ private def postponeElabTermCore (stx : Syntax) (expectedType? : Option Expr) : def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) := return (← get).syntheticMVars.find? mvarId +register_builtin_option debug.byAsSorry : Bool := { + defValue := false + group := "debug" + descr := "replace `by ..` blocks with `sorry` IF the expected type is a proposition" +} + +/-- +Creates a new metavariable of type `type` that will be synthesized using the tactic code. +The `tacticCode` syntax is the full `by ..` syntax. +-/ +def mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind) : TermElabM Expr := do + if ← pure (debug.byAsSorry.get (← getOptions)) <&&> isProp type then + mkSorry type false + else + let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque + let mvarId := mvar.mvarId! + let ref ← getRef + registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext) kind + return mvar + /-- Create an auxiliary annotation to make sure we create an `Info` even if `e` is a metavariable. See `mkTermInfo`. diff --git a/tests/lean/interactive/4880.lean.expected.out b/tests/lean/interactive/4880.lean.expected.out index bea1021183..88d320c447 100644 --- a/tests/lean/interactive/4880.lean.expected.out +++ b/tests/lean/interactive/4880.lean.expected.out @@ -2,6 +2,16 @@ "uri": "file:///4880.lean", "diagnostics": [{"source": "Lean 4", + "severity": 1, + "range": + {"start": {"line": 16, "character": 12}, + "end": {"line": 16, "character": 17}}, + "message": + "could not synthesize default value for field 'h1' of 'B' using tactics", + "fullRange": + {"start": {"line": 16, "character": 12}, + "end": {"line": 16, "character": 17}}}, + {"source": "Lean 4", "severity": 1, "range": {"start": {"line": 16, "character": 12}, @@ -11,6 +21,16 @@ "fullRange": {"start": {"line": 16, "character": 12}, "end": {"line": 16, "character": 17}}}, + {"source": "Lean 4", + "severity": 1, + "range": + {"start": {"line": 22, "character": 17}, + "end": {"line": 22, "character": 20}}, + "message": + "could not synthesize default value for parameter '_h1' using tactics", + "fullRange": + {"start": {"line": 22, "character": 17}, + "end": {"line": 22, "character": 20}}}, {"source": "Lean 4", "severity": 1, "range": diff --git a/tests/lean/run/autoparam.lean b/tests/lean/run/autoparam.lean index 31fda18ba3..7dd13506a9 100644 --- a/tests/lean/run/autoparam.lean +++ b/tests/lean/run/autoparam.lean @@ -1,3 +1,6 @@ +/-! +# Testing the autoparam feature +-/ def f (x y : Nat) (h : x = y := by assumption) : Nat := x + x @@ -13,3 +16,33 @@ x + x #check fun x => f2 x x #check fun x => f3 x x + +/-- +error: could not synthesize default value for parameter 'h' using tactics +--- +error: tactic 'assumption' failed +⊢ 1 = 2 +-/ +#guard_msgs in example := f 1 2 + +/-! +From #2950, field autoparam should mention which field failed. +-/ + +structure Foo where + val : String + len : Nat := val.length + inv : val.length = len := by next => decide + +/-- +error: could not synthesize default value for field 'inv' of 'Foo' using tactics +--- +error: tactic 'decide' proved that the proposition + "abc".length = 5 +is false +-/ +#guard_msgs in +def test2 : Foo := { + val := "abc" + len := 5 +} diff --git a/tests/lean/run/mergeSort.lean b/tests/lean/run/mergeSort.lean index 954bfa156a..2215f56327 100644 --- a/tests/lean/run/mergeSort.lean +++ b/tests/lean/run/mergeSort.lean @@ -37,6 +37,8 @@ inductive NoLE | mk : NoLE /-- +error: could not synthesize default value for parameter 'le' using tactics +--- error: failed to synthesize LE NoLE Additional diagnostic information may be available using the `set_option diagnostics true` command. @@ -51,6 +53,8 @@ instance : LE UndecidableLE where le := fun _ _ => true /-- +error: could not synthesize default value for parameter 'le' using tactics +--- error: type mismatch a ≤ b has type