From 480d7314a2c499f670609b2c2623a79d36cea760 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 17 Oct 2024 14:23:34 +0200 Subject: [PATCH] fix: do not force snapshot tree too early (#5752) This turns out to be the issue behind #5736, though really it is yet another indicator of a general thread pool weakness. (cherry picked from commit fc5e3cc66e3f317a03a17d9b19cc8d6476cf31cd) --- src/Lean/Language/Basic.lean | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index f6efc004fa7e..0c0b4e3735c2 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -243,11 +243,16 @@ instance : ToSnapshotTree SnapshotLeaf where structure DynamicSnapshot where /-- Concrete snapshot value as `Dynamic`. -/ val : Dynamic - /-- Snapshot tree retrieved from `val` before erasure. -/ - tree : SnapshotTree + /-- + Snapshot tree retrieved from `val` before erasure. We do thunk even the first level as accessing + it too early can create some unnecessary tasks from `toSnapshotTree` that are otherwise avoided by + `(sync := true)` when accessing only after elaboration has finished. Early access can even lead to + deadlocks when later forcing these unnecessary tasks on a starved thread pool. + -/ + tree : Thunk SnapshotTree instance : ToSnapshotTree DynamicSnapshot where - toSnapshotTree s := s.tree + toSnapshotTree s := s.tree.get /-- Creates a `DynamicSnapshot` from a typed snapshot value. -/ def DynamicSnapshot.ofTyped [TypeName α] [ToSnapshotTree α] (val : α) : DynamicSnapshot where