Struct LeanResult 

pub struct LeanResult {
    pub receipt: Receipt,
    pub target_lean: String,
    pub target_logos: Option<String>,
    pub assumptions: Vec<String>,
    pub information_losses: Vec<Loss>,
    pub diagnostics: Vec<Diagnostic>,
    pub audit: Option<Value>,
    pub package: Option<PackageRef>,
}

A logos-lean-result/1 document under construction.

Fields

receipt: Receipt

target_lean: String

target_logos: Option<String>

assumptions: Vec<String>

information_losses: Vec<Loss>

diagnostics: Vec<Diagnostic>

audit: Option<Value>

The importer’s audit (logos-lean-import-report/1), when the import ran.

package: Option<PackageRef>

Implementations

impl LeanResult

pub fn new(target_lean: impl Into<String>) -> Self

A result for target in which nothing has run.

pub fn status(&self, stage: &str) -> StageStatus

pub fn pass(&mut self, stage: &'static str, detail: impl Into<String>)

pub fn mark( &mut self, stage: &'static str, status: StageStatus, diagnostic: Diagnostic, )

Record stage as status for the reason diagnostic gives.

pub fn fail(&mut self, stage: &'static str, diagnostic: Diagnostic)

stage failed for the reason diagnostic gives.

pub fn outcome(&self) -> Outcome

The outcome: the first stage that failed decides it; otherwise every stage passed (verified), or the first stage that did not decides it.

pub fn exit_code(&self) -> i32

pub fn finish(&mut self)

Explain a stage that did not run where it decides the outcome: when nothing failed, a lean_accepted stage that was never observed is the reason the result is not verified.

pub fn to_json(&self) -> Value

Trait Implementations

impl Clone for LeanResult

fn clone(&self) -> LeanResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanResult

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

Formats the value using the given formatter.

impl PartialEq for LeanResult

fn eq(&self, other: &LeanResult) -> 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 LeanResult