Enum LeanSessionImportProfile 

pub enum LeanSessionImportProfile {
    ExportedPublic,
    Server,
    Private,
    FullPrivateCompat,
}

Closed import profiles for full host sessions.

Profiles intentionally expose names tied to host semantics rather than raw Lean import knobs. All full-session profiles keep loadExts := true; the no-extension variant remains a profiling-only diagnostic path and never produces a normal LeanSession. Because full sessions load environment extensions, they are not eligible for Environment.freeRegions cleanup; use a worker process boundary to reset Lean import state.

Variants

ExportedPublic

Public exported declarations only, with environment extensions loaded.

Server

Server-level import data without import all, with environment extensions loaded.

Private

Private-level import data without import all, with environment extensions loaded.

FullPrivateCompat

Legacy compatibility import shape: import all, private level, with environment extensions loaded.

Implementations

impl LeanSessionImportProfile

pub const fn label(self) -> &'static str

pub const fn import_all(self) -> bool

pub const fn import_level(self) -> LeanImportLevel

pub const fn load_exts(self) -> bool

Trait Implementations

impl Clone for LeanSessionImportProfile

fn clone(&self) -> LeanSessionImportProfile

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for LeanSessionImportProfile

impl Debug for LeanSessionImportProfile

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

Formats the value using the given formatter.

impl Default for LeanSessionImportProfile

fn default() -> LeanSessionImportProfile

Returns the “default value” for a type.

impl Eq for LeanSessionImportProfile

impl PartialEq for LeanSessionImportProfile

fn eq(&self, other: &LeanSessionImportProfile) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for LeanSessionImportProfile