feat: compiled tactic configuration elaborators, and configurability

[kmill]

This PR changes the way tactic configurations work so that they are compiled ahead of time, rather than relying on elaboration and compilation at tactic run time, improving performance. It also introduces some configurability for the generated configuration elaborators. For example, it's now possible to create custom tactic option interpreters. This will be used by simp to support user-defined options like simp +user.mySimprocOption.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-13 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-16 01:43:12)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-03 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-05 18:56:25)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-13426 build failed against this PR. (2026-04-16 01:47:56) View Log
• 💥 Mathlib branch lean-pr-testing-13426 build failed against this PR. (2026-05-05 19:00:44) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-13426 build failed against this PR. (2026-04-16 05:18:15) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-13426 build failed against this PR. (2026-04-16 06:32:19) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-13426 build failed against this PR. (2026-04-16 15:32:31) View Log

[kmill]

!bench

[leanprover-radar]

Benchmark results for fdb1411 against d76e5a1 are in. There are significant results. @kmill

• ✅ build//instructions: -8.2G (-0.07%)

Large changes (3✅, 9🟥)

• 🟥 build/module/Lean.Elab.Tactic.Grind.Main//instructions: +6.5G (+41.12%)
• 🟥 build/module/Lean.Elab.Tactic.NormCast//instructions: +5.4G (+55.49%)
• 🟥 build/module/Lean.Elab.Tactic.Simp//instructions: +5.8G (+38.16%)
• ✅ elab/mut_rec_wf//instructions: -2.8G (-10.32%)
• ✅ elab/mut_rec_wf//task-clock: -299ms (-13.32%)
• ✅ elab/mut_rec_wf//wall-clock: -295ms (-14.42%)
• 🟥 size/all/.c//lines: +189.6k (+1.72%)
• 🟥 size/all/.ir//bytes: +5MiB (+1.50%)
• 🟥 size/all/.olean.private//bytes: +10MiB (+0.85%)
• 🟥 size/compile/.out//bytes: +33MiB (+1.91%)
• 🟥 size/install//bytes: +24MiB (+0.95%)
• 🟥 size/libleanshared.so//bytes: +2MiB (+1.58%)

Medium changes (7✅, 10🟥)

• ✅ build/module/Init.Data.Array.Basic//instructions: -1.7G (-12.45%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Elab.MutualInductive//instructions: -1.1G (-2.99%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Attr//instructions: +2.7G (+109.32%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Decide//instructions: +1.1G (+23.17%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Do.VCGen.Basic//instructions: +1.2G (+12.91%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Grind.Config//instructions: +1.7G (+23.60%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Lets//instructions: +2.8G (+80.37%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.LibrarySearch//instructions: +1.0G (+24.09%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Omega.Frontend//instructions: +1.2G (+3.26%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Rewrite//instructions: +1.5G (+38.36%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.SolveByElim//instructions: +3.8G (+86.22%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Try//instructions: +1.3G (+4.20%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Sym.Pattern//instructions: -1.8G (-7.30%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DTreeMap.Internal.Queries//instructions: -1.2G (-5.84%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: -2.0G (-2.96%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul//instructions: -1.2G (-5.22%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: -4.1G (-3.75%) (reduced significance based on absolute threshold)

Small changes (223✅, 12🟥)

Too many entries to display here. View the full report on radar instead.