feat: incremental elaboration of definition headers, bodies, and top-level tactic blocks

[Kha]

Implements a syntax-based approach for incremental reporting and reuse for the following intra-command elaboration steps:

• finished definition (def/theorem/abbrev/opaque/instance/example) headers (binders and result type) when all syntax above is unchanged
• finished definition bodies when all headers of the mutual block are unchanged (so only works for the last body for now)
• finished tactic steps t when the whole definition body is of the form := by ... t ..., what I call a "top-level" tactic block

TODO

• [ ] support for tactic combinators such as induction, case (as seen above), next, ...
• [ ] testing, testing, testing
• [ ] more documentation
• [ ] refine API; this is the "it works" stage
• [ ] incremental reporting may lead to MessageLog.hasErrors becoming false where it was true before during elaboration
• [ ] later: incremental info trees for immediate hover on finished tactic steps etc.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6af7a01af643e82e1deeb6b7523b8099d177b159 --onto 611b1746896bbadf459c00cc218fa31cf51b4e08. (2024-03-13 06:04:49)