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.

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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