Function rs_compile_env

crates/ffi/src/compile.rs:289–381

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

/// FFI: compile a Lean environment and stream the serialized Ixon.Env
/// straight to `out_path` (see `Env::put_file`) — no env-sized `Vec` or
/// Lean `ByteArray` is built. Writes `<out_path>.tmp`, then renames, so
/// a crash cannot leave a truncated file. The file is the canonical
/// `Env::put` encoding (see `put_file`'s equivalence test).
///
/// Fail-closed semantics live here, behind the FFI: when
/// `allow_partial == 0` and any requested constant landed in
/// `CompileState.ungrounded`, nothing is written — the final path is
/// never created — and the returned status carries the full ungrounded
/// list for the caller to report. With `allow_partial != 0`, the
/// grounded subset is serialized and the same status discloses what
/// was omitted (see plans/aux-recursor-alias-collision.md §8).
///
/// Returns `Ix.CompileM.CompileEnvStatus` (layout
/// `LeanIxCompileEnvStatus`): root (64-hex canonical consts merkle
/// root — matches the serialized header, computed even when nothing is
/// written), ungrounded (`Array (String × String)` of pretty-name /
/// reason, sorted by name), bytes (0 when not written), named count,
/// unique anon count.
#[unsafe(no_mangle)]
pub extern "C" fn rs_compile_env(
  env_consts_ptr: LeanList<LeanBorrowed<'_>>,
  out_path: LeanString<LeanBorrowed<'_>>,
  allow_partial: u8,
) -> LeanIOResult<LeanOwned> {
  let rust_env = crate::lean_env::decode_env_for_compile(env_consts_ptr);
  let rust_env = Arc::new(rust_env);

  let compile_stt =
    match compile_env_with_options(&rust_env, CompileOptions::default()) {
      Ok(stt) => stt,
      Err(e) => {
        let msg = format!("rs_compile_env: Rust compilation failed: {:?}", e);
        return LeanIOResult::error_string(&msg);
      },
    };

  // Deterministically ordered (pretty name, reason) pairs — DashMap
  // iteration order is shard-dependent.
  let mut ungrounded: Vec<(String, String)> = compile_stt
    .ungrounded
    .iter()
    .map(|e| (e.key().pretty(), e.value().clone()))
    .collect();
  ungrounded.sort_by(|a, b| a.0.cmp(&b.0));

  // Canonical consts merkle root — equals the serialized header root
  // when a file is written; still reported on a fail-closed abort so
  // callers can record what the complete-subset content was. Computed
  // once here (parallel sort + tree) and handed to the writer — the
  // sort and the ~2·N-node tree used to run twice per compile.
  let mut const_addrs: Vec<Address> =
    compile_stt.env.consts.iter().map(|e| e.key().clone()).collect();
  {
    use rayon::prelude::*;
    const_addrs.par_sort_unstable();
  }
  let root = ixon::merkle::merkle_root_canonical_sorted(&const_addrs)
    .unwrap_or_else(ixon::merkle::zero_address);