From 31eb42f2b3d5c6fca826a65bbaf17aee9e992955 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 24 Jul 2026 09:01:10 +0000
Subject: [PATCH] experiment: measure kernel impact

---
 mathlib4/lakefile.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/mathlib4/lakefile.lean b/mathlib4/lakefile.lean
index 1c2f6bf57..4d799a378 100644
--- a/mathlib4/lakefile.lean
+++ b/mathlib4/lakefile.lean
@@ -44,6 +44,7 @@ abbrev mathlibLeanOptions := #[
     ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
     ⟨`autoImplicit, false⟩,
     ⟨`maxSynthPendingDepth, .ofNat 3⟩,
+    ⟨`debug.skipKernelTC, true⟩,
   ] ++ -- options that are used in `lake build`
     mathlibOnlyLinters.map fun s ↦ { s with name := `weak ++ s.name }