Struct AcceptRequest 

pub struct AcceptRequest<'a> {
    pub lake_root: &'a Utf8Path,
    pub workspace_root: &'a Utf8Path,
    pub target: &'a Utf8Path,
    pub edit_line: u32,
    pub patched_diagnostics: &'a [Diagnostic],
    pub provenance: &'a Provenance,
    pub timeout: Duration,
    pub run_reverse_dep: bool,
    pub negative_control: Option<&'a NegativeControl>,
}

Everything the accept predicate needs for one attempt.

Fields

lake_root: &'a Utf8Path

Source-of-truth project root (holds the pre-edit file).

workspace_root: &'a Utf8Path

Patched workspace copy root (holds the post-edit file).

target: &'a Utf8Path

Target file, relative to each root.

edit_line: u32

One-based first line the edit was allowed to touch.

patched_diagnostics: &'a [Diagnostic]

Diagnostics from the patched compile (used to spot a sorry warning).

provenance: &'a Provenance

Tooling provenance for any Lean run.

timeout: Duration

Per-command timeout for axiom and build checks.

run_reverse_dep: bool

Run the reverse-dependency guard (guard 3).

negative_control: Option<&'a NegativeControl>

Negative-control manifest, when the loop supplies one (guard 4).

Trait Implementations

impl<'a> Clone for AcceptRequest<'a>

fn clone(&self) -> AcceptRequest<'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'a> Debug for AcceptRequest<'a>

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

Formats the value using the given formatter.