feat: labeled and unique sorries

[kmill]

This PR makes it harder to create "fake" theorems about definitions that are stubbed-out with sorry by using an encoding that ensures each sorry is 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, since making these unique tends to cause a confusing cascade of errors. In general however such sorries are labeled. This enables "go to definition" on sorry in the Infoview, which brings you to its origin. The option set_option pp.sorrySource true causes the pretty printer to show source position information on sorries.

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 `[email protected]._hyg.153
  

  It can either be made unique (like the above) or merely labeled. Labeled sorries use an encoding that does not impact defeq:

  sorryAx (Unit → Nat) false (Function.const Lean.Name () `[email protected]._hyg.174)
  

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

• Renames OmissionInfo to DelabTermInfo and adds configuration options to control LSP interactions. One field is a source position to use for "go to definition". This is used to implement "go to definition" on labeled sorries.

• 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 start with printing with this source position information.

• Removes Lean.Meta.mkSyntheticSorry in favor of Lean.Meta.mkSorry and Lean.Meta.mkLabeledSorry.

• Changes sorryAx so that the synthetic argument is no longer optional.

• Gives addPPExplicitToExposeDiff awareness of labeled sorries. It can set pp.sorrySource when source positions differ.

• Modifies the delaborator framework so that delaborators can set Info themselves without it being overwritten.

Incidentally closes #4972.

Inspired by this Zulip thread.

[leanprover-community-bot]

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)
• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-11-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-12-01 22:37:58)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-12-08 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-12-08 21:32:16)

[alexkeizer]

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

[kmill]

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]

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]

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