Simple Builtin Facet Declarations #
This module contains the definitions of most of the builtin facets.
The others are defined Build.Info
. The facets there require configuration
definitions (e.g., Module
), and some of the facets here are used in said
definitions.
- path : Lake.FilePath
Library file path.
- name : String
Library name without platform-specific prefix/suffix (for
-l
).
A dynamic/shared library for linking.
Instances For
Optional library directory (for -L
).
Instances For
Module Facets #
- name : Lake.Name
The name of the module facet.
- data_eq : Lake.ModuleData s.name = α
Proof that module's facet build result is of type α.
A module facet name along with proof of its data type.
Instances For
The facet which builds all of a module's dependencies
(i.e., transitive local imports and --load-dynlib
shared libraries).
Returns the list of shared libraries to load along with their search path.
Instances For
The C file built from the Lean file via lean
.
Instances For
Package Facets #
A package's cloud build release.
Instances For
A package's extraDepTargets
mixed with its transitive dependencies'.
Instances For
Target Facets #
A Lean library's static artifact.
Instances For
A Lean library's extraDepTargets
mixed with its package's.
Instances For
A Lean binary executable.
Instances For
A external library's static binary.
Instances For
A external library's dynlib.