Expand description
Core primitives for Lean 4 tracing and theorem-agent evaluation.
The crate is intentionally split into small modules so the CLI remains thin and future users can reuse the library without depending on terminal UX.
The library never spawns a model: a runner is an external process that
eval talks to over a line-oriented contract. Pure parsing helpers like
parse_lean_diagnostics run without a Lean toolchain, which makes them the
easiest entry point:
use lean_agent_core::{parse_lean_diagnostics, DiagnosticSeverity};
let stderr = "Main.lean:3:0: error: unsolved goals\n⊢ 1 = 1";
let diagnostics = parse_lean_diagnostics(stderr, true);
assert_eq!(diagnostics.len(), 1);
assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Error);
assert_eq!(diagnostics[0].line, Some(3));
assert!(diagnostics[0].goal_state.is_some());Re-exports§
pub use accept::AXIOM_WHITELIST;pub use accept::AcceptOutcome;pub use accept::AcceptReport;pub use accept::AcceptRequest;pub use accept::GuardStatus;pub use accept::NegativeControl;pub use accept::RejectReason;pub use accept::check_negative_control;pub use accept::evaluate;pub use config::FileConfig;pub use config::ProjectConfig;pub use config::ReportConfig;pub use config::TraceConfig;pub use config::TraceFileConfig;pub use context::ContextBundle;pub use context::ContextOptions;pub use context::ContextRequest;pub use context::Declaration;pub use context::SourceLine;pub use context::SourceWindow;pub use context::build_context;pub use context::collect_imports;pub use context::detect_declaration;pub use context::gather_context;pub use context::parse_file_line_spec;pub use diagnostics::parse_lean_diagnostics;pub use discover::discover_lean_files;pub use error::Error;pub use error::Result;pub use eval::EvalOptions;pub use eval::EvalSummary;pub use eval::RunnerResponse;pub use eval::run_eval;pub use mine::AllowedEdit;pub use mine::MineKind;pub use mine::MineOptions;pub use mine::MineSummary;pub use mine::MineTask;pub use mine::TargetSpan;pub use mine::mine_errors;pub use mine::mine_placeholders;pub use mine::run_mine;pub use patch::AppliedPatch;pub use patch::SpanReplacement;pub use patch::apply_edits;pub use patch::apply_single_span;pub use process::LeanInvocation;pub use process::LeanRunOutput;pub use process::capture_provenance;pub use process::run_lean_file;pub use replay::Attempt;pub use replay::ReplayOptions;pub use replay::ReplayResult;pub use replay::ReplayStatus;pub use replay::ReplaySummary;pub use replay::run_replay;pub use report::Report;pub use report::build_report;pub use trace::TraceSummary;pub use trace::run_trace;pub use types::Diagnostic;pub use types::DiagnosticSeverity;pub use types::FileStatus;pub use types::FileTrace;pub use types::GoalState;pub use types::LeanFile;pub use types::Provenance;pub use types::TraceRecord;pub use workspace::CopyOptions;pub use workspace::Workspace;pub use writer::JsonlWriter;pub use writer::TraceWriter;pub use writer::write_jsonl;
Modules§
- accept
- Accept predicate for replayed proof attempts.
- config
- Configuration objects for tracing and reporting.
- context
- Building a compact, high-signal context bundle around one line of a Lean file.
- diagnostics
- Parsing Lean/Lake diagnostic output.
- discover
- Lean file discovery.
- error
- Error types for
lean-agent-core. - eval
- The agent stage: hand mined tasks to an external runner, collect attempts.
- mine
- Mining replayable proof tasks out of a Lean project.
- patch
- Bounded, line-spanned patch application into an isolated workspace copy.
- process
- Running external Lean/Lake processes and capturing run provenance.
- replay
- Replaying bounded proof attempts against isolated workspace copies.
- report
- Building human-readable summaries from trace records.
- trace
- Trace-run orchestration.
- types
- Stable data model for trace and evaluation artifacts.
- workspace
- Isolated, disposable copies of a Lake project for replay.
- writer
- Trace artifact writers.