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.
Module Facets #
Equations
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.
Equations
Instances For
The C file built from the Lean file via lean
.
Equations
Instances For
The LLVM BC file built from the Lean file via lean
.
Equations
Instances For
The object file .c.o
built from c
.
On Windows, this is c.o.noexport
, on other systems it is c.o.export
).
Equations
Instances For
Package Facets #
A package's optional cached build archive (e.g., from Reservoir or GitHub). Will NOT cause the whole build to fail if the archive cannot be fetched.
Equations
Instances For
A package's cached build archive (e.g., from Reservoir or GitHub). Will cause the whole build to fail if the archive cannot be fetched.
Equations
Instances For
A package's optional build archive from Reservoir. Will NOT cause the whole build to fail if the barrel cannot be fetched.
Equations
Instances For
A package's Reservoir build archive from Reservoir. Will cause the whole build to fail if the barrel cannot be fetched.
Equations
Instances For
A package's optional build archive from a GitHub release. Will NOT cause the whole build to fail if the release cannot be fetched.
Equations
Instances For
A package's build archive from a GitHub release. Will cause the whole build to fail if the release cannot be fetched.
Equations
Instances For
A package's extraDepTargets
mixed with its transitive dependencies'.
Equations
Instances For
Target Facets #
The library's default facets (as specified by its defaultFacets
configuration). .
Equations
Instances For
A Lean library's static artifact.
Equations
Instances For
A Lean library's static artifact (with exported symbols).
Static libraries with explicit exports are built as thin libraries. Such libraries are usually used as part of the local build process of some shared artifact and not publicly distributed. Standard static libraries are much better for distribution.
Equations
Instances For
A Lean library's extraDepTargets
mixed with its package's.
Equations
Instances For
A Lean binary executable.
Equations
Instances For
A external library's static binary.
Equations
Instances For
A external library's dynlib.
Equations
Instances For
The default facet for an input file. Produces the file path.
Equations
Instances For
The default facet for an input directory. Produces the matching files in the directory.