Module context 

Building a compact, high-signal context bundle around one line of a Lean file.

The daily speedup this replaces is hand-copying imports, the enclosing theorem, the compiler errors, and the goal state into a chat prompt. Given a FILE.lean:LINE target, gather_context reads the source, optionally traces the file once for diagnostics and goal state, and returns a ContextBundle that serializes to JSON or renders to Markdown.

The bundle builder build_context is pure: it takes already-read source text plus optional diagnostics, so it is fully testable without touching the filesystem or spawning Lean.

Structs

ContextBundle

A compact context bundle around one line of a Lean file.

ContextOptions

Runtime options for gather_context when a live Lean trace is wanted.

ContextRequest

Where to center a context bundle and how much surrounding source to include.

Declaration

The enclosing declaration detected around the target line.

SourceLine

One numbered line of the surrounding source window.

SourceWindow

A window of source lines centered on the target line.

Functions

build_context

Assemble a bundle from already-read source and optional trace results.

collect_imports

Collect import lines (those starting at column zero) in source order.

detect_declaration

Detect the declaration enclosing target_idx, if any.

gather_context

Read the file, optionally trace it once, and assemble a ContextBundle.

parse_file_line_spec

Parse a FILE.lean:LINE target into its path and one-based line.