Struct ContextOptions 

pub struct ContextOptions {
    pub run_trace: bool,
    pub lake_root: Utf8PathBuf,
    pub timeout: Duration,
    pub include_warnings: bool,
}

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

Fields

run_trace: bool

Run lake lean over the file to attach diagnostics and goal state.

lake_root: Utf8PathBuf

Lake workspace root used for the trace and provenance probes.

timeout: Duration

Process timeout for the trace.

include_warnings: bool

Keep warning diagnostics in the bundle.

Implementations

impl ContextOptions

pub fn new(lake_root: Utf8PathBuf) -> Self

Tracing options rooted at lake_root with a sixty-second timeout.

Trait Implementations

impl Clone for ContextOptions

fn clone(&self) -> ContextOptions

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ContextOptions

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for ContextOptions

impl PartialEq for ContextOptions

fn eq(&self, other: &ContextOptions) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for ContextOptions