Understanding Lake facets, targets, and friends

Stream: lean4

[Thomas Murrills]

I'm attempting to understand the conceptual framework of lake's build system, and while I've understood some things, I still don't get some foundational things, like "what a facet really is".

I'm hoping that by (1) linking to what I have already found helpful here and (2) airing my confusions, people will be able to find a resource on zulip if they have similar questions—and, if my confusions aren't too idiosyncratic, maybe this discussion could help with documentation more generally. :)

Resources

The place to start is of course the language reference page for Lake, which is a great help already.

I'll also link here the docgen4 lakefile, which constitutes a worked example of custom targets and package_, module_, and library_facets.

There's also some insight in this Zulip thread from Mac Malone, who is responsible for Lake (though from 2023; have things changed?). There's some oblique info in this thread on some limitations of module_facet (2024; still relevant?) and another small worked example for sqlite bindings on zulip here.

There are also some tiny but useful examples in the example file for lake in the lean4 repo.

Questions

There's one main question I have, then one smaller question.

1. What's the difference between a facet and a target? (What is each?) Likewise, what's the relationship between modules/packages/libraries and facets/targets?

Here are the clues I have so far (each of which is an excerpt from the reference manual).

A target represents an output that can be requested by a user. A persistent build output, such as object code, an executable binary, or an .olean file, is called an artifact. In the process of producing an artifact, Lake may need to produce further artifacts; for example, compiling a Lean program into an executable requires that it and its dependencies be compiled to object files, which are themselves produced from C source files, which result from elaborating Lean sourcefiles and producing .olean files. Each link in this chain is a target, and Lake arranges for each to be built in turn.

Custom targets contain arbitrary code to run a build, written using Lake's internal API.

... Lake proceeds to build each artifact. This involves running the appropriate build tool on the input files and saving the artifact and its trace file, as specified in the corresponding facet. (emph mine)

A facet describes the production of a target from another. Conceptually, any target may have facets. However, executables, external libraries, and custom targets provide only a single implicit facet. Packages, libraries, and modules have multiple facets that can be requested by name when invoking lake build to select the corresponding target.

When no facet is explicitly requested, but an initial target is designated, lake build produces the initial target's default facet. Each type of initial target has a corresponding default facet (e.g. producing an executable binary from an executable target or building a package's default targets)

lake build [targets...]

Builds the specified facts of the specified targets.

Each of the targets is specified by a string of the form:

[[@]package[/]][target|[+]module][:facet]

The optional @ and + markers can be used to disambiguate packages and modules from file paths as well as executables, and libraries, which are specified by name as target. [...] Module targets may also be specified by their filename, with an optional facet after a colon.

The available facets depend on whether a package, library, executable, or module is to be built. They are listed in the section on facets.

a – The default facet(s) of target a

@a – The default targets of package a

+A – The Lean artifacts of module A (because the default facet of modules is leanArts)

@a/b – The default facet of target b of package a

... packages depend on other packages, while build targets depend on other build targets, which may be in the same package or in a different one. One facet of a given target may depend on other facets of the same target.

Package facets allow the production of an artifact or set of artifacts from a whole package. The Lake API makes it possible to query a package for its libraries; thus, one common use for a package facet is to build a given facet of each library.

(Aside: in these callouts in the manual, "Library facets" and "Module facets" at the start of the respective bubbles are both typoed as "Package facets".)

Confusions and subquestions:

• Modules, libraries, and packages have facets; targets also have facets. Are modules, libraries, and packages targets, or do they have targets? Packages and libraries are indeed called "initial targets" at some point in the manual. However, packages can also have targets (and target defines targets "for the package"), suggesting packages are not necessarily targets per se—or not just targets. Likewise, I wouldn't think of packages, libraries, and modules as meeting the definition of target and "representing a kind of output" in and of themselves (if anything, they're sources, the "opposite" of a target!).
• A target seems to in part be a way of producing artifacts; after all, it contains code for a job. But so do facets; in fact, according to some language, apparently facets are the things that specify how to produce artifacts. Why are they separate things? Do all targets only produce artifacts "via" a facet? The language used seems to suggest so at times, but in e.g. the docgen source, the targets seem self-contained.
• Likewise, targets can already depend on other targets. So why do we need facets to do the same? What is the motivation behind having facets in the first place? Is it simply to enable a different command line interface, or does it give us a conceptually different sort of thing?
• "Each type of initial target has a corresponding default facet". Is the initial part conceptually crucial here? Do non-initial targets not necessarily have default facets? Why?
• We can add facets to packages, libraries, and modules via the respective commands. The language seems to suggest we could add them to (other?) targets, too. But these don't seem to be "blessed" in the same way. Is this just a measure of (in)convenience? Or are the abstractions of package/library/module woven more deeply into the conceptual framework of lake in a way that changes how we should understand their relationship to facets/targets? (Obviously they are woven deeply into lake in general, but I'm trying to figure out if the very concept of targets and facets depends on them in some way.)

I don't expect every question to be answered individually here; but hopefully this is enough to make clear where I'm confused! Sometimes it feels like there are unspoken assumptions about what these systems should look like or be capable of that I'm not privy to, so I'm trying to make it obvious which assumptions I don't share—I suspect that there is some relatively simple presentation which would make answering all of these questions trivial!

2. What's the intended utility of the return type of a facet or target?

I'm guessing the answer here is "it allows facets/targets to provide data to other facets/targets which may call it, such that the calling facet/target can use that data to access the called facet/target's built artifacts/computed metadata/etc.". But is this right? If so, is this the full extent of what that data is for?

---

If you read this far, thanks. :)

[Eric Wieser]

You mind find reading the lakefile of doc-gen helpful; I certainly can't claim whether it's idiomatic, but it is making heavier-than-usual usage of lake facets

[Thomas Murrills]

Indeed—that is already linked above! :)

[Mac Malone]

Some quick clarifications for now:

• Package, libraries, and modules are all targets (and, more specifically, initial targets). A target is anything one can request from Lake, e.g., via lake build, lake query, or a fetch in the Lake API. While it is true that packages, libraries, and modules are not ouputs per se, requesting them does produce an output (their default targets / facet(s)).
• A facet is essentially a function between targets. It produces a target from another. For example, the module c facet (i.e., +mod:c) produces the module's C target from a module target. Initial targets are those not produced by facet. Instead, they are specified by a Lake configuration file. Initial targets have a default facet to determine which of their possible outputs Lake should produce when they are requested.

We can add facets to packages, libraries, and modules via the respective commands. The language seems to suggest we could add them to (other?) targets, too.

Yes! The API theoretically supports this. However, this is currently unimplemented due to a lack of use cases.