Enum Request 

#[non_exhaustive]
pub enum Request {
    Health,
    LoadFixtureCapability {
        fixture_root: String,
    },
    CallFixtureMul {
        fixture_root: String,
        lhs: u64,
        rhs: u64,
    },
    TriggerLeanPanic {
        fixture_root: String,
    },
    OpenHostSession {
        project_root: String,
        package: String,
        lib_name: String,
        imports: Vec<String>,
    },
    Elaborate {
        source: String,
        options: LeanWorkerElabOptions,
    },
    KernelCheck {
        source: String,
        options: LeanWorkerElabOptions,
        progress: bool,
    },
    DeclarationKinds {
        names: Vec<String>,
        progress: bool,
    },
    DeclarationNames {
        names: Vec<String>,
        progress: bool,
    },
    RunDataStream {
        export: String,
        request_json: String,
        progress: bool,
    },
    CapabilityMetadata {
        export: String,
        request_json: String,
    },
    CapabilityDoctor {
        export: String,
        request_json: String,
    },
    JsonCommand {
        export: String,
        request_json: String,
    },
    InferType {
        source: String,
        options: LeanWorkerElabOptions,
    },
    Whnf {
        source: String,
        options: LeanWorkerElabOptions,
    },
    IsDefEq {
        lhs: String,
        rhs: String,
        transparency: LeanWorkerMetaTransparency,
        options: LeanWorkerElabOptions,
    },
    Describe {
        name: String,
    },
    ListDeclarationsStrings {
        filter: LeanWorkerDeclarationFilter,
        progress: bool,
    },
    DescribeBulk {
        names: Vec<String>,
        progress: bool,
    },
    ProcessFile {
        source: String,
        options: LeanWorkerElabOptions,
    },
    ProcessModule {
        source: String,
        options: LeanWorkerElabOptions,
    },
    EmitTestRows {
        streams: Vec<String>,
    },
    EmitTestRowsThenExit,
    EmitTestRowsThenPanic,
    Terminate,
}

Parent-issued worker request body.

Variants (Non-exhaustive)

Non-exhaustive enums could have additional variants added in future. Therefore, when matching against variants of non-exhaustive enums, an extra wildcard arm must be added to account for any future variants.

Health

LoadFixtureCapability

Fields

fixture_root: String

CallFixtureMul

Fields

fixture_root: String

lhs: u64

rhs: u64

TriggerLeanPanic

Fields

fixture_root: String

OpenHostSession

Fields

project_root: String

package: String

lib_name: String

imports: Vec<String>

Elaborate

Fields

source: String

options: LeanWorkerElabOptions

KernelCheck

Fields

source: String

options: LeanWorkerElabOptions

progress: bool

DeclarationKinds

Fields

names: Vec<String>

progress: bool

DeclarationNames

Fields

names: Vec<String>

progress: bool

RunDataStream

Fields

export: String

request_json: String

progress: bool

CapabilityMetadata

Fields

export: String

request_json: String

CapabilityDoctor

Fields

export: String

request_json: String

JsonCommand

Fields

export: String

request_json: String

InferType

Fields

source: String

options: LeanWorkerElabOptions

Whnf

Fields

source: String

options: LeanWorkerElabOptions

IsDefEq

Fields

lhs: String

rhs: String

transparency: LeanWorkerMetaTransparency

options: LeanWorkerElabOptions

Describe

Fields

name: String

ListDeclarationsStrings

Fields

filter: LeanWorkerDeclarationFilter

progress: bool

DescribeBulk

Fields

names: Vec<String>

progress: bool

ProcessFile

Fields

source: String

options: LeanWorkerElabOptions

ProcessModule

Fields

source: String

options: LeanWorkerElabOptions

EmitTestRows

Fields

streams: Vec<String>

EmitTestRowsThenExit

EmitTestRowsThenPanic

Terminate

Trait Implementations

impl Clone for Request

fn clone(&self) -> Request

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Request

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Request

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for Request

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

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for Request

impl StructuralPartialEq for Request