[basvandijk]

This PR fixes the exit code of lean on 32-bit targets such as WebAssembly (wasm32) and i386 after options like --version, --help and --deps, after an unknown option or an invalid argument, when called without a file name, and after --run. In these cases lean exited with a code derived from a heap address instead of 0, 1 or the exit code of the program's main; a run that processes a file without --run was not affected, because it ends with IO.Process.exit.

lean gets these codes as UInt32 values from Lean code: as the error of Lean.ShellOptions.process (since #11434) and as the result of Lean.shellMain. src/util/shell.cpp read both with unbox, the second through get_io_scalar_result<uint32> from src/util/io.h. On 32-bit targets a boxed UInt32 is a heap object rather than a scalar, so unbox returned half its address. This PR reads both with unbox_uint32, as the C code that the compiler generates for a main that returns UInt32 does, and replaces get_io_scalar_result, which had no other use, with get_io_uint32_result. On 64-bit targets unbox_uint32 is the same as unbox.

This PR adds no test: tests/misc/lean_version.sh, lean_help.sh and lean_ghash.sh already check that --version, --help and --githash exit with 0, but CI runs them only on 64-bit targets, where the old code works. The Web Assembly job that #16135 re-enables runs six other tests.

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

Closes #16136

🤖 Generated with Claude Code

[basvandijk]

How this was tested:

• WebAssembly, with this change applied on top of chore: re-enable the Web Assembly CI job #16135 and built as its Web Assembly job builds it. Without the change, lean --version, --short-version, --githash, --help, --features and --deps of an empty file exit with 178, lean -z, lean -j x and lean without a file name with 154, and lean --run of a main that returns 3 with 134; tests/misc/lean_version.sh, lean_help.sh and lean_ghash.sh fail. With the change, they exit with 0, 1 and 3, and the three tests pass. lean_unknown_option.sh and lean_unknown_file.sh, which only check that lean fails, pass with and without the change. With the change reverted, lean --version, lean without a file name and lean --run exit with 178, 154 and 134 again. --print-prefix and --print-libdir fail on WebAssembly with and without the change, with ReferenceError: __filename is not defined from IO.appPath, which is a separate problem.
• i386: not tested with this change. The native i386 stage 0 of that job, which is built from stage0/src and so keeps the old code until the next stage0 update, shows the bug: it exits with 162 for --version, --short-version, --githash, --help, --features, --print-prefix, --print-libdir and --deps of an empty file, with 130 for -z, -j x and lean without a file name, and with 42 for lean --run of a main that returns 3.
• x86-64: with this change, lean --version, --short-version, --githash, --help, --features, --print-prefix, --print-libdir and --deps of an empty file exit with 0, lean -z, lean -j x and lean without a file name with 1, and lean --run of a main that returns 3 with 3. The full test suite passes (4750 tests).