isDefEq cache for terms not containing metavariables..

Make Environment.mk and Environment.add private, and add replay as a safer alternative.

IO.Process.output no longer inherits the standard input of the caller.

Do not inhibit caching of default-level match reduction.

List the valid case tags when the user writes an invalid one.

The derive handler for DecidableEq now handles mutual inductive types.

Show path of failed import in Lake.

Fix linker warnings on macOS.

Lake: Add postUpdate? package configuration option. Used by a package to specify some code which should be run after a successful lake update of the package or one of its downstream dependencies. (lake#185)

Improvements to Lake startup time (#2572, #2573)

refine e now replaces the main goal with metavariables which were created during elaboration of e and no longer captures pre-existing metavariables that occur in e (#2502).

• This is accomplished via changes to withCollectingNewGoalsFrom, which also affects elabTermWithHoles, refine', calc (tactic), and specialize. Likewise, all of these now only include newly-created metavariables in their output.

• Previously, both newly-created and pre-existing metavariables occurring in e were returned inconsistently in different edge cases, causing duplicated goals in the infoview (issue #2495), erroneously closed goals (issue #2434), and unintuitive behavior due to refine e capturing previously-created goals appearing unexpectedly in e (no issue; see PR).