Skip to main content

Run

Struct Run 

Source
pub struct Run<S> { /* private fields */ }

Implementations§

Source§

impl Run<Active>

Source

pub fn dispatch( plan: RunPlan, ledger: &mut dyn Ledger, hooks: &mut RunHooks<'_>, ) -> Result<Run<Active>, AxError>

The dispatch pair: the job pin lands first, then the run exists. Two ledger lines, two clock samples — the pin is a fact about the city and the start is a fact about the run. Written by the plan’s charter, the one author of every run’s opening (crates/runtime/spec/Run.lean §8-52).

§Errors

Propagates whatever the ledger says; nothing else here can fail.

Source

pub fn advance( &mut self, ledger: &mut dyn Ledger, model: &mut dyn Model, hooks: &mut RunHooks<'_>, ) -> Result<Advance, AxError>

Takes one turn. Every exit from a phase is either the next phase or a cancellation, so the three safe points are the only places an interruption can land.

§Errors

Propagates ledger and provider failures. A tool failure is not one of them: it reaches the model as this call’s result.

Source

pub fn freeze( self, ledger: &mut dyn Ledger, handoff: &Handoff, completion: Completion, hooks: &mut RunHooks<'_>, ) -> Result<Run<Frozen>, AxError>

The only exit. Both lines are written here, so no caller can end a run by simply dropping it and leaving the ledger without a verdict.

A cancelled run freezes inside the turn it interrupted and carries that turn’s stamp; any other ending samples the clock once, and run_frozen follows one millisecond later because the two lines record one event.

§Errors

Propagates ledger failures and a clock that has run past u64.

Source

pub fn turns_taken(&self) -> u32

Source§

impl Run<Frozen>

Source

pub fn completion(&self) -> &Completion

Source

pub fn plan(&self) -> &RunPlan

What this run was dispatched with, for a successor that takes the same work on.

Source

pub fn transcript(&self) -> Result<Transcript, AxError>

What the model saw, scanned and ready to write beside the room.

§Errors

Propagates a message that will not serialise.

Source

pub fn turns(&self) -> u32

Source

pub fn run_id(&self) -> RunId

Auto Trait Implementations§

§

impl<S> Freeze for Run<S>
where S: Freeze,

§

impl<S> RefUnwindSafe for Run<S>
where S: RefUnwindSafe,

§

impl<S> Send for Run<S>
where S: Send,

§

impl<S> Sync for Run<S>
where S: Sync,

§

impl<S> Unpin for Run<S>
where S: Unpin,

§

impl<S> UnsafeUnpin for Run<S>
where S: UnsafeUnpin,

§

impl<S> UnwindSafe for Run<S>
where S: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = !

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, !>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.