Function rs_kernel_roundtrip_no_compile

crates/ffi/src/kernel.rs:3423–3471

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

      let mut active = self.active.lock().unwrap();
      let mut active_slow_lines = Vec::new();
      if let Some(active_slow_threshold) = self.active_slow_threshold {
        for slot in active.iter_mut() {
          if let Some(check) = slot.as_mut() {
            let age = check.started.elapsed();
            if !check.reported_active_slow && age >= active_slow_threshold {
              check.reported_active_slow = true;
              active_slow_lines.push(format!(
                "[rs_kernel_check] still checking {} after {:.0}s",
                compact_in_flight_label(
                  &check.label,
                  self.in_flight_label_chars
                ),
                age.as_secs_f64()
              ));
            }
          }
        }
      }

      let mut entries: Vec<_> = active
        .iter()
        .filter_map(|slot| {
          slot.as_ref().map(|check| (check.started, check.label.clone()))
        })
        .collect();
      entries.sort_by_key(|(started, _)| *started);
      let in_flight = entries
        .into_iter()
        .take(self.in_flight_limit)
        .map(|(started, label)| {
          format!(
            "{} ({:.0}s)",
            compact_in_flight_label(&label, self.in_flight_label_chars),
            started.elapsed().as_secs_f64()
          )
        })
        .collect::<Vec<_>>();
      (in_flight, active_slow_lines)
    };
    let active_suffix = if in_flight.is_empty() {
      String::new()
    } else {
      format!(" · in-flight: {}", in_flight.join(", "))
    };
    let mem_suffix = kernel_check_mem_suffix(Some(&self.peak_rss_mib));

    self.log(&format!(
      "[rs_kernel_check] {done}/{} ({pct:.1}%) · {:.1}/s · elapsed {:.0}s{eta}{mem_suffix}{active_suffix}",
      self.total,
      rate,
      elapsed,
    ));