Documentation

Lake.Build.Facets

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.

structure Lake.Dynlib :

A dynamic/shared library for linking.

  • Library file path.

  • name : String

    Library name without platform-specific prefix/suffix (for -l).

Optional library directory (for -L).

Equations
  • self.dir? = self.path.parent

Module Facets #

structure Lake.ModuleFacet (α : Type) :

A module facet name along with proof of its data type.

  • name : Lean.Name

    The name of the module facet.

  • data_eq : Lake.ModuleData self.name = α

    Proof that module's facet build result is of type α.

Instances For
instance Lake.instReprModuleFacet {α✝ : Type} [Repr α✝] :
Equations
  • Lake.instReprModuleFacet = { reprPrec := Lake.reprModuleFacet✝ }
Equations
  • =
Equations
  • Lake.instCoeDepNameModuleFacetOfFamilyOutModuleData = { coe := { name := facet, data_eq := } }
@[reducible, inline]

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
@[reducible, inline]

The core build facet of a Lean file. Elaborates the Lean file via lean and produces all the Lean artifacts of the module (i.e., olean, ilean, c). Its trace just includes its dependencies.

Equations
@[reducible, inline]

The olean file produced by lean.

Equations
@[reducible, inline]

The ilean file produced by lean.

Equations
@[reducible, inline]

The C file built from the Lean file via lean.

Equations
@[reducible, inline]

The LLVM BC file built from the Lean file via lean.

Equations
@[reducible, inline]

The object file .c.o built from c. On Windows, this is c.o.noexport, on other systems it is c.o.export).

Equations
@[reducible, inline]

The object file .c.o.export built from c (with -DLEAN_EXPORTING).

Equations
@[reducible, inline]

The object file .c.o.noexport built from c (without -DLEAN_EXPORTING).

Equations
@[reducible, inline]

The object file .bc.o built from bc.

Equations
@[reducible, inline]

The object file built from c/bc. On Windows with the C backend, no Lean symbols are exported. On every other configuration, symbols are exported.

Equations
@[reducible, inline]

The object file built from c/bc (with Lean symbols exported).

Equations
@[reducible, inline]

The object file built from c/bc (without Lean symbols exported).

Equations

Package Facets #

@[reducible, inline]

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
@[reducible, inline]

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
@[reducible, inline]

A package's optional build archive from Reservoir. Will NOT cause the whole build to fail if the barrel cannot be fetched.

Equations
@[reducible, inline]

A package's Reservoir build archive from Reservoir. Will cause the whole build to fail if the barrel cannot be fetched.

Equations
@[reducible, inline]

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
@[reducible, inline]

A package's build archive from a GitHub release. Will cause the whole build to fail if the release cannot be fetched.

Equations
@[reducible, inline]

A package's extraDepTargets mixed with its transitive dependencies'.

Equations

Target Facets #

@[reducible, inline]

A Lean library's Lean artifacts (i.e., olean, ilean, c).

Equations
@[reducible, inline]

A Lean library's static artifact.

Equations
@[reducible, inline]

A Lean library's static artifact (with exported symbols).

Equations
@[reducible, inline]

A Lean library's shared artifact.

Equations
@[reducible, inline]

A Lean library's extraDepTargets mixed with its package's.

Equations
@[reducible, inline]

A Lean binary executable.

Equations
@[reducible, inline]

A external library's static binary.

Equations
@[reducible, inline]

A external library's shared binary.

Equations
@[reducible, inline]

A external library's dynlib.

Equations