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

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

source
instance Lake.InputFileConfig.text.instConfigField {name : Lean.Name} :
ConfigField (InputFileConfig name) `text Bool
Equations

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

source
instance Lake.InputFileConfig.instConfigFields {name : Lean.Name} :
ConfigFields (InputFileConfig name)
Equations

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

source
instance Lake.InputFileConfig.path.instConfigField {name : Lean.Name} :
ConfigField (InputFileConfig name) `path System.FilePath
Equations

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

source
instance Lake.InputFileConfig.instConfigInfo :
ConfigInfo `Lake.InputFileConfig
Equations

- Lake.InputFileConfig.instConfigInfo = { fields := Lake.InputFileConfig._fields, arity := 1 }

source
instance Lake.InputFileConfig.instEmptyCollection {name : Lean.Name} :
EmptyCollection (InputFileConfig name)
Equations

- Lake.InputFileConfig.instEmptyCollection = { emptyCollection := { } }

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

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

source
instance Lake.InputDirConfig.filter.instConfigField {name : Lean.Name} :
ConfigField (InputDirConfig name) `filter PathPat
Equations

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

source
instance Lake.InputDirConfig.instEmptyCollection {name : Lean.Name} :
EmptyCollection (InputDirConfig name)
Equations

- Lake.InputDirConfig.instEmptyCollection = { emptyCollection := { } }

source
instance Lake.InputDirConfig.text.instConfigField {name : Lean.Name} :
ConfigField (InputDirConfig name) `text Bool
Equations

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

source
instance Lake.InputDirConfig.instConfigFields {name : Lean.Name} :
ConfigFields (InputDirConfig name)
Equations

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

source
instance Lake.InputDirConfig.instConfigInfo :
ConfigInfo `Lake.InputDirConfig
Equations

- Lake.InputDirConfig.instConfigInfo = { fields := Lake.InputDirConfig._fields, arity := 1 }

source
instance Lake.InputDirConfig.path.instConfigField {name : Lean.Name} :
ConfigField (InputDirConfig name) `path System.FilePath
Equations

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