feat: labeled and unique sorries

[kmill]

This PR makes it harder to create "fake" theorems about definitions stubbed-out with sorry by arranging things so that each instance of 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 confusing cascading errors. In general though, 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 `lean.foo.12.8.11.8.11.13._sorry._@.lean.foo._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 () `lean.foo.14.7.13.7.13.69._sorry._@.lean.foo._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 print 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 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)

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

[mhuisi]

Mixing a Name and an Lsp.Range is a bit strange, since the former is a Lean concept and the latter is an LSP concept. Could this just use Lsp.Location, or should it be a Lean-specific structure of Name and String.Pos?