#![allow(clippy::expect_used, clippy::panic, clippy::wildcard_enum_match_arm)]
use std::path::PathBuf;
use std::sync::Mutex;
use lean_rs::{HostStage, LeanDiagnosticCode, LeanError, LeanRuntime};
use lean_rs_host::{
LeanCancellationToken, LeanCapabilities, LeanHost, LeanProgressEvent, LeanProgressSink, LeanSession,
};
fn fixture_lake_root() -> PathBuf {
let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
let workspace = manifest_dir
.parent()
.and_then(std::path::Path::parent)
.expect("crates/<name>/ lives two directories beneath the workspace root");
workspace.join("fixtures").join("lean")
}
fn runtime() -> &'static LeanRuntime {
LeanRuntime::init().expect("Lean runtime initialisation must succeed")
}
fn fixture_host() -> LeanHost<'static> {
LeanHost::from_lake_project(runtime(), fixture_lake_root()).expect("host opens cleanly")
}
fn session_over_handles<'lean, 'c>(caps: &'c LeanCapabilities<'lean, 'c>) -> LeanSession<'lean, 'c> {
caps.session(&["LeanRsFixture.Handles"], None, None)
.expect("session imports cleanly")
}
#[derive(Default)]
struct RecordingSink {
events: Mutex<Vec<LeanProgressEvent>>,
}
impl RecordingSink {
fn events(&self) -> Vec<LeanProgressEvent> {
self.events.lock().expect("progress event lock is not poisoned").clone()
}
}
impl LeanProgressSink for RecordingSink {
fn report(&self, event: LeanProgressEvent) {
self.events
.lock()
.expect("progress event lock is not poisoned")
.push(event);
}
}
struct CancelOnFirstEvent<'a> {
token: &'a LeanCancellationToken,
events: Mutex<Vec<LeanProgressEvent>>,
}
impl LeanProgressSink for CancelOnFirstEvent<'_> {
fn report(&self, event: LeanProgressEvent) {
self.events
.lock()
.expect("progress event lock is not poisoned")
.push(event);
if event.current >= 1 {
self.token.cancel();
}
}
}
struct PanicSink;
impl LeanProgressSink for PanicSink {
fn report(&self, event: LeanProgressEvent) {
panic!("lean-rs progress sink deliberate panic at {}", event.current);
}
}
fn assert_cancelled(err: LeanError) {
assert_eq!(err.code(), LeanDiagnosticCode::Cancelled);
match err {
LeanError::Cancelled(_) => {}
other @ (LeanError::LeanException(_) | LeanError::Host(_)) => {
panic!("expected LeanError::Cancelled, got {other:?}");
}
other => panic!("expected LeanError::Cancelled, got {other:?}"),
}
}
#[test]
fn query_declarations_bulk_reports_ordered_multi_phase_progress() {
let host = fixture_host();
let caps = host
.load_capabilities("lean_rs_fixture", "LeanRsFixture")
.expect("load caps");
let mut session = session_over_handles(&caps);
let sink = RecordingSink::default();
let names = [
"LeanRsFixture.Handles.nameAnonymous",
"LeanRsFixture.Handles.nameMkStr",
"LeanRsFixture.Handles.exprConstNat",
];
let decls = session
.query_declarations_bulk(&names, None, Some(&sink))
.expect("progress bulk query succeeds");
assert_eq!(decls.len(), names.len());
let events = sink.events();
assert_eq!(events.len(), names.len() * 2, "prepare + query phase per item");
assert!(
events
.iter()
.take(names.len())
.all(|event| event.phase == "prepare_names"),
"first phase prepares names: {events:?}",
);
assert!(
events
.iter()
.skip(names.len())
.all(|event| event.phase == "query_declarations_bulk"),
"second phase queries declarations: {events:?}",
);
for (idx, event) in events.iter().take(names.len()).enumerate() {
assert_eq!(
event.current,
u64::try_from(idx.saturating_add(1)).expect("idx fits u64")
);
assert_eq!(event.total, Some(names.len() as u64));
}
for (idx, event) in events.iter().skip(names.len()).enumerate() {
assert_eq!(
event.current,
u64::try_from(idx.saturating_add(1)).expect("idx fits u64")
);
assert_eq!(event.total, Some(names.len() as u64));
}
}
#[test]
fn progress_current_is_monotonic_within_each_phase() {
let host = fixture_host();
let caps = host
.load_capabilities("lean_rs_fixture", "LeanRsFixture")
.expect("load caps");
let mut session = session_over_handles(&caps);
let sink = RecordingSink::default();
let names = [
"LeanRsFixture.Handles.nameAnonymous",
"LeanRsFixture.Handles.nameMkStr",
"LeanRsFixture.Handles.exprConstNat",
"LeanRsFixture.Handles.nameToString",
];
session
.query_declarations_bulk(&names, None, Some(&sink))
.expect("progress bulk query succeeds");
let events = sink.events();
for phase in ["prepare_names", "query_declarations_bulk"] {
let mut last = 0;
for event in events.iter().filter(|event| event.phase == phase) {
assert!(
event.current >= last,
"phase {phase} regressed from {last} to {}",
event.current,
);
last = event.current;
}
}
}
#[test]
fn pre_cancelled_progress_call_records_no_dispatch_or_event() {
let host = fixture_host();
let caps = host
.load_capabilities("lean_rs_fixture", "LeanRsFixture")
.expect("load caps");
let mut session = session_over_handles(&caps);
let sink = RecordingSink::default();
let token = LeanCancellationToken::new();
token.cancel();
let before = session.stats();
let err = session
.declaration_kind_bulk(&["LeanRsFixture.Handles.nameAnonymous"], Some(&token), Some(&sink))
.expect_err("pre-cancelled progress call must fail");
assert_cancelled(err);
assert_eq!(session.stats(), before, "pre-cancelled call records no FFI");
assert!(sink.events().is_empty(), "pre-cancelled call emits no progress");
}
#[test]
fn sink_triggered_cancellation_fires_at_next_progress_boundary() {
let host = fixture_host();
let caps = host
.load_capabilities("lean_rs_fixture", "LeanRsFixture")
.expect("load caps");
let mut session = session_over_handles(&caps);
let token = LeanCancellationToken::new();
let sink = CancelOnFirstEvent {
token: &token,
events: Mutex::new(Vec::new()),
};
let names = [
"LeanRsFixture.Handles.nameAnonymous",
"LeanRsFixture.Handles.nameMkStr",
"LeanRsFixture.Handles.exprConstNat",
];
let err = session
.declaration_kind_bulk(&names, Some(&token), Some(&sink))
.expect_err("sink-triggered cancellation must fail the operation");
assert_cancelled(err);
assert!(
session.stats().ffi_calls > 0,
"first item dispatched before cancellation"
);
let first_phase = {
let events = sink.events.lock().expect("progress event lock is not poisoned");
assert_eq!(events.len(), 1, "cancellation fires at the next loop boundary");
events.first().expect("one progress event was recorded").phase
};
assert_eq!(first_phase, "declaration_kind_bulk");
}
#[test]
fn progress_sink_panic_is_contained_by_callback_trampoline() {
let host = fixture_host();
let caps = host
.load_capabilities("lean_rs_fixture", "LeanRsFixture")
.expect("load caps");
let mut session = session_over_handles(&caps);
let err = session
.declaration_kind_bulk(&["LeanRsFixture.Handles.nameAnonymous"], None, Some(&PanicSink))
.expect_err("progress sink panic must become a host error");
assert_eq!(err.code(), LeanDiagnosticCode::Internal);
match err {
LeanError::Host(failure) => {
assert_eq!(failure.stage(), HostStage::CallbackPanic);
assert!(
failure.message().contains("lean-rs progress sink deliberate panic"),
"panic message should be preserved, got {:?}",
failure.message(),
);
}
other @ (LeanError::LeanException(_) | LeanError::Cancelled(_)) => {
panic!("expected Host(CallbackPanic), got {other:?}");
}
other => panic!("expected Host(CallbackPanic), got {other:?}"),
}
}
#[test]
fn no_progress_bulk_path_remains_one_dispatch() {
let host = fixture_host();
let caps = host
.load_capabilities("lean_rs_fixture", "LeanRsFixture")
.expect("load caps");
let mut session = session_over_handles(&caps);
let names = [
"LeanRsFixture.Handles.nameAnonymous",
"LeanRsFixture.Handles.nameMkStr",
"LeanRsFixture.Handles.exprConstNat",
];
let before = session.stats();
let kinds = session
.declaration_kind_bulk(&names, None, None)
.expect("no-progress bulk query succeeds");
let after = session.stats();
assert_eq!(kinds.len(), names.len());
assert_eq!(after.ffi_calls - before.ffi_calls, 1);
assert_eq!(after.batch_items - before.batch_items, names.len() as u64);
}