From 87120c312e10bc76c86767ea6082c009e7b0ee80 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 28 Apr 2026 11:13:30 +1000
Subject: [PATCH] fix: typo in `enableInitializersExecution` error message
 (#13553)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes a typo in the error message thrown by `runInitAttrs` when
initializer execution has not been enabled. The message previously
referred to `enableInitializerExecution` (singular), but the actual
function is `enableInitializersExecution` (plural).

Reported on Zulip by Siddhartha Gadgil:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Error.20in.20error.20message.20.28initializer.29/near/590973368

🤖 Prepared with Claude Code
---
 src/Lean/Compiler/InitAttr.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean
index be6b79f329..dd43797930 100644
--- a/src/Lean/Compiler/InitAttr.lean
+++ b/src/Lean/Compiler/InitAttr.lean
@@ -159,7 +159,7 @@ def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit :=
 @[export lean_run_init_attrs]
 private unsafe def runInitAttrs (env : Environment) (opts : Options) : IO Unit := do
   if !(← isInitializerExecutionEnabled) then
-    throw <| IO.userError "`enableInitializerExecution` must be run before calling `importModules (loadExts := true)`"
+    throw <| IO.userError "`enableInitializersExecution` must be run before calling `importModules (loadExts := true)`"
   -- **Note**: `ModuleIdx` is not an abbreviation, and we don't have instances for it.
   -- Thus, we use `(modIdx : Nat)`
   for mod in env.header.modules, (modIdx : Nat) in 0...* do