lean_agent_core/
lib.rs

1//! Core primitives for Lean 4 tracing and theorem-agent evaluation.
2//!
3//! The crate is intentionally split into small modules so the CLI remains thin
4//! and future users can reuse the library without depending on terminal UX.
5//!
6//! The library never spawns a model: a runner is an external process that
7//! [`eval`] talks to over a line-oriented contract. Pure parsing helpers like
8//! [`parse_lean_diagnostics`] run without a Lean toolchain, which makes them the
9//! easiest entry point:
10//!
11//! ```
12//! use lean_agent_core::{parse_lean_diagnostics, DiagnosticSeverity};
13//!
14//! let stderr = "Main.lean:3:0: error: unsolved goals\n⊢ 1 = 1";
15//! let diagnostics = parse_lean_diagnostics(stderr, true);
16//!
17//! assert_eq!(diagnostics.len(), 1);
18//! assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Error);
19//! assert_eq!(diagnostics[0].line, Some(3));
20//! assert!(diagnostics[0].goal_state.is_some());
21//! ```
22
23#![warn(missing_docs)]
24
25pub mod accept;
26pub mod config;
27pub mod context;
28pub mod diagnostics;
29pub mod discover;
30pub mod error;
31pub mod eval;
32pub mod mine;
33pub mod patch;
34pub mod process;
35pub mod replay;
36pub mod report;
37pub mod trace;
38pub mod types;
39pub mod workspace;
40pub mod writer;
41
42pub use accept::{
43    AXIOM_WHITELIST, AcceptOutcome, AcceptReport, AcceptRequest, GuardStatus, NegativeControl,
44    RejectReason, check_negative_control, evaluate,
45};
46pub use config::{FileConfig, ProjectConfig, ReportConfig, TraceConfig, TraceFileConfig};
47pub use context::{
48    ContextBundle, ContextOptions, ContextRequest, Declaration, SourceLine, SourceWindow,
49    build_context, collect_imports, detect_declaration, gather_context, parse_file_line_spec,
50};
51pub use diagnostics::parse_lean_diagnostics;
52pub use discover::discover_lean_files;
53pub use error::{Error, Result};
54pub use eval::{EvalOptions, EvalSummary, RunnerResponse, run_eval};
55pub use mine::{
56    AllowedEdit, MineKind, MineOptions, MineSummary, MineTask, TargetSpan, mine_errors,
57    mine_placeholders, run_mine,
58};
59pub use patch::{AppliedPatch, SpanReplacement, apply_edits, apply_single_span};
60pub use process::{LeanInvocation, LeanRunOutput, capture_provenance, run_lean_file};
61pub use replay::{Attempt, ReplayOptions, ReplayResult, ReplayStatus, ReplaySummary, run_replay};
62pub use report::{Report, build_report};
63pub use trace::{TraceSummary, run_trace};
64pub use types::{
65    Diagnostic, DiagnosticSeverity, FileStatus, FileTrace, GoalState, LeanFile, Provenance,
66    TraceRecord,
67};
68pub use workspace::{CopyOptions, Workspace};
69pub use writer::{JsonlWriter, TraceWriter, write_jsonl};
lean_agent_core/lib.rs

lean_agent_core/
lib.rs
