From 20a7fe89b5e957287f5f705dbd6de3be4e8f6b13 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 14 Aug 2024 15:39:35 +0200 Subject: [PATCH] perf: mark entire reported info tree as persistent (#5040) As we can definitely not free it until .ilean generation at the very end --- src/Lean/Language/Lean.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index e74107bee0..e4757b55f9 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -599,7 +599,7 @@ where let minimal := internal.minimalSnapshots.get scope.opts && !Parser.isTerminalCommand stx finishedPromise.resolve { diagnostics := (← Snapshot.Diagnostics.ofMessageLog cmdState.messages) - infoTree? := cmdState.infoState.trees[0]! + infoTree? := Runtime.markPersistent cmdState.infoState.trees[0]! cmdState := if minimal then { env := initEnv maxRecDepth := 0