From c2a80b25706321b2843bc31885dd2870ddf03c80 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 31 Jan 2025 11:49:25 +0100 Subject: [PATCH] change default to sync, minus persistent exts --- src/Lean/Environment.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index a3ee299ae87a7..54a56d9ee60cc 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -869,7 +869,7 @@ end EnvExtension 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 σ) - (asyncMode : EnvExtension.AsyncMode := .mainOnly) : IO (EnvExtension σ) := do + (asyncMode : EnvExtension.AsyncMode := .sync) : IO (EnvExtension σ) := do unless (← initializing) do throw (IO.userError "failed to register environment, extensions can only be registered during initialization") let exts ← EnvExtension.envExtensionsRef.get