Struct OptionsBuilder

pub struct OptionsBuilder { /* private fields */ }

Builder that conveniently allows to specify common Isabelle options.

Implementations

impl OptionsBuilder

pub fn new() -> Self

pub fn threads(&mut self, threads: isize) -> &mut Self

Maximum number of worker threads for prover process (0 = hardware max.)

pub fn thread_stack_limit(&mut self, limit: f32) -> &mut Self

Maximum stack size for worker threads (in giga words, 0 = unlimited)

pub fn parallel_limit(&mut self, limit: isize) -> &mut Self

Approximative limit for parallel tasks (0 = unlimited)

pub fn parallel_proofs(&mut self, limit: isize) -> &mut Self

Level of parallel proof checking: 0, 1, 2

pub fn timeout_scale(&mut self, scale: f32) -> &mut Self

Scale factor for timeout in Isabelle/ML and session build

pub fn record_proofs(&mut self, level: isize) -> &mut Self

Level of proofterm recording: 0, 1, 2, negative means unchanged

pub fn quick_and_dirty(&mut self, flag: bool) -> &mut Self

If true then some tools will OMIT some proofs

pub fn skip_proofs(&mut self, flag: bool) -> &mut Self

If true then skips over proofs (implicit ‘sorry’)

pub fn timeout(&mut self, limit: f32) -> &mut Self

Timeout for session build job (seconds > 0)

pub fn timeout_build(&mut self, flag: bool) -> &mut Self

pub fn process_output_limit(&mut self, limit: isize) -> &mut Self

Build process output limit (in million characters, 0 = unlimited)

pub fn process_output_tail(&mut self, tail: isize) -> &mut Self

Build process output tail shown to user (in lines, 0 = unlimited)

pub fn pide_reports(&mut self, flag: bool) -> &mut Self

pub fn build_pide_reports(&mut self, flag: bool) -> &mut Self

Trait Implementations

impl Default for OptionsBuilder

fn default() -> OptionsBuilder

Returns the “default value” for a type.

impl From<OptionsBuilder> for HashMap<String, String>

fn from(val: OptionsBuilder) -> Self

Consumes the builder and return a key value map of the specified options.