-DRUNTIME_STATS=ON breaks lean build

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

-DLEAN_RUNTIME=ON does not compile: Full error gist.

/homes/sb2743/temp/lean4/src/runtime/allocprof.cpp: In constructor ‘lean::allocprof::allocprof(std::ostream&, const char*)’:
/homes/sb2743/temp/lean4/src/runtime/allocprof.cpp:12:25: error: ‘g_num_ctor’ was not declared in this scope; did you mean ‘m_num_ctor’?
   12 |         m_num_ctor    = g_num_ctor;
      |                         ^~~~~~~~~~
      |                         m_num_ctor
/homes/sb2743/temp/lean4/src/runtime/allocprof.cpp:13:25: error: ‘g_num_closure’ was not declared in this scope; did you mean ‘m_num_closure’?
   13 |         m_num_closure = g_num_closure;
      |                         ^~~~~~~~~~~~~
      |                         m_num_closure
/homes/sb2743/temp/lean4/src/runtime/allocprof.cpp:14:25: error: ‘g_num_string’ was not declared in this scope; did you mean ‘m_num_string’?
   14 |         m_num_string  = g_num_string;
      |                         ^~~~~~~~~~~~
      |                         m_num_string
...
/homes/sb2743/temp/lean4/src/runtime/alloc.cpp:45:21: error: template argument 1 is invalid
   45 | static atomic<uint64> g_num_exports(0);
      |                     ^
/homes/sb2743/temp/lean4/src/runtime/alloc.cpp:46:15: error: ‘uint64’ was not declared in this scope; did you mean ‘uint64_t’?
   46 | static atomic<uint64> g_num_recycled_pages(0);
      |               ^~~~~~
      |               uint64_t
/homes/sb2743/temp/lean4/src/runtime/alloc.cpp:46:21: error: template argument 1 is invalid
   46 | static atomic<uint64> g_num_recycled_pages(0);

Steps to Reproduce

git clone https://github.com/leanprover/lean4.git  && \
  mkdir -p lean4/build/ && \
  cd lean4/build/ && \
  cmake ../ -DRUNTIME_STATS=ON && \
  make -j6

Expected behavior: Build succeeds.

Actual behavior: Build fails.

Versions

uname -a
Linux dev-cpu-tcg40 6.5.0-25-generic #25~22.04.1-Ubuntu SMP PREEMPT_DYNAMIC Tue Feb 20 16:09:15 UTC 2 x86_64 x86_64 x86_64 GNU/Linux

Impact

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

Start by reproducing the failure with the documented CMake command and inspect src/runtime/allocprof.cpp and src/runtime/alloc.cpp, where the compiler errors are reported. Compare the runtime-statistics build path with the normal build and confirm that make succeeds with -DRUNTIME_STATS=ON.