Hacktoberfest 2026: the issues maintainers tagged for October, open and beginner-friendly. Browse Hacktoberfest issues

Boxed scalar closed terms are initialized eagerly at module initialization, so code in branches that are never taken runs before `main`

Open
  • Is something wrong?
#15,746 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
5/5
Estimated time
Over a week
Newbie friendliness
35/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Domain
compilers

Research direction

Start by reproducing the issue with the supplied Lake project and Main.lean, comparing the compiled executable with lean --run. Trace how boxed scalar values in lists or arrays are initialized during compilation and module initialization, then identify where evaluation should remain conditional. Done means the compiled program prints main started and f = [] without evaluating crash () before main.

Written by the indexing model from the issue text.

Description

bug
Prerequisites
  • [ X] Check that your issue is not already filed:
    https://github.com/leanprover/lean4/issues
  • [ X] Reduce the issue to a minimal, self-contained, reproducible test case.
    Avoid dependencies to Mathlib or Batteries.
  • [X ] Test your test case against the latest nightly release, for example on
    https://live.lean-lang.org/#project=lean-nightly
    (You can also use the settings there to switch to “Lean nightly”)
  • When reporting a perceived soundness bug: Does it affect lake check --paranoid?
    If in doubt, please reach out on [email protected] for responsible disclosure.
Description

In compiled code, a function call inside an if branch that is never taken is still executed, at program startup, before main runs. The interpreter (lean --run) behaves correctly.

It happens when:

  • the function returns UInt32, UInt64, USize, Float or Char (it does not happen with UInt8, UInt16, Bool or Nat),
  • the call does not depend on runtime values, e.g. crash () (constant arguments, or arguments the function doesn't use),
  • the result is put into a List or an Array.

Putting @[never_extract] on the function avoids the problem.

Context

Found while experimenting with compiled Lean programs. No prior Zulip discussion.

Steps to Reproduce
  1. Create a Lake project with the following Main.lean:
def crash (_ : Unit) : UInt64 :=
  let xs : Array UInt64 := #[1, 2]
  xs[100]!  -- out of bounds -> panic

def f (n : Nat) : List UInt64 :=
  if n > 10 then [crash ()] else []

def main (args : List String) : IO Unit := do
  IO.println "main started"
  IO.println s!"f = {f args.length}"
  1. Build it with lake build and run the executable without arguments, so the branch is not taken.
  2. For comparison, run lean --run Main.lean.

Expected behavior: crash () is never evaluated, because the branch is never taken:

main started
f = []

This is what lean --run Main.lean prints.

Actual behavior: The compiled binary evaluates crash () during module initialization, before main:

Error: index out of bounds
main started
f = []
Versions

Lean 4.35.0 (commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release)
Also reproduced with 4.30.0 and the latest nightly (4.37.0-nightly-2026-10-16, commit 88539871b4133140b0d5e9beb4cd446bcc0d2f40).

OS: Ubuntu 24.04.5 LTS (x86_64 / amd64)
Also reproduced on Windows 10 Enterprise 10.0.19045.6456

Additional Information

Observed consequences

  • Non-terminating code in a dead branch: the program hangs at startup.
  • Deep recursion in a dead branch: stack overflow, main never starts.
  • LEAN_ABORT_ON_PANIC=1: the program aborts before main, even though the branch is never taken.
  • Misleading diagnostics: the panic is reported at startup. If the branch is taken later, no panic is reported, because the value is already cached.
  • Effects hidden in pure code (unsafeIO, FFI declared as pure) run regardless of the guarding condition.
  • Importing a module that contains the pattern is enough. The function doesn't need to be called.
  • With precompileModules := true, the code runs inside the lean process when elaborating downstream modules. A non-terminating dead branch makes lake build of a downstream module hang.
Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Dominant language
Lean
Stars
9.6k
Forks
1.1k
Avg merge
1d 2h
Merged PRs (30d)
297

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/lean4

All issues in leanprover/lean4

Similar issues

More Compilers issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.