feat: labeled and unique sorries #5757

kmill · 2024-10-17T23:03:42Z

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 of sorry be non-defeq to any other. For example, this now fails:

example : (sorry : Nat) = sorry := rfl -- fails

However, this still succeeds, since the sorry is a single indeterminate Nat:

def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds

One can be more careful by putting parameters to the right of the colon:

def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails

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 to
```
sorryAx (Lean.Name → Nat) false `lean.foo.47.11.47.16._unique_sorry._@.lean.foo._hyg.33
```
It can either be made unique (like the above) or merely labeled.
Makes the sorry term, the sorry 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 particular sorry.
Makes hovering over a labeled sorry show something friendlier than that full sorryAx expression. Instead, the first hover shows the simplified sorry `«lean.foo:48:11». Hovering over that hover shows the full sorryAx. Setting set_option pp.sorrySource true makes sorry always print with this source position information.
Removes Lean.Meta.mkSyntheticSorry in favor of Lean.Meta.mkSorry.
Changes sorryAx so that the synthetic 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.

leanprover-community-bot · 2024-10-17T23:22:27Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d6a7eb3987c612fed2df8a986883a079f7cefcfe --onto 3a34a8e0d119d8a907614af62b405d85149672f0. (2024-10-17 23:22:27)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1d66ff82318a8597f5203e8745d3e77b7f975f70 --onto 3a34a8e0d119d8a907614af62b405d85149672f0. (2024-10-18 02:29:03)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fd15d8f9ed4c8e196e86a316f99e92fc80a74d15 --onto 3a34a8e0d119d8a907614af62b405d85149672f0. (2024-10-18 03:33:58)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fd15d8f9ed4c8e196e86a316f99e92fc80a74d15 --onto 682173d7c084de77bd948b458ef9a7bf48bcb34e. (2024-10-19 21:34:44)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 76164b284b0769672d8a643c4396356a6f053fba --onto 8151ac79d66e7990d5bf5e1b71f8a33aec7d6446. (2024-10-21 22:10:43)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 76164b284b0769672d8a643c4396356a6f053fba --onto f752ce2db94892fe70686730fb594bc6e7da5159. (2024-10-23 05:50:20)

alexkeizer · 2024-10-19T18:19:07Z

Nice! I'm curious how this interacts with #print axioms. Will each unique sorry show up independently?

kmill · 2024-10-19T18:30:02Z

Interesting idea @alexkeizer! That wasn't the plan, but I'll look into it. Maybe it would be better to have a #print sorries command?

In the current implementation, the sorryAx still appears like usual, but what's unique is that it's given a unique Lean.Name argument. So, #print axioms still prints sorryAx.

alexkeizer · 2024-10-19T21:18:39Z

I should clarify, I think I'd prefer the unique names don't show up in #print axioms, as it'd might make it harder to check for axioms with a #guard_msgs in #print axioms line. At least, I'm assuming that the name is derived from the line-number of the sorry, and thus that the output of #print axioms would become more brittle.

Granted, 99% of the time we use the #guard_msgs in #print axioms pattern to assert that there's no sorries, so in reality it's not a big deal either way.

Having a separate #print sorries could be useful, though!

kmill · 2024-10-19T21:53:51Z

@alexkeizer These unique sorries just pretty print as sorry, unless you set set_option pp.sorrySource. It could work by having some number of sorrys in the output rather than just a single sorryAx, and the benefit is you can "go to definition" on each of these to see where they come from. I won't touch #print axioms in this PR though.

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

kmill · 2024-10-23T05:33:01Z

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -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 =>
+


@mhuisi Can I ask you to take a look at my changes here? I refactored it a bit, added some consumeMDatas 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?

kmill · 2024-10-23T05:38:34Z

tests/lean/interactive/Diff.lean.expected.out

-                             Lean.Widget.TaggedText.tag
-                               { subexprPos := "/1", diffStatus? := none }
-                               (Lean.Widget.TaggedText.text "True")]),
+{ goals := #[{ type := Lean.Widget.TaggedText.append


@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.

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?

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.

kmill requested review from mhuisi, Kha and tydeu as code owners October 17, 2024 23:03

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 17, 2024

kmill force-pushed the unique_sorry branch 2 times, most recently from 5ea2192 to 1efdc9c Compare October 18, 2024 03:17

kmill requested review from Vtec234, leodemoura and kim-em as code owners October 19, 2024 21:14

kmill added 4 commits October 21, 2024 10:14

pervasive mkUniqueSorry

3e91655

unique -> labeled sorries. Turns out using unique sorries for elabora…

64b2f32

…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

fix tests

c666fbc

kmill force-pushed the unique_sorry branch from a58b494 to c666fbc Compare October 21, 2024 21:45

revert comment

051b236

kmill changed the title ~~feat: unique sorries~~ feat: labeled and unique sorries Oct 21, 2024

more unique

bcfced4

kmill commented Oct 23, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: labeled and unique sorries #5757

feat: labeled and unique sorries #5757

kmill commented Oct 17, 2024 •

edited

Loading

leanprover-community-bot commented Oct 17, 2024 •

edited

Loading

alexkeizer commented Oct 19, 2024

kmill commented Oct 19, 2024

alexkeizer commented Oct 19, 2024 •

edited

Loading

kmill commented Oct 19, 2024 •

edited

Loading

kmill Oct 23, 2024

kmill Oct 23, 2024

Vtec234 Oct 24, 2024

kmill Oct 24, 2024

feat: labeled and unique sorries #5757

Are you sure you want to change the base?

feat: labeled and unique sorries #5757

Conversation

kmill commented Oct 17, 2024 • edited Loading

leanprover-community-bot commented Oct 17, 2024 • edited Loading

alexkeizer commented Oct 19, 2024

kmill commented Oct 19, 2024

alexkeizer commented Oct 19, 2024 • edited Loading

kmill commented Oct 19, 2024 • edited Loading

kmill Oct 23, 2024

Choose a reason for hiding this comment

kmill Oct 23, 2024

Choose a reason for hiding this comment

Vtec234 Oct 24, 2024

Choose a reason for hiding this comment

kmill Oct 24, 2024

Choose a reason for hiding this comment

kmill commented Oct 17, 2024 •

edited

Loading

leanprover-community-bot commented Oct 17, 2024 •

edited

Loading

alexkeizer commented Oct 19, 2024 •

edited

Loading

kmill commented Oct 19, 2024 •

edited

Loading