Struct Build 

pub struct Build {
    pub files: PackageFiles,
    pub receipt: Receipt,
    pub audit: Stage,
}

A built package and the producing run’s receipt. A build never claims more than its receipt: assemble is the door that refuses to hand out a package whose receipt is not clean.

Fields

files: PackageFiles

receipt: Receipt

audit: Stage

The assumption policy over the checked proof alone: the audit of what it rests on, before the package’s contract holds that against Lean’s report. The receipt’s assumption_policy is this audit and then the contract’s agreement.