Module Setup Information

Data types used by Lean module headers and the --setup CLI.

structure Lean.Import : Type

• module : Name
• importAll : Bool

  import all; whether to import and expose all data saved by the module.

• isExported : Bool

  Whether to activate this import when the current module itself is imported.

• isMeta : Bool

  Whether all definitions (transitively) reachable through the

instance Lean.instReprImport : Repr Import

Equations

• Lean.instReprImport = { reprPrec := Lean.reprImport✝ }

instance Lean.instInhabitedImport : Inhabited Import

Equations

• Lean.instInhabitedImport = { default := { module := default, importAll := default, isExported := default, isMeta := default } }

instance Lean.instToJsonImport : ToJson Import

Equations

• Lean.instToJsonImport = { toJson := Lean.toJsonImport✝ }

instance Lean.instFromJsonImport : FromJson Import

Equations

• Lean.instFromJsonImport = { fromJson? := Lean.fromJsonImport✝ }

instance Lean.instCoeNameImport : Coe Name Import

Equations

• Lean.instCoeNameImport = { coe := fun (x : Lean.Name) => { module := x } }

instance Lean.instToStringImport : ToString Import

Equations

• Lean.instToStringImport = { toString := fun (imp : Lean.Import) => toString imp.module }

structure Lean.ModuleHeader : Type

Abstract structure of a module's header.

• imports : Array Import

  The module's direct imports (i.e., those listed in the header).

• isModule : Bool

  Whether the module is participating in the module system.

instance Lean.instReprModuleHeader : Repr ModuleHeader

Equations

• Lean.instReprModuleHeader = { reprPrec := Lean.reprModuleHeader✝ }

instance Lean.instInhabitedModuleHeader : Inhabited ModuleHeader

Equations

• Lean.instInhabitedModuleHeader = { default := { imports := default, isModule := default } }

instance Lean.instToJsonModuleHeader : ToJson ModuleHeader

Equations

• Lean.instToJsonModuleHeader = { toJson := Lean.toJsonModuleHeader✝ }

instance Lean.instFromJsonModuleHeader : FromJson ModuleHeader

Equations

• Lean.instFromJsonModuleHeader = { fromJson? := Lean.fromJsonModuleHeader✝ }

structure Lean.ImportArtifacts : Type

Module data files used for an import statement. This structure is designed for efficient JSON serialization.

• oleanParts : Array System.FilePath

instance Lean.instReprImportArtifacts : Repr ImportArtifacts

Equations

• Lean.instReprImportArtifacts = { reprPrec := Lean.reprImportArtifacts✝ }

instance Lean.instInhabitedImportArtifacts : Inhabited ImportArtifacts

Equations

• Lean.instInhabitedImportArtifacts = { default := { oleanParts := default } }

instance Lean.instToJsonImportArtifacts : ToJson ImportArtifacts

Equations

• Lean.instToJsonImportArtifacts = { toJson := fun (x : Lean.ImportArtifacts) => Lean.toJson x.oleanParts }

instance Lean.instFromJsonImportArtifacts : FromJson ImportArtifacts

Equations

• Lean.instFromJsonImportArtifacts = { fromJson? := fun (x : Lean.Json) => Lean.ImportArtifacts.mk <$> Lean.fromJson? x }

def Lean.ImportArtifacts.olean? (arts : ImportArtifacts) : Option System.FilePath

Equations

• arts.olean? = arts.oleanParts[0]?

def Lean.ImportArtifacts.oleanServer? (arts : ImportArtifacts) : Option System.FilePath

Equations

• arts.oleanServer? = arts.oleanParts[1]?

def Lean.ImportArtifacts.oleanPrivate? (arts : ImportArtifacts) : Option System.FilePath

Equations

• arts.oleanPrivate? = arts.oleanParts[2]?

structure Lean.ModuleArtifacts : Type

Files containing data for a single module.

• lean? : Option System.FilePath
• olean? : Option System.FilePath
• oleanServer? : Option System.FilePath
• oleanPrivate? : Option System.FilePath
• ilean? : Option System.FilePath
• ir? : Option System.FilePath
• c? : Option System.FilePath
• bc? : Option System.FilePath

instance Lean.instReprModuleArtifacts : Repr ModuleArtifacts

Equations

• Lean.instReprModuleArtifacts = { reprPrec := Lean.reprModuleArtifacts✝ }

instance Lean.instInhabitedModuleArtifacts : Inhabited ModuleArtifacts

Equations

• One or more equations did not get rendered due to their size.

instance Lean.instToJsonModuleArtifacts : ToJson ModuleArtifacts

Equations

• Lean.instToJsonModuleArtifacts = { toJson := Lean.toJsonModuleArtifacts✝ }

instance Lean.instFromJsonModuleArtifacts : FromJson ModuleArtifacts

Equations

• Lean.instFromJsonModuleArtifacts = { fromJson? := Lean.fromJsonModuleArtifacts✝ }

def Lean.ModuleArtifacts.oleanParts (arts : ModuleArtifacts) : Array System.FilePath

Equations

• One or more equations did not get rendered due to their size.

structure Lean.ModuleSetup : Type

A module's setup information as described by a JSON file.

• name : Name

  Name of the module.

• isModule : Bool

  Whether the module, by default, participates in the module system. Even if false, a module can still choose to participate by using module in its header.

• imports? : Option (Array Import)

  The module's direct imports. If none, uses the imports from the module header.

• importArts : NameMap ImportArtifacts

  Pre-resolved artifacts of transitively imported modules.

• dynlibs : Array System.FilePath

  Dynamic libraries to load with the module.

• plugins : Array System.FilePath

  Plugins to initialize with the module.

• options : LeanOptions

  Additional options for the module.

instance Lean.instReprModuleSetup : Repr ModuleSetup

Equations

• Lean.instReprModuleSetup = { reprPrec := Lean.reprModuleSetup✝ }

instance Lean.instInhabitedModuleSetup : Inhabited ModuleSetup

Equations

• One or more equations did not get rendered due to their size.

instance Lean.instToJsonModuleSetup : ToJson ModuleSetup

Equations

• Lean.instToJsonModuleSetup = { toJson := Lean.toJsonModuleSetup✝ }

instance Lean.instFromJsonModuleSetup : FromJson ModuleSetup

Equations

• Lean.instFromJsonModuleSetup = { fromJson? := Lean.fromJsonModuleSetup✝ }

def Lean.ModuleSetup.load (path : System.FilePath) : IO ModuleSetup

Load a ModuleSetup from a JSON file.

Equations

• One or more equations did not get rendered due to their size.