Skip to content

Commit

Permalink
change default to sync
Browse files Browse the repository at this point in the history
  • Loading branch information
Kha committed Jan 30, 2025
1 parent 8f4253e commit 3573efd
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Lean/Environment.lean
Original file line number Diff line number Diff line change
Expand Up @@ -865,7 +865,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
Expand Down Expand Up @@ -954,7 +954,7 @@ structure PersistentEnvExtension (α : Type) (β : Type) (σ : Type) where
addEntryFn : σ → β → σ
exportEntriesFn : σ → Array α
statsFn : σ → Format
asyncMode : EnvExtension.AsyncMode := .mainOnly
asyncMode : EnvExtension.AsyncMode := .sync

instance {α σ} [Inhabited σ] : Inhabited (PersistentEnvExtensionState α σ) :=
⟨{importedEntries := #[], state := default }⟩
Expand Down

0 comments on commit 3573efd

Please sign in to comment.