Function rs_tmp_decode_const_map

crates/ffi/src/lean_env.rs:1116–1637

(
  obj: LeanList<LeanBorrowed<'_>>,
)

fn decode_name_constant_info(
  obj: LeanBorrowed<'_>,
  global: &GlobalCache,
) -> (Name, ConstantInfo) {
  let mut cache = Cache::new(global);
  // Outer Prod (Name × ConstantInfo) has no public LeanProd<LeanBorrowed>
  // constructor, so read the two fields through the raw ctor.
  let pair = obj.as_ctor();
  let name = decode_name(pair.get(0), global);
  let constant_info = decode_constant_info(pair.get(1), &mut cache);
  (name, constant_info)
}

/// Resident-decoded-constant bound for [`decode_env_lazy`]'s cache.
///
/// Sized by sweep, not by hit rate: on FLT (511k consts) wall time is
/// flat from 4096 through 1M entries (60–67 s; misses hide in the
/// scheduler's dependency-stall slack) while peak RSS climbs from
/// 11.5 GiB (4k) → 13.0 (64k) → 24.7 (1M); Mathlib (737k consts)
/// confirms parity at this size (87.5 s / 17.0 GiB vs 87.3 s /
/// 18.3 GiB at 64k). So the cache buys RAM, not speed, and the bound
/// sits at the small end with headroom over the 4k floor measured to
/// still not thrash.
const LAZY_ENV_CACHE_ENTRIES: usize = 16384;

/// Decode for the production compile FFI entries: an on-demand view
/// that avoids materializing the full Rust copy of the environment —
/// the eager copy is the single largest memory term at scale. The
/// on-demand decode costs a few percent of wall (per-constant fetches
/// vs one batched decode); `IX_COMPILE_EAGER=1` buys that back on
/// machines with RAM to spare. Measured on FLT: −8 % wall for
/// +13 GiB peak; Mathlib eager exceeds a 56 GB machine outright
/// (the copy sits alongside the Lean-held env). Test and roundtrip
/// entries keep [`decode_env`] (they re-read the env structurally
/// throughout).
pub fn decode_env_for_compile(list: LeanList<LeanBorrowed<'_>>) -> Env {
  if std::env::var("IX_COMPILE_EAGER").as_deref() == Ok("1") {
    return decode_env(list);
  }
  decode_env_lazy(list, LAZY_ENV_CACHE_ENTRIES)
}

/// Lazy variant of [`decode_env`]: decode only the *names* eagerly,
/// keep a per-constant `LeanShared` handle, and decode `ConstantInfo`s
/// on demand through `Env`'s bounded cache.
///
/// Thread-safety is identical to the eager path, which already decodes
/// in parallel: `lean_mark_mt` (via `LeanShared::new`) transitions the
/// reachable graph to atomic refcounting, structural reads through
/// `LeanBorrowed` accessors are refcount-silent, and each element's
/// owned handle keeps its Lean objects alive for the `Env`'s lifetime
/// regardless of what the Lean side does after the FFI call.
pub fn decode_env_lazy(
  list: LeanList<LeanBorrowed<'_>>,
  cache_entries: usize,
) -> Env {
  let shared_list = LeanShared::new(list.inner().to_owned_ref());
  let objs = collect_list_shared(shared_list.borrow().as_list());
  let global = Arc::new(GlobalCache::with_capacity(objs.len() * 3));