Many things reset the Meta cache

Stream: lean4

[Jovan Gerbscheid]

Lean keeps some cache in the MetaM and CoreM monads. In particular, results of type class search and whnf are cached. The function modifyEnv/setEnv clears this cache. There are many places calling modifyEnv where it is unneccessary to reset the cache. Examples include

• passing an argument to simp (because isRflProof calls modifyEnv)
• passing a configuration option to a tactic (e.g. simp +zeta) (because elaborating a structure { zeta := true } calls modifyEnv because it looks up information about the structur in the environment)

Here is some code demonstrating this:

import Lean

open Lean Meta Elab Term Tactic

/- Uncomment any of the lines of code, and observa that it resets the cache. -/
elab "test" : tactic => do
  -- evalTactic <| ← `(tactic| simp [iff_self])
  -- evalTactic <| ← `(tactic| simp +zeta)
  -- evalTactic <| ← `(tactic| simp only)

  -- _ ← Term.elabTerm (← `({})) (Expr.const ``Simp.Config [])

  -- recordExtraModUseFromDecl (isMeta := true) ``Simp.Config
  -- _ ← computeStructureResolutionOrder ``Simp.Config true
  -- _ ← isRflProof <| mkConst ``iff_self
  -- _ ← withoutExporting do return

  return

def foo (α : Type) [Mul α] := 5

/--
trace: [Meta.synthInstance] ✅️ Mul α
  [Meta.synthInstance] result inst✝ (cached)
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example {α : Type} [Mul α] : 2 + 2 = 5 := by
  have := foo α
  test
  set_option trace.Meta.synthInstance true in
  have := foo α
  sorry

[Jovan Gerbscheid]

I made a testing PR to Lean that liberally avoids resetting the cache, and the result is a 2% speedup in Mathlib, which can be seen here: https://speed.lean-lang.org/mathlib4/compare/d26e9feb-7b9e-4568-ab85-cadd2c20d0f7/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash2=eff2dfbcb624fa536176b4b688e158695bc48671

[Floris van Doorn]

including a 7.5% reduction in type-class resolution time!