lean --version, --run and other options exit with a garbage code on 32-bit targets #16136

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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 security@lean-fro.org for responsible disclosure.

Description

On 32-bit targets, lean exits with a code derived from a heap address in these cases:

• options that end it during option processing: --version, --short-version, --githash, --help and --features should exit with 0, and an unknown option or an invalid argument such as -j x with 1;
• the early returns of Lean.shellMain, for example --print-prefix, --print-libdir and --deps of a file, which should exit with 0, and lean without a file name, which should exit with 1;
• lean --run, which should exit with the code that the program's main returns.

When it processes a file without --run, shellMain ends with IO.Process.exit, so the exit code of such a run is correct.

lean gets these codes as UInt32 values from Lean code. Since #11434, Lean.ShellOptions.process throws them as the error of an EIO UInt32 ShellOptions, and process_shell_option reads them with unbox (shell.cpp#L242). Lean.shellMain returns them as an IO UInt32, and run_shell_main reads them with get_io_scalar_result<uint32> (shell.cpp#L217), which also uses unbox (io.h#L48):

rc = unbox(io_result_get_error(r));   // shell.cpp
T r = unbox(io_result_get_value(o));  // io.h, with T = uint32

On 64-bit targets a boxed UInt32 is a scalar, so unbox returns the code. On 32-bit targets, lean_box_uint32 allocates an object for it, so unbox returns half the object's address, and the process exits with that modulo 256.

Context

Found while building the WebAssembly (wasm32) lean of the Web Assembly CI job, which #16134 proposes to re-enable; its stage 0 is a native i386 lean. Both show the bug. tests/misc/lean_version.sh, lean_help.sh and lean_ghash.sh check that --version, --help and --githash exit with 0, but CI only runs them on 64-bit targets. lean_unknown_option.sh only checks that lean -z fails, so it passes with the bug.

Steps to Reproduce

1. Build lean for i386, for example with the stage 0 options of the Web Assembly entry that chore: re-enable the Web Assembly CI job #16135 re-enables in .github/workflows/ci.yml, or build the WebAssembly lean as that job does on chore: re-enable the Web Assembly CI job #16135's branch. The commented-out entry on master passes only -m32 to the stage 0 compiler; with that, Ubuntu 24.04's clang 18 sets FLT_EVAL_METHOD to 2, and lean.h stops with an #error.
2. Run lean --version; echo $? and lean -z; echo $?.
3. Save def main : IO UInt32 := pure 3 as run3.lean and run lean --run run3.lean; echo $?.

Expected behavior: exit codes 0, 1 and 3.

Actual behavior: the i386 lean exits with 162, 130 and 42, and the WebAssembly lean with 178, 154 and 134. On i386, --short-version, --githash, --help, --features, --print-prefix, --print-libdir and --deps of an empty file also exit with 162, and -j x and lean without a file name with 130. On WebAssembly, --print-prefix and --print-libdir fail before they return, with ReferenceError: __filename is not defined, which is a separate problem.

Versions

Lean 4.37.0-pre. The i386 lean is stage 0 of master 5f155ca (2026-10-30), so it is built from stage0/src, which has the same lines; it was built on Ubuntu 24.04 with clang 18 and the stage 0 options of #16135 (-m32 -msse2 -mfpmath=sse). The wasm32 lean is stage 1 of #16135's branch, which is master 5f155ca plus commits that do not touch src/util or src/Lean/Shell.lean (master alone does not build for wasm32), built with Emscripten 3.1.44 and run with Node.js 26.13.0. The nightly releases have no 32-bit build, so I could not run the test case on one. src/util/shell.cpp and src/util/io.h have the same lines in nightly-2026-10-30, and the builds I tested are based on master 5f155ca, six commits after it.

Additional Information

Reading both codes with unbox_uint32 (lean_unbox_uint32) fixes them; on 64-bit targets it is the same as unbox. The C code that the compiler generates for a main that returns UInt32 already reads the result with lean_unbox_uint32.

Claude Code, an AI coding assistant, helped with the investigation and this description. I reviewed and checked them.

Impact

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