perf: lake: read the build store without taking its ref

[zeldovich]

The StateRefT'-based MonadDStore/MonadStore instances in Lake.Util.StoreInsts implement a memo lookup as modifyGet fun m => (m.get? k, m). On a multi-threaded ref, ST.Ref.modifyGet takes the cell (an atomic exchange with null) and holds it for the duration of the tree search; lean_st_ref_take spins, without backoff, while the cell is taken. Lake's build store (the StateRefT' IO.RealWorld BuildStore layer of RecBuildT) is such a ref, so every memo lookup of every build thread is serialized through one spinlock, and a holder that is preempted leaves all other threads spinning.

The lookups are frequent: fetchTransImportArts walks each compiled module's transitive import closure with two store fetches per transitive import, concurrently on every pool thread. On a 192-vCPU machine building a 26k-module workspace with import closures of 700-2,200 modules, lake accounted for 38.5k of the build's 99k CPU-seconds; perf attributed 97% of lake's cycles to lean_st_ref_take, with every sampled stack inside Lake.recFetch/recFetchWithIndex.

A lookup now reads the map with get instead: ST.Ref.get holds the cell only while it bumps a reference count, and a read of a persistent map needs no exclusion. Only store (an insert) still takes the cell. The StateT instances are unchanged; modifyGet on a pure state involves no ref.

Same machine and workspace, clean build: 930 s to 754 s wall, 90.1k to 48.8k user CPU-seconds in total, lake's own CPU time 38.5k to 3.2k CPU-seconds.

[Rob23oba]

!bench

[leanprover-radar]

Benchmark results for 63e1769 against 8258e75 are in. No significant results found. @Rob23oba

• ✅ build//instructions: -539.0M (-0.01%)

Small changes (2🟥)

• 🟥 build/module/Lake.Build.Index//instructions: +19.9M (+1.17%)
• 🟥 build/module/Lake.Util.StoreInsts//instructions: +15.4M (+1.87%)