feat: better #eval command

[kmill]

This refactors and improves the #eval command, introducing some new features.

• Now evaluated results can be represented using ToExpr and pretty printing. This means hoverable output. If ToExpr fails, it then tries Repr and then ToString. The eval.pp option controls whether or not to try ToExpr.
• There is now auto-derivation of Repr instances, enabled with the pp.derive.repr option (default to true). For example:

  inductive Baz
    | a | b
  
  #eval Baz.a
  -- Baz.a

  It simply does deriving instance Repr for Baz when there's no way to represent Baz. If core Lean gets ToExpr derive handlers, they could be used here as well.
• The option eval.type controls whether or not to include the type in the output. For now the default is false.
• Now things like #eval do return 2 work. It tries using CommandElabM, TermElabM, or IO when the monad is unknown.
• Now there is no longer Lean.Eval or Lean.MetaEval. These each used to be responsible for both adapting monads and printing results. The concerns have been split into two. (1) The MonadEval class is responsible for adapting monads for evaluation (it is similar to MonadLift, but instances are allowed to use default data when initializing state) and (2) finding a way to represent results is handled separately.
• Error messages about failed instance synthesis are now more precise. Once it detects that a MonadEval class applies, then the error message will be specific about missing ToExpr/Repr/ToString instances.
• Fixes a bug where Repr/ToString instances can't be found by unfolding types "under the monad". For example, this works now:

  def Foo := List Nat
  def Foo.mk (l : List Nat) : Foo := l
  #eval show Lean.CoreM Foo from do return Foo.mk [1,2,3]

• Elaboration errors now abort evaluation. This eliminates some not-so-relevant error messages.
• Now evaluating a value of type m Unit never prints a blank message.
• Fixes bugs where evaluating MetaM and CoreM wouldn't collect log messages.

The run_cmd, run_elab, and run_meta commands are now frontends for #eval.

[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 248864c716e4276da7135de2b624a7b6b198f50c --onto 3e75d8f74297bc258352f8d89f71496aacefe7ae. (2024-10-08 20:32:28)