[basvandijk]

This PR fixes the scalar fields of static objects, such as the hashes of name literals, on 32-bit targets such as wasm32-wasip1 and i686, by choosing the form of LEAN_SCALAR_PTR_LITERAL by pointer size instead of by LEAN_EMSCRIPTEN.

Since #12082, the compiler writes the scalar fields of static constructor objects in 8-byte chunks with LEAN_SCALAR_PTR_LITERAL. Unless LEAN_EMSCRIPTEN was defined, lean.h used its 64-bit form, which on a 32-bit target casts each chunk to a single 4-byte pointer: each object got one slot per chunk instead of two and lost the upper half of every chunk, without a compiler warning. A name literal then had a wrong hash, and compared unequal to the same name built at run time. Lean's build defines LEAN_EMSCRIPTEN only for its own C++ code, not for the C that leanc compiles, so this affected Emscripten too. On 64-bit targets, the preprocessed lean.h does not change.

The new test tests/compile/static_scalar_fields.lean compares the scalar fields of several kinds of static objects, including a name literal's hash, with the same values built at run time. CI has no 32-bit job, so there it passes with or without this change; on wasm32-wasip1 it fails without it.

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

Closes #15814

🤖 Generated with Claude Code

[basvandijk]

How this was tested:

• lean.h before and after this PR, with the file from LEAN_SCALAR_PTR_LITERAL truncates static scalar fields on 32-bit targets #15814, which expands LEAN_SCALAR_PTR_LITERAL once and asserts that this takes 8 bytes, and a C++ version of it with static_assert: compiled with -fsyntax-only -Wall -Wextra, and preprocessed with -E -P -DNDEBUG, ignoring blank lines.

  Target	Before	After	Preprocessed output
  x86_64, gcc 16.2.0 and clang 21.1.8, C and C++	compiles	compiles	identical
  i686, gcc 16.2.0 with -msse2 -mfpmath=sse, C and C++	assertion fails	compiles	changed
  wasm32-wasip1, clang 21.1.8, C and C++	assertion fails	compiles	changed
  Emscripten 6.0.9, emcc and em++, as leanc compiles	assertion fails	compiles	changed
  Emscripten 6.0.9, emcc and em++, with -DLEAN_EMSCRIPTEN	compiles	compiles	identical
  Emscripten 6.0.9, emcc and em++, with -DLEAN_EMSCRIPTEN -sMEMORY64	assertion fails	compiles	changed

• The new test on wasm32-wasip1. The only wasm32-wasip1 build of the runtime and Init at hand is of v4.34.1, with WASI patches and an equivalent fix, so this used v4.34.1. It compiles the test to the same C as this branch, apart from the name of one specialized BEq function. That C, compiled with -O3 -DNDEBUG, linked against that runtime and Init, and run with wasmtime 45.0.2, prints false on every line with v4.34.1's lean.h, whose condition is master's, and the expected output with this PR's condition.

• This branch, built with cmake --preset release on x86_64 Linux: the new test passes in both modes of tests/compile/run_test.sh and with ctest, the other 105 tests in tests/compile pass, and so does tests/lint.py.

The bug dates from #12082 (v4.29.0). CI's Web Assembly and Linux 32bit jobs had been disabled before that, in #6424 and #7924. A correction to #15814: generated C is affected on Emscripten too, since Lean's build defines LEAN_EMSCRIPTEN only for the runtime's C++.

stage0/src/include/lean/lean.h keeps the old condition until the next stage0 update.