-
Notifications
You must be signed in to change notification settings - Fork 415
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: labeled and unique sorries #5757
base: master
Are you sure you want to change the base?
Conversation
Mathlib CI status (docs):
|
5ea2192
to
1efdc9c
Compare
Nice! I'm curious how this interacts with |
Interesting idea @alexkeizer! That wasn't the plan, but I'll look into it. Maybe it would be better to have a In the current implementation, the |
I should clarify, I think I'd prefer the unique names don't show up in Granted, 99% of the time we use the Having a separate |
@alexkeizer These unique sorries just pretty print as |
Motivation: `sorry` should have an indeterminate value so that it's harder to make "fake" theorems about stubbed-out definitions. This PR makes each instance of `sorry` be non-defeq to any other. For example, this now fails: ```lean example : (sorry : Nat) = sorry := rfl -- fails ``` However, this still succeeds: ```lean def f (n : Nat) : Nat := sorry example : f 0 = f 1 := rfl -- succeeds ``` One can be more careful by putting variables to the right of the colon: ```lean def f : (n : Nat) → Nat := sorry example : f 0 = f 1 := rfl -- fails ``` Details: Adds `Lean.Meta.mkUniqueSorry`, which creates a sorry that is not defeq to any other sorry. It also encodes the source position into the term. Makes the `sorry` term and `sorry` tactic create unique sorries. Adds support to the LSP so that "go to definition" on `sorry` in the Infoview goes to the origin of that particular `sorry`. Fixes `sorry` pretty printing: no more `sorryAx` in the Infoview. Removes `Lean.Meta.mkSyntheticSorry` in favor of `Lean.Meta.mkSorry`.
…tion errors can compound the issues. In any case, they can still be labeled. improves addPPExplicitToExposeDiff when functions are overapplied fixes mdata bugs in location RPC handler fixes leanprover#4972
@@ -151,12 +151,21 @@ def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx) | |||
let i := ictx.info | |||
let ci := ictx.ctx | |||
let children := ictx.children | |||
match i with | |||
| .ofTermInfo ti => | |||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@mhuisi Can I ask you to take a look at my changes here? I refactored it a bit, added some consumeMData
s that avoid some issues, but also add in specific handling for sorry
, which is awkward.
I'm wondering it would be better if TermInfo/OmissionInfo would include an optional source position field. Maybe this could be deferred until we finally make a separate TermInfo-like type for delaboration?
Lean.Widget.TaggedText.tag | ||
{ subexprPos := "/1", diffStatus? := none } | ||
(Lean.Widget.TaggedText.text "True")]), | ||
{ goals := #[{ type := Lean.Widget.TaggedText.append |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@Vtec234 I wanted to flag that this test changed. I modified how the delaborator adds terminfo — it now doesn't add terminfo to syntax that already has it. I haven't really gotten to the bottom of why this test has changed though. If you find it to be worrisome, I'll spend more time trying to figure it out. The infoview seems to have the same diffs at least.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the top-level expression not being tagged anymore might mean that it can no longer be selected with shift-click. Are you able to select it?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, I see some divergence in hovers. (Strangely, it's that in ∀ (x : Nat), x = x → True
, the x = x → True
lost its tag.) I'll aim for getting this PR to preserve this test file.
Motivation:
sorry
should have an indeterminate value so that it's harder to make "fake" theorems about stubbed-out definitions. This PR makes it possible for each instance ofsorry
be non-defeq to any other. For example, this now fails:However, this still succeeds, since the
sorry
is a single indeterminateNat
:One can be more careful by putting parameters to the right of the colon:
Most sources of synthetic sorries are now unique, except for elaboration errors. Making these unique tend to cause confusing cascading errors.
In general though, sorries are labeled. This enables "go to definition" on
sorry
in the Infoview, which brings you to its origin.Details:
Adds
Lean.Meta.mkLabeledSorry
, which creates a sorry that is labeled with its source position. For example,(sorry : Nat)
might elaborate toIt can either be made unique (like the above) or merely labeled.
Makes the
sorry
term, thesorry
tactic, and every elaboration failure create labeled sorries. Most are unique sorries, but some elaboration errors are labeled sorries.Adds support to the LSP so that "go to definition" on
sorry
in the Infoview goes to the origin of that particularsorry
.Makes hovering over a labeled
sorry
show something friendlier than that fullsorryAx
expression. Instead, the first hover shows the simplifiedsorry `«lean.foo:48:11»
. Hovering over that hover shows the fullsorryAx
. Settingset_option pp.sorrySource true
makessorry
always print with this source position information.Removes
Lean.Meta.mkSyntheticSorry
in favor ofLean.Meta.mkSorry
.Changes
sorryAx
so that thesynthetic
argument is no longer optional.Improves
addPPExplicitToExposeDiff
to handle "over-applied" functions.Fixes a number of delaborators so that they respond to
pp.explicit
.Modifies delaborator framework so that delaborators can set Info themselves without it being overwritten.
Incidentally closes #4972.
Inspired by this Zulip thread.