#![allow(clippy::expect_used, clippy::panic, clippy::wildcard_enum_match_arm)]
use std::path::{Path, PathBuf};
use std::sync::Mutex;
use lean_rs::LeanRuntime;
use lean_rs_host::{EvidenceStatus, LeanElabOptions, LeanHost};
use lean_rs_worker::{
LeanWorker, LeanWorkerCancellationToken, LeanWorkerConfig, LeanWorkerElabOptions, LeanWorkerError,
LeanWorkerKernelStatus, LeanWorkerProgressEvent, LeanWorkerProgressSink, LeanWorkerSessionConfig,
};
fn worker_binary() -> PathBuf {
PathBuf::from(env!("CARGO_BIN_EXE_lean-rs-worker-child"))
}
fn workspace_root() -> PathBuf {
let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
manifest_dir
.parent()
.and_then(Path::parent)
.expect("crates/<name> lives two directories below the workspace root")
.to_path_buf()
}
fn fixture_root() -> PathBuf {
workspace_root().join("fixtures").join("lean")
}
fn ensure_fixture_built() {
let fixture = fixture_root();
lean_toolchain::build_lake_target_quiet(&fixture, "LeanRsFixture").expect("fixture Lake target builds");
}
fn worker_config() -> LeanWorkerConfig {
LeanWorkerConfig::new(worker_binary())
}
fn handles_session_config() -> LeanWorkerSessionConfig {
LeanWorkerSessionConfig::new(
fixture_root(),
"lean_rs_fixture",
"LeanRsFixture",
["LeanRsFixture.Handles"],
)
}
fn elaboration_session_config() -> LeanWorkerSessionConfig {
LeanWorkerSessionConfig::new(
fixture_root(),
"lean_rs_fixture",
"LeanRsFixture",
["LeanRsHostShims.Elaboration"],
)
}
fn runtime() -> &'static LeanRuntime {
LeanRuntime::init().expect("Lean runtime initialisation must succeed")
}
fn direct_host() -> LeanHost<'static> {
LeanHost::from_lake_project(runtime(), fixture_root()).expect("host opens cleanly")
}
#[derive(Default)]
struct RecordingSink {
events: Mutex<Vec<LeanWorkerProgressEvent>>,
}
impl RecordingSink {
fn events(&self) -> Vec<LeanWorkerProgressEvent> {
self.events.lock().expect("progress lock is not poisoned").clone()
}
}
impl LeanWorkerProgressSink for RecordingSink {
fn report(&self, event: LeanWorkerProgressEvent) {
self.events.lock().expect("progress lock is not poisoned").push(event);
}
}
struct CancelOnFirstProgress<'a> {
token: &'a LeanWorkerCancellationToken,
events: Mutex<Vec<LeanWorkerProgressEvent>>,
}
impl LeanWorkerProgressSink for CancelOnFirstProgress<'_> {
fn report(&self, event: LeanWorkerProgressEvent) {
self.events.lock().expect("progress lock is not poisoned").push(event);
self.token.cancel();
}
}
#[test]
fn declaration_bulk_adapter_matches_in_process_session() {
ensure_fixture_built();
let names = [
"LeanRsFixture.Handles.nameAnonymous",
"LeanRsFixture.Handles.nameMkStr",
"LeanRsFixture.Handles.exprConstNat",
"This.Name.Does.Not.Exist",
];
let host = direct_host();
let caps = host
.load_capabilities("lean_rs_fixture", "LeanRsFixture")
.expect("fixture capability loads");
let mut direct = caps
.session(&["LeanRsFixture.Handles"], None, None)
.expect("direct session opens");
let direct_kinds = direct
.declaration_kind_bulk(&names, None, None)
.expect("direct kind bulk succeeds");
let direct_names = direct
.declaration_name_bulk(&names, None, None)
.expect("direct name bulk succeeds");
let mut worker = LeanWorker::spawn(&worker_config()).expect("worker starts");
let mut session = worker
.open_session(&handles_session_config(), None, None)
.expect("worker session opens");
let worker_kinds = session
.declaration_kinds(&names, None, None)
.expect("worker kind bulk succeeds");
let worker_names = session
.declaration_names(&names, None, None)
.expect("worker name bulk succeeds");
assert_eq!(worker_kinds, direct_kinds);
assert_eq!(worker_names, direct_names);
}
#[test]
fn elaboration_and_kernel_adapter_match_status_shape() {
ensure_fixture_built();
let opts = LeanWorkerElabOptions::new();
let mut worker = LeanWorker::spawn(&worker_config()).expect("worker starts");
let mut session = worker
.open_session(&elaboration_session_config(), None, None)
.expect("worker session opens");
let ok = session
.elaborate("(1 + 1 : Nat)", &opts, None, None)
.expect("worker elaboration dispatch succeeds");
let bad = session
.elaborate("1 +", &opts, None, None)
.expect("worker failed elaboration returns diagnostics");
let checked = session
.kernel_check("theorem lean_rs_worker_checked : 1 + 1 = 2 := rfl", &opts, None, None)
.expect("worker kernel check dispatch succeeds");
assert!(ok.success);
assert!(!bad.success);
assert!(!bad.diagnostics.is_empty(), "failed elaboration carries diagnostics");
assert_eq!(checked.status, LeanWorkerKernelStatus::Checked);
let host = direct_host();
let caps = host
.load_capabilities("lean_rs_fixture", "LeanRsFixture")
.expect("fixture capability loads");
let mut direct = caps
.session(&["LeanRsHostShims.Elaboration"], None, None)
.expect("direct session opens");
let direct_status = direct
.kernel_check(
"theorem lean_rs_worker_checked_direct : 1 + 1 = 2 := rfl",
&LeanElabOptions::new(),
None,
None,
)
.expect("direct kernel check succeeds")
.status();
assert_eq!(direct_status, EvidenceStatus::Checked);
}
#[test]
fn progress_events_cross_worker_boundary_in_order() {
ensure_fixture_built();
let names = [
"LeanRsFixture.Handles.nameAnonymous",
"LeanRsFixture.Handles.nameMkStr",
"LeanRsFixture.Handles.exprConstNat",
];
let sink = RecordingSink::default();
let mut worker = LeanWorker::spawn(&worker_config()).expect("worker starts");
let mut session = worker
.open_session(&handles_session_config(), None, None)
.expect("worker session opens");
let kinds = session
.declaration_kinds(&names, None, Some(&sink))
.expect("worker kind bulk with progress succeeds");
assert_eq!(kinds.len(), names.len());
let events = sink.events();
assert_eq!(events.len(), names.len());
for (idx, event) in events.iter().enumerate() {
assert_eq!(event.phase, "declaration_kind_bulk");
assert_eq!(event.current, u64::try_from(idx + 1).expect("idx fits u64"));
assert_eq!(event.total, Some(names.len() as u64));
}
}
#[test]
fn parent_can_cancel_long_worker_request_at_progress_boundary() {
ensure_fixture_built();
let token = LeanWorkerCancellationToken::new();
let sink = CancelOnFirstProgress {
token: &token,
events: Mutex::new(Vec::new()),
};
let names = vec!["LeanRsFixture.Handles.nameAnonymous"; 20_000];
let mut worker = LeanWorker::spawn(&worker_config()).expect("worker starts");
let mut session = worker
.open_session(&handles_session_config(), None, None)
.expect("worker session opens");
let err = session
.declaration_kinds(&names, Some(&token), Some(&sink))
.expect_err("parent cancellation should stop worker request");
match err {
LeanWorkerError::Cancelled { operation } => assert_eq!(operation, "worker_declaration_kinds"),
other => panic!("expected worker cancellation, got {other:?}"),
}
assert!(
!sink.events.lock().expect("progress lock is not poisoned").is_empty(),
"cancellation happens after at least one worker progress event",
);
}