feat: lake: builtin facet memoize toggle

[tydeu]

This PR makes memoization of built-in facets toggleable through a memoize option on the facet configuration. Built-in facets which are essentially aliases (e.g., default, o) have had memoization disabled.

[tydeu]

!bench

[leanprover-bot]

Here are the benchmark results for commit 84667e9.
There were significant changes against commit 12a21e7:

  Benchmark          Metric         Change
  ==================================================
- lake build no-op   instructions     2.9%  (12.1 σ)
+ lake config elab   wall-clock      -3.8% (-11.4 σ)
+ lake env           task-clock      -5.1% (-20.8 σ)
+ lake env           wall-clock      -5.3% (-32.5 σ)
+ liasolver          task-clock      -4.3% (-17.9 σ)
+ liasolver          wall-clock      -4.4% (-14.9 σ)
+ qsort              task-clock      -6.1% (-10.6 σ)
+ qsort              wall-clock      -6.1% (-10.5 σ)
+ rbmap              task-clock      -2.3% (-11.0 σ)
+ rbmap              wall-clock      -2.3% (-10.4 σ)
+ rbmap_fbip         task-clock      -5.3% (-40.1 σ)
+ rbmap_fbip         wall-clock      -5.3% (-47.2 σ)
+ simp_arith1        task-clock      -1.8% (-10.2 σ)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-7738 has successfully built against this PR. (2025-03-30 23:22:05) View Log