Method report

crates/ffi/src/kernel.rs:2642–2720

(&self)

      "[123/456] _private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Proof";
    let compact = compact_in_flight_label(label, 40);
    assert!(compact.starts_with("[123/456] ..."));
    assert!(compact.ends_with("Internal.Formula.Proof"));
    assert!(compact.chars().count() <= 40);
  }

  #[test]
  fn compact_in_flight_label_handles_tiny_limits() {
    assert_eq!(compact_in_flight_label("[1/2] Very.Long.Name", 0), "");
    assert_eq!(compact_in_flight_label("[1/2] Very.Long.Name", 2), "[1");
  }
}

/// Default threshold at and above which a completed check is "slow" enough to
/// keep a persistent line in quiet mode. Override with
/// `IX_KERNEL_CHECK_SLOW_MS`.
const DEFAULT_SLOW_THRESHOLD: Duration = Duration::from_secs(7);

/// Default threshold for a one-shot "still checking ..." line when an active
/// parallel check has been in-flight for a long time. Override with
/// `IX_KERNEL_CHECK_ACTIVE_SLOW_MS`; set it to `0` to disable the notice.
const DEFAULT_ACTIVE_SLOW_THRESHOLD: Duration = Duration::from_secs(30);

const DEFAULT_IN_FLIGHT_LIMIT: usize = 3;
const DEFAULT_IN_FLIGHT_LABEL_CHARS: usize = 120;
const DEFAULT_CHECK_CLEAR_EVERY: usize = 1;

fn env_duration_ms(var: &str, default: Duration) -> Duration {
  std::env::var(var)
    .ok()
    .and_then(|s| s.parse::<u64>().ok())
    .map_or(default, Duration::from_millis)
}

fn env_duration_ms_optional(var: &str, default: Duration) -> Option<Duration> {
  let ms = std::env::var(var)
    .ok()
    .and_then(|s| s.parse::<u64>().ok())
    .unwrap_or_else(|| u64::try_from(default.as_millis()).unwrap_or(u64::MAX));
  if ms == 0 { None } else { Some(Duration::from_millis(ms)) }
}

fn env_usize(var: &str, default: usize) -> usize {
  std::env::var(var)
    .ok()
    .and_then(|s| s.parse::<usize>().ok())
    .unwrap_or(default)
}

fn kernel_check_slow_threshold() -> Duration {
  env_duration_ms("IX_KERNEL_CHECK_SLOW_MS", DEFAULT_SLOW_THRESHOLD)
}

fn kernel_check_clear_every() -> usize {
  env_usize("IX_KERNEL_CHECK_CLEAR_EVERY", DEFAULT_CHECK_CLEAR_EVERY).max(1)
}

/// Threshold (max cache len) above which a per-block diagnostic line is
/// emitted, when `IX_KERNEL_CHECK_DIAG=1`. Default 100k entries — empirically