mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
43956fc069
This PR implements lazy initialization of closed terms. Previous work has already made sure that ~70% of the closed terms occurring in core can be statically initialized from the binary. With this the remaining ones are initialized lazily instead of at startup. For this we implement a small statically initializable lock that goes with each term. When trying to access the term we quickly check a flag to say whether it has already been initialized. If not we take the lock and initialize it, otherwise we dereference the pointer and fetch the value.