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.

instance Lake.InputFileConfig.instConfigMeta : ConfigInfo `Lake.InputFileConfig

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

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

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

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

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

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

instance Lake.InputDirConfig.instConfigMeta : ConfigInfo `Lake.InputDirConfig

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

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

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

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