refactor: lake: use StateRefT for BuildStore

[tydeu]

This PR uses StateRefT instead of StateT to equip the Lake build monad with a build store.

As a IO reference, different threads may now contend with the build store. The benchmark results indicate the change has a significant performance impact. On the thread-safety front, the lack of a mutex should not be a concern because the build store is a memorization data structure and thus inconsistent state is theoretically okay.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-11-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-12-02 19:14:25)

[tydeu]

!bench

[leanprover-bot]

Here are the benchmark results for commit 79d8c56.
There were no significant changes against commit 27df5e9.