Function rs_kernel_check_consts

crates/ffi/src/kernel.rs:222–343

(
  env_consts: LeanList<LeanBorrowed<'_>>,
  names: LeanArray<LeanBorrowed<'_>>,
  expect_pass: LeanArray<LeanBorrowed<'_>>,
  quiet: LeanBool<LeanBorrowed<'_>>,
)

/// `IX_KERNEL_CHECK_NAME_CHARS`.
#[unsafe(no_mangle)]
pub extern "C" fn rs_kernel_check_consts(
  env_consts: LeanList<LeanBorrowed<'_>>,
  names: LeanArray<LeanBorrowed<'_>>,
  expect_pass: LeanArray<LeanBorrowed<'_>>,
  quiet: LeanBool<LeanBorrowed<'_>>,
) -> LeanIOResult<LeanOwned> {
  let total_start = Instant::now();
  let quiet = quiet.to_bool();

  // ---------------------------------------------------------------------
  // Decode inputs
  // ---------------------------------------------------------------------
  let t0 = Instant::now();
  let rust_env = decode_env(env_consts);
  // Decode names structurally — no `Name.toString` / `parse_name` dance.
  // The resulting `Name`s are byte-for-byte the same as the kernel's
  // stored names (same component strings, same content hash).
  let names_vec: Vec<Name> = decode_name_array(&names);
  // `Array Bool` elements are boxed tagged scalars:
  // `lean_box(n) = (n << 1) | 1`, so `Bool.false` has raw value 1 and
  // `Bool.true` has raw value 3. `unbox_usize()` (= `as_raw() >> 1`)
  // recovers the ctor tag (0 = false, 1 = true).
  let expect_pass_vec: Vec<bool> =
    expect_pass.map(|b| b.unbox_usize() == 1).into_iter().collect();
  eprintln!("[rs_kernel_check] read env:   {:>8.1?}", t0.elapsed());

  // ---------------------------------------------------------------------
  // Compile Lean → Ixon
  // ---------------------------------------------------------------------
  let t1 = Instant::now();
  let rust_env_arc = Arc::new(rust_env);
  let compile_state =
    match compile_env_with_options(&rust_env_arc, CompileOptions::default()) {
      Ok(s) => s,
      Err(e) => {
        return build_uniform_error(
          names_vec.len(),
          &format!("[compile] {e:?}"),
        );
      },
    };
  eprintln!("[rs_kernel_check] compile:    {:>8.1?}", t1.elapsed());

  let CompileState { env: ixon_env, ungrounded: compile_ungrounded, .. } =
    compile_state;

  // Snapshot per-constant compile failures (ill-formed inductives,
  // cascading MissingConstant, etc.) keyed by `Name` so the check loop
  // can skip the kernel and report them as compile-side rejections.
  // `compile_env` no longer aborts on per-block failure; it populates
  // `CompileState.ungrounded` and continues, letting good constants still
  // compile cleanly.
  let ungrounded: FxHashMap<Name, String> = compile_ungrounded
    .iter()
    .map(|e| (e.key().clone(), e.value().clone()))
    .collect();
  drop(compile_ungrounded);
  drop(rust_env_arc);