max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: typo in enableInitializersExecution error message (#13553)

Browse source 
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
This commit is contained in:
Kim Morrison 2026-04-28 11:13:30 +10:00 • committed by GitHub
parent 2ad0f96d48
commit 87120c312e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Compiler/InitAttr.lean
View file

@ -159,7 +159,7 @@ def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit :=
@[export lean_run_init_attrs] @[export lean_run_init_attrs]
private unsafe def runInitAttrs (env : Environment) (opts : Options) : IO Unit := do private unsafe def runInitAttrs (env : Environment) (opts : Options) : IO Unit := do
if !(← isInitializerExecutionEnabled) then 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. -- **Note**: `ModuleIdx` is not an abbreviation, and we don't have instances for it.
-- Thus, we use `(modIdx : Nat)` -- Thus, we use `(modIdx : Nat)`
for mod in env.header.modules, (modIdx : Nat) in 0...* do for mod in env.header.modules, (modIdx : Nat) in 0...* do