INTERNAL PANIC: Error when Pickling Proof State

[RexWzh]

When trying to pickle the proof state to test.olean, the system throws INTERNAL PANIC.

I've tried on versions v4.19.0-rc2, v4.18.0 and v4.10.0.

Steps to reproduce:

{"cmd": "import Mathlib", "env": null}

{"cmd": "theorem mathd_algebra_59 (b : ℝ) (h₀ : (4 : ℝ) ^ b + 2 ^ 3 = 12) : b = 1 := by sorry", "env": 0}

{"tactic": "have h₁ : 0 < 2 := by norm_num", "proofState": 0}

{"pickleTo": "test.olean", "proofState": 1}

Outputs:

{"env": 0}

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 1, "column": 79},
   "goal": "b : ℝ\nh₀ : 4 ^ b + 2 ^ 3 = 12\n⊢ b = 1",
   "endPos": {"line": 1, "column": 84}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 1, "column": 8},
   "endPos": {"line": 1, "column": 24},
   "data": "declaration uses 'sorry'"}],
 "env": 1}

{"proofState": 1,
 "goals": ["b : ℝ\nh₀ : 4 ^ b + 2 ^ 3 = 12\nh₁ : 0 < 2\n⊢ b = 1"]}

INTERNAL PANIC: closures cannot be compacted. One possible cause of this error is trying to store a function in a persistent environment extension.