diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index d8fa923f4608..eadc464bb990 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -648,13 +648,11 @@ set_option linter.unusedVariables.funArgs false in Auxiliary axiom used to implement the `sorry` term and tactic. The `sorry` term/tactic expands to `sorryAx _ (synthetic := false)`. -This is intended for stubbing out incomplete parts of a proof while still having a syntactically correct proof skeleton. -Lean will give a warning whenever a proof uses `sorry`, so you aren't likely to miss it, -but you can double check if a theorem depends on `sorry` by looking for `sorryAx` in the output +It intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton. +Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it, +but you can double check if a declaration depends on `sorry` by looking for `sorryAx` in the output of the `#print axioms my_thm` command. -"Go to definition" on `sorry` will go to the source position where it was introduced. - The `synthetic` flag is false when written explicitly by the user, but it is set to `true` when a tactic fails to prove a goal, or if there is a type error in the expression. A synthetic `sorry` acts like a regular one, except that it diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 0f5adb4bbb2e..6c38ebe39835 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -403,7 +403,7 @@ syntax (name := acRfl) "ac_rfl" : tactic The `sorry` tactic is a temporary placeholder for an incomplete tactic proof, closing the main goal using `exact sorry`. -This is intended for stubbing out incomplete parts of a proof while still having a syntactically correct proof skeleton. +This is intended for stubbing-out incomplete parts of a proof while still having a syntactically correct proof skeleton. Lean will give a warning whenever a proof uses `sorry`, so you aren't likely to miss it, but you can double check if a theorem depends on `sorry` by looking for `sorryAx` in the output of the `#print axioms my_thm` command, which is the axiom used by implementation of `sorry`. diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean index 38372ebae9da..8d7266314985 100644 --- a/src/Lean/Elab/Extra.lean +++ b/src/Lean/Elab/Extra.lean @@ -578,7 +578,7 @@ def elabDefaultOrNonempty : TermElab := fun stx expectedType? => do else -- It is in the context of an `unsafe` constant. We can use sorry instead. -- Another option is to make a recursive application since it is unsafe. - mkSorry expectedType false + mkUniqueSorry expectedType false builtin_initialize registerTraceClass `Elab.binop diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index d37aa7381743..d57d9490efb1 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -977,7 +977,7 @@ where values.mapM (instantiateMVarsProfiling ·) catch ex => logException ex - headers.mapM fun header => mkSorry header.type (synthetic := true) + headers.mapM fun header => withRef header.declId <| mkUniqueSorry header.type (synthetic := true) let headers ← headers.mapM instantiateMVarsAtHeader let letRecsToLift ← getLetRecsToLift let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 471ad586ea70..cd3f15c26b84 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -20,7 +20,7 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := fa let all := preDefs.toList.map (·.declName) forallTelescope preDef.type fun xs type => do let value ← if useSorry then - mkLambdaFVars xs (← mkSorry type (synthetic := true)) + mkLambdaFVars xs (← withRef preDef.ref <| mkUniqueSorry type (synthetic := true)) else liftM <| mkInhabitantFor preDef.declName xs type addNonRec { preDef with @@ -114,7 +114,7 @@ private partial def ensureNoUnassignedLevelMVarsAtPreDef (preDef : PreDefinition private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM PreDefinition := do let pendingMVarIds ← getMVarsAtPreDef preDef if (← logUnassignedUsingErrorInfos pendingMVarIds) then - let preDef := { preDef with value := (← mkSorry preDef.type (synthetic := true)) } + let preDef := { preDef with value := (← withRef preDef.ref <| mkUniqueSorry preDef.type (synthetic := true)) } if (← getMVarsAtPreDef preDef).isEmpty then return preDef else diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 67cc91c88dcd..0cfcfe7e1c66 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -14,7 +14,7 @@ open Meta def admitGoal (mvarId : MVarId) : MetaM Unit := mvarId.withContext do let mvarType ← inferType (mkMVar mvarId) - mvarId.assign (← mkSorry mvarType (synthetic := true)) + mvarId.assign (← mkUniqueSorry mvarType (synthetic := true)) def goalsToMessageData (goals : List MVarId) : MessageData := MessageData.joinSep (goals.map MessageData.ofGoal) m!"\n\n" diff --git a/src/Lean/Elab/Tactic/LibrarySearch.lean b/src/Lean/Elab/Tactic/LibrarySearch.lean index 56fcfd830316..46e2bbe88b97 100644 --- a/src/Lean/Elab/Tactic/LibrarySearch.lean +++ b/src/Lean/Elab/Tactic/LibrarySearch.lean @@ -70,7 +70,7 @@ def elabExact?Term : TermElab := fun stx expectedType? => do if let some suggestions ← librarySearch introdGoal then if suggestions.isEmpty then logError "`exact?%` didn't find any relevant lemmas" else logError "`exact?%` could not close the goal. Try `by apply` to see partial suggestions." - mkSorry expectedType (synthetic := true) + mkUniqueSorry expectedType (synthetic := true) else addTermSuggestion stx (← instantiateMVars goal).headBeta instantiateMVars goal diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 209c04c596e8..89f60a707410 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1107,7 +1107,7 @@ private def mkSyntheticSorryFor (expectedType? : Option Expr) : TermElabM Expr : let expectedType ← match expectedType? with | none => mkFreshTypeMVar | some expectedType => pure expectedType - mkSorry expectedType (synthetic := true) + mkUniqueSorry expectedType (synthetic := true) /-- Log the given exception, and create a synthetic sorry for representing the failed @@ -1213,7 +1213,7 @@ 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 + withRef tacticCode <| mkUniqueSorry type false else let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque let mvarId := mvar.mvarId! @@ -1769,7 +1769,7 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPo withRef stx <| ensureHasType expectedType? e errorMsgHeader? catch ex => if (← read).errToSorry && ex matches .error .. then - exceptionToSorry ex expectedType? + withRef stx <| exceptionToSorry ex expectedType? else throw ex diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index ef5ab60d0ab7..511460537ce6 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -514,7 +514,7 @@ def mkSome (type value : Expr) : MetaM Expr := do return mkApp2 (mkConst ``Option.some [u]) type value /-- -Return `sorryAx type synthetic`. Recall that `synthetic` is true if this sorry is from an error. +Returns `sorryAx type synthetic`. Recall that `synthetic` is true if this sorry is from an error. -/ def mkSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do let u ← getLevel type @@ -544,7 +544,7 @@ def UniqueSorryView.decode? (name : Name) : Option UniqueSorryView := do failure /-- -Make a `sorryAx` that is unique, in the sense that it is not defeq to any other `sorry` created by `mkUniqueSorry`. +Makes a `sorryAx` that is unique, in the sense that it is not defeq to any other `sorry` created by `mkUniqueSorry`. Encodes the source position of the current ref into the term. -/ @@ -559,7 +559,7 @@ def mkUniqueSorry (type : Expr) (synthetic : Bool) : MetaM Expr := do return .app e (toExpr tag) /-- -Return a `UniqueSorryView` if `e` is an application of an expression returned by `mkUniqueSorry`. +Returns a `UniqueSorryView` if `e` is an application of an expression returned by `mkUniqueSorry`. -/ def isUniqueSorry? (e : Expr) : Option UniqueSorryView := do guard <| e.isAppOf ``sorryAx && e.getAppNumArgs ≥ 3 diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index 71a35af9fd4e..21183a8be37d 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/src/Lean/Meta/Tactic/Util.lean @@ -60,7 +60,7 @@ def _root_.Lean.MVarId.admit (mvarId : MVarId) (synthetic := true) : MetaM Unit mvarId.withContext do mvarId.checkNotAssigned `admit let mvarType ← mvarId.getType - let val ← mkSorry mvarType synthetic + let val ← mkUniqueSorry mvarType synthetic mvarId.assign val /-- Beta reduce the metavariable type head -/ diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 97c1048c0296..f2f82aacd8db 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -218,11 +218,13 @@ def binderIdent : Parser := ident <|> hole /-- The `sorry` term is a temporary placeholder for a missing proof or value. -This is intended for stubbing out incomplete parts of a proof while still having a syntactically correct proof skeleton. -Lean will give a warning whenever a proof uses `sorry`, so you aren't likely to miss it, -but you can double check if a theorem depends on `sorry` by looking for `sorryAx` in the output +The syntax is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton. +Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it, +but you can double check if a declaration depends on `sorry` by looking for `sorryAx` in the output of the `#print axioms my_thm` command, which is the axiom used by implementation of `sorry`. +"Go to definition" on `sorry` will go to the source position where it was introduced. + Each `sorry` is guaranteed to be unique, so for example the following fails: ```lean example : (sorry : Nat) = sorry := rfl -- fails diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index bf0de8759ebd..a5c152de926a 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -212,7 +212,7 @@ where } /-- -Annotates the term with the current expression position and registers `TermInfo` +Annotate the term with the current expression position and register `TermInfo` to associate the term to the current expression. -/ def annotateTermInfo (stx : Term) : Delab := do @@ -221,13 +221,31 @@ def annotateTermInfo (stx : Term) : Delab := do pure stx /-- -Modifies the delaborator so that it annotates the resulting term with the current expression -position and registers `TermInfo` to associate the term to the current expression. +Annotates the term with the current expression position and registers `TermInfo` +to associate the term to the current expression, unless (1) the syntax has a position and it is for the current position +and (2) there is already `TermInfo` at this position. +-/ +def annotateTermInfoUnlessAnnotated (stx : Term) : Delab := do + if let .synthetic ⟨pos⟩ ⟨pos'⟩ := stx.raw.getHeadInfo then + if pos == pos' && pos == (← getPos) then + if (← get).infos.contains pos then + return stx + annotateTermInfo stx + +/-- +Modifies the delaborator so that it annotates the resulting term using `annotateTermInfo`. -/ def withAnnotateTermInfo (d : Delab) : Delab := do let stx ← d annotateTermInfo stx +/-- +Modifies the delaborator so that it ensures resulting term is annotated using `annotateTermInfoUnlessAnnotated`. +-/ +def withAnnotateTermInfoUnlessAnnotated (d : Delab) : Delab := do + let stx ← d + annotateTermInfoUnlessAnnotated stx + def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do -- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here. let suggestion := if suggestion.isAnonymous then `a else suggestion @@ -271,11 +289,13 @@ inductive OmissionReason | deep | proof | maxSteps + | uniqueSorry def OmissionReason.toString : OmissionReason → String | deep => "Term omitted due to its depth (see option `pp.deepTerms`)." | proof => "Proof omitted (see option `pp.proofs`)." | maxSteps => "Term omitted due to reaching the maximum number of steps allowed for pretty printing this expression (see option `pp.maxSteps`)." + | uniqueSorry => "This is a `sorry` term associated to a source position. Use 'Go to definition' to go there." def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit := do let info := Info.ofOmissionInfo <| ← mkOmissionInfo stx e @@ -365,7 +385,7 @@ def omission (reason : OmissionReason) : Delab := do partial def delabFor : Name → Delab | Name.anonymous => failure | k => - (do annotateTermInfo (← (delabAttribute.getValues (← getEnv) k).firstM id)) + (do annotateTermInfoUnlessAnnotated (← (delabAttribute.getValues (← getEnv) k).firstM id)) -- have `app.Option.some` fall back to `app` etc. <|> if k.isAtomic then failure else delabFor k.getRoot diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 81f13404a076..9217b2becd05 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -573,7 +573,7 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do else let delabHead (insertExplicit : Bool) : Delab := do guard <| !insertExplicit - withAnnotateTermInfo x + withAnnotateTermInfoUnlessAnnotated x delabAppCore (n - arity) delabHead (unexpand := false) @[builtin_delab app] @@ -1227,14 +1227,30 @@ def delabNameMkStr : Delab := whenPPOption getPPNotation do def delabNameMkNum : Delab := delabNameMkStr @[builtin_delab app.sorryAx] -def delabSorry : Delab := whenPPOption getPPNotation do +def delabSorry : Delab := whenPPOption getPPNotation <| whenNotPPOption getPPExplicit do guard <| (← getExpr).getAppNumArgs ≥ 2 - let mut arity := 2 -- If this is constructed by `Lean.Meta.mkUniqueSorry`, then don't print the unique tag. - if isUniqueSorry? (← getExpr) |>.isSome then - arity := 3 - withOverApp arity do - `(sorry) + -- But, if `pp.explicit` is false and `pp.sorrySource` is true, then print a simplified version of the tag. + if let some view := isUniqueSorry? (← getExpr) then + withOverApp 3 do + if let (some module, some range) := (view.module?, view.range?) then + if ← getPPOption getPPSorrySource then + -- LSP line numbers start at 0, so add one to it. + -- Technically using the character as the column is incorrect since this is UTF-16 position, but we have no filemap to work with. + let posAsName := Name.mkSimple s!"{module}:{range.start.line + 1}:{range.start.character}" + let pos := mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{posAsName}"] + let src ← withAppArg <| annotateTermInfo pos + `(sorry $src) + else + -- Hack: use omission info so that the first hover gives the sorry source. + let stx ← `(sorry) + let stx ← annotateCurPos stx + addOmissionInfo (← getPos) stx (← getExpr) .uniqueSorry + return stx + else + `(sorry) + else + withOverApp 2 `(sorry) open Parser Command Term in @[run_builtin_parser_attribute_hooks] diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean index 4b3688126156..afbe508339b8 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Options.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean @@ -34,6 +34,11 @@ register_builtin_option pp.match : Bool := { group := "pp" descr := "(pretty printer) disable/enable 'match' notation" } +register_builtin_option pp.sorrySource : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) if true, pretty print 'sorry' with its originating source position, if available" +} register_builtin_option pp.coercions : Bool := { defValue := true group := "pp" @@ -250,6 +255,7 @@ def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o) def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o) def getPPUnicodeFun (o : Options) : Bool := o.get pp.unicode.fun.name false def getPPMatch (o : Options) : Bool := o.get pp.match.name (!getPPAll o) +def getPPSorrySource (o : Options) : Bool := o.get pp.sorrySource.name pp.sorrySource.defValue def getPPFieldNotation (o : Options) : Bool := o.get pp.fieldNotation.name (!getPPAll o) def getPPFieldNotationGeneralized (o : Options) : Bool := o.get pp.fieldNotation.generalized.name pp.fieldNotation.generalized.defValue def getPPStructureInstances (o : Options) : Bool := o.get pp.structureInstances.name (!getPPAll o) diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index c5ed7152e989..231ccafbf5c6 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -151,8 +151,17 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx) let i := ictx.info let ci := ictx.ctx let children := ictx.children - match i with - | .ofTermInfo ti => + + let locationLinksDefault : RequestM (Array LocationLink) := do + -- If other go-tos fail, we try to show the elaborator or parser + if let some ei := i.toElabInfo? then + if kind == declaration && ci.env.contains ei.stx.getKind then + return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind + if kind == definition && ci.env.contains ei.elaborator then + return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator + return #[] + + let locationLinksFromTermInfo (ti : TermInfo) : RequestM (Array LocationLink) := do let mut expr := ti.expr if kind == type then expr ← ci.runMetaM i.lctx do @@ -206,6 +215,11 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx) } results := results.insertAt 0 result return results + locationLinksDefault + + match i with + | .ofTermInfo ti => return ← locationLinksFromTermInfo ti + | .ofOmissionInfo ti => return ← locationLinksFromTermInfo ti.toTermInfo | .ofFieldInfo fi => if kind == type then let expr ← ci.runMetaM i.lctx do @@ -220,13 +234,7 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx) if kind == definition || kind == declaration then return ← ci.runMetaM i.lctx <| locationLinksFromImport i | _ => pure () - -- If other go-tos fail, we try to show the elaborator or parser - if let some ei := i.toElabInfo? then - if kind == declaration && ci.env.contains ei.stx.getKind then - return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind - if kind == definition && ci.env.contains ei.elaborator then - return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator - return #[] + locationLinksDefault open Elab GoToKind in def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams) diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean index 7cd58e70dbfc..65aaa5f3c2bb 100644 --- a/src/Lean/Widget/InteractiveCode.lean +++ b/src/Lean/Widget/InteractiveCode.lean @@ -84,6 +84,7 @@ def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := delabApp else withOptionAtCurrPos pp.proofs.name true do + withOptionAtCurrPos pp.sorrySource.name true do delab let mut e := e -- When hovering over a metavariable, we want to see its value, even if `pp.instantiateMVars` is false.