From 367b0fc80fd22e1256b330080b0c20306338f73c Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sun, 10 Apr 2022 20:08:37 -0400 Subject: [PATCH] doc: note persistent exts are sometimes needed --- src/Lean/Environment.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index daf721458d..c975f4f943 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -282,7 +282,10 @@ end EnvExtension /- Environment extensions can only be registered during initialization. Reasons: 1- Our implementation assumes the number of extensions does not change after an environment object is created. - 2- We do not use any synchronization primitive to access `envExtensionsRef`. -/ + 2- We do not use any synchronization primitive to access `envExtensionsRef`. + + Note that by default, extension state is *not* stored in .olean files and will not propagate across `import`s. + For that, you need to register a persistent environment extension. -/ def registerEnvExtension {σ : Type} (mkInitial : IO σ) : IO (EnvExtension σ) := EnvExtensionInterfaceImp.registerExt mkInitial private def mkInitialExtensionStates : IO (Array EnvExtensionState) := EnvExtensionInterfaceImp.mkInitialExtStates