Function build_check_work

crates/ffi/src/kernel.rs:950–976

(
  ixon_env: &IxonEnv,
  names: &[Name],
  expect_pass: &[bool],
  ungrounded: &FxHashMap<Name, String>,
)

  Compile,
}

impl ErrKind {
  fn tag(self) -> u8 {
    match self {
      ErrKind::Kernel => KERNEL_EXCEPTION_TAG,
      ErrKind::Compile => COMPILE_ERROR_TAG,
    }
  }
}

/// Per-constant result: `Ok(())` on pass, `Err((kind, msg))` on rejection.
type CheckRes = Result<(), (ErrKind, String)>;

const KERNEL_CHECK_STACK_SIZE: usize = 256 * 1024 * 1024;

unsafe extern "C" {
  /// Lean runtime (`src/util/thread.cpp`): stack size, in bytes, for
  /// subsequently spawned `lthread`s — dedicated task threads and new
  /// task-pool workers. This is the knob behind `lean --tstack`.
  fn lean_internal_set_thread_stack_size(size: usize);
}

/// `Ix.Tc.setLeanThreadStackSize : USize → BaseIO Unit`
///
/// ABI adapter: the runtime setter is a bare `void(size_t)`, so Lean can't
/// `@[extern]` it directly. The pure-Lean parallel checker calls this before
/// spawning its `.dedicated` workers so they get `KERNEL_CHECK_STACK_SIZE`-
/// class stacks — deep recursor expansions overflow the default 8 MB
/// `lthread` stack just like they would the Rust workers' (see above).
#[unsafe(no_mangle)]