Adds `@[app_delab ident]` as a macro for `@[delab app.ident]`. Resolves
the identifier when expanding the macro, saving needing to use the fully
qualified identifiers that `@[delab]` requires. Also, unlike `@[delab]`,
throws an error if the identifier cannot be resolved.

Closes leanprover#4899

…xor] (leanprover#4981)

…prover#4987)

closes leanprover#4920

closes leanprover#4947

This is a better fix to the problem reported at
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nat.20fighting,
which itself had a problem as reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/omega.20regression/near/456539091.

.. as well as neg_neq_iff_neq_neg.

---------

Co-authored-by: Henrik Böving <hargonix@gmail.com>

We observed a small performance improvement at
https://github.com/leanprover/LNSym/blob/proof_size_expt/Proofs/SHA512/Experiments/Sym30.lean
Before: 2.65s
After: 2.60s

Closes leanprover#4513

---------

Co-authored-by: Kim Morrison <kim@tqft.net>

After having added already `BitVec.ushiftRight_*_distrib`in
leanprover#4667 for ushiftRight, this PR
now completes the `*_distrib` theorems for shift.

Closes leanprover#4959

Helpful for diagnosing which linter is failing, c.f. [recent
problem](https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/quote4/near/457349304)
in quote4.

Co-authored-by: Siddharth <siddu.druid@gmail.com>

Without this change, a stack overflow on Mac OS during tactic execution
can lead to the message:

    terminated by signal SIGBUS (Misaligned address error)

This comes from `lean_alloc_small`. With the change, the process instead
terminates with the more accurate and actionable:

    Stack overflow detected. Aborting.

The prior default of 1000000 could not be achieved in practice, because
the stack would overflow after around 5000 recursive invocations. This
meant that a poorly-chosen @[ext] lemma could crash Lean.

Talking to Mathlib users, it seems that 10 would be a very large number
in practice, so a default limit of 100 should not change successful
uses. But it does make it much easier to diagnose and recover from poor
choices of @[ext] lemmas.

Co-authored-by: Atticus Kuhn <52258164+AtticusKuhn@users.noreply.github.com>

)

Closes: leanprover#4573

…nprover#5001)

...unless we are about to kill the process anyway (which is not the
default)

Ensures panics are visible as regular messages in the language server
and properly ordered in relation to other messages on the cmdline

Step 2/~7 in upstreaming LeanSAT.

---------

Co-authored-by: Tobias Grosser <tobias@grosser.es>
Co-authored-by: Siddharth <siddu.druid@gmail.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>

According to the release notes of cache this should not break anything
as they merely upgraded the node version.

…over#4982)

For structure projections, the pretty printer assumed that the
expression was type correct. Now it checks that the object being
projected is of the correct type. Such terms appear in type mismatch
errors.

Also, fixes and improves `#print` for structures. The types of
projections now use MessageData (so are now hoverable), and the type of
`self` is now the correct type.

Closes leanprover#4670

…5004)

leanprover#4976 moved resolution of a promise to an earlier point, but that led to
object being marked MT earlier, so we need to move the code that
minimizes those objects earlier too to revert the performance
regression.

…10 to 3 (leanprover#5009)

Follows up on
leanprover#5003 (comment)

…eanprover#5014)

…anprover#5012)

as that’s the simp normal form.

…sics