Documentation

Lake.Config.InputFileConfig

structure Lake.InputFileConfig (name : Lean.Name) :

The declarative configuration for a single input file.

path : System.FilePath
The path to the input file (relative to the package root).
Defaults to the name of the target.
text : Bool
Whether this is a text file. If so, Lake normalize line endings for its trace. This avoids rebuilds across platforms with different line endings.
Defaults to false.

Instances For

instance Lake.InputFileConfig.instConfigMeta :

ConfigInfo `Lake.InputFileConfig

Equations

Lake.InputFileConfig.instConfigMeta = { fields := Lake.InputFileConfig._fields }

instance Lake.InputFileConfig.path.instConfigField {name : Lean.Name} :

ConfigField (InputFileConfig name) `path System.FilePath

Equations

Lake.InputFileConfig.path.instConfigField = { toConfigProj := Lake.InputFileConfig.path._proj }

instance Lake.InputFileConfig.text.instConfigField {name : Lean.Name} :

ConfigField (InputFileConfig name) `text Bool

Equations

Lake.InputFileConfig.text.instConfigField = { toConfigProj := Lake.InputFileConfig.text._proj }

instance Lake.InputFileConfig.instConfigFields {name : Lean.Name} :

ConfigFields (InputFileConfig name)

Equations

Lake.InputFileConfig.instConfigFields = { fields := Lake.InputFileConfig._fields }

instance Lake.instEmptyCollectionInputFileConfig {name : Lean.Name} :

EmptyCollection (InputFileConfig name)

Equations

Lake.instEmptyCollectionInputFileConfig = { emptyCollection := { } }

structure Lake.InputDirConfig (name : Lean.Name) :

The declarative configuration for an input directory.

path : System.FilePath
The path to the input directory (relative to the package root).
Defaults to the name of the target.
text : Bool
Whether the directory is composed of text files. If so, Lake normalize line endings for their traces. This avoids rebuilds across platforms with different line endings.
Defaults to false.
filter : PathPat

Instances For

instance Lake.InputDirConfig.filter.instConfigField {name : Lean.Name} :

ConfigField (InputDirConfig name) `filter PathPat

Equations

Lake.InputDirConfig.filter.instConfigField = { toConfigProj := Lake.InputDirConfig.filter._proj }

instance Lake.InputDirConfig.instConfigMeta :

ConfigInfo `Lake.InputDirConfig

Equations

Lake.InputDirConfig.instConfigMeta = { fields := Lake.InputDirConfig._fields }

instance Lake.InputDirConfig.path.instConfigField {name : Lean.Name} :

ConfigField (InputDirConfig name) `path System.FilePath

Equations

Lake.InputDirConfig.path.instConfigField = { toConfigProj := Lake.InputDirConfig.path._proj }

instance Lake.InputDirConfig.text.instConfigField {name : Lean.Name} :

ConfigField (InputDirConfig name) `text Bool

Equations

Lake.InputDirConfig.text.instConfigField = { toConfigProj := Lake.InputDirConfig.text._proj }

instance Lake.InputDirConfig.instConfigFields {name : Lean.Name} :

ConfigFields (InputDirConfig name)

Equations

Lake.InputDirConfig.instConfigFields = { fields := Lake.InputDirConfig._fields }

instance Lake.instEmptyCollectionInputDirConfig {name : Lean.Name} :

EmptyCollection (InputDirConfig name)

Equations

Lake.instEmptyCollectionInputDirConfig = { emptyCollection := { } }