Quickstart: The Module System #

The module system provides a means of controlling how information may flow between modules.

Within modules, we can decide if information is public, and is thus seen by downstream modules, or if it is private, meaning that downstream modules are freed from the burden of loading this information.

Similarly, when importing information between modules, we can control whether a module's imports will be picked up transitively by downstream imports via public import.

This provides various benefits:

• Cheaper builds: by refusing to load the private data of upstream modules (which would include e.g. large theorem proofs), and by pruning long chains of unnecessarily transitive imports, we can load less data when building each module, saving on memory and other resources.

• Faster rebuilds: changes made exclusively to a module's private data do not trigger rebuilds of downstream modules which import that module, since downstream modules only depend on public data, allowing us to reuse previous builds.

• API control: making certain data private allows us to insist that downstream users use the API we want, and do not rely on "accidental" facts of the implementation. Likewise, we do not need to force internal import dependencies on downstream files if we only use them privately.

The module system also has us manage what code is available to execute at compile time through the meta keyword. This affects syntax, macros, tactics, elaborators, attributes, and other compile-time affordances. Most code is not meta, and the guarantee that it will not be needed while compiling a file allows us to avoid costs associated with producing and loading the code.

A file is a "module file", i.e. participating in the module system, if and only if it has the module keyword at the top. Non-module files are allowed to import module files, but at the cost of loading both public and private information and following even non-public imports transitively, eliminating the benefits of the module system from that point forward. Module files cannot import non-module files.

Visibility #

Each module has a public scope and a private scope.

The information in the private scope can use any information from the public scope, but the reverse is not true. We use an arrow to show information flowing from one scope to another.

import A puts the public scope of A into the private scope of the current module.

public import A puts the public scope of A into the public scope of the current module.

Note that both of these imports only access the public scope of A.

Module B receiving A's public scope in its own public scope means that downstream imports of B (public or not) will also necessarily receive the public scope of A along with the public scope of B.

Information flows through the arrows in these diagrams transitively, meaning we can chain arrows together to infer new, composite arrows. In other words, the arrows in these diagrams may be composed.

As such, chains of public imports form transitive chains of dependencies.

But what if B does not want to provide A to its importers? A non-public import "breaks the chain". Observe that C loads no data at all from A, regardless of whether it uses import B or public import B. This is how B is able to use data from A privately without forcing it on downstream consumers such as C.

This also enables us to skip rebuilding C when editing A. Since the resulting public scope of B will not be changed by any changes to A, the build of C will consider C's dependencies to be up-to-date, and will thus skip building C and reuse the previous build results.

It is therefore generally good practice to make imports non-public if possible, and to only use public import where necessary or to deliberately provide access to API.

Both public import A and import A provide only A's public scope, but what if you do need something from A's private scope? As an escape hatch, import all A will request the private scope of A and put it in the target module's private scope.

Because arrows in the following diagram can be followed transitively, the public scope of A is also available in B's private scope.

import all should be avoided if at all possible; the need for an imported module's private scope is generally a sign that either something is being done wrong in the current module, or that the public scope of the upstream module should be redesigned.

Note that public import all is not allowed. The private scope of a module cannot ever be lifted into the public scope through imports.

public import A and import all A (on separate lines) will import the public scope into the public scope and the private scope into the private scope.

In the diagram below, gray arrows show the implicit connections produced by following the black arrows transitively.

Declarations #

An ordinary constant has several pieces of data associated with it:

• name : Name
• type : Expr
• (optional) value : Expr
• (optional) code : IR

In some sense "the constant" is simply its name. Its type, value, and so on are merely data associated with the constant.

Each constant has a visibility, i.e. which scope it is in (public or private).

The associated pieces of data may have different individual visibilities, and so may behave differently under imports. For example, if the constant is public but some data associated with it is private (say, its value), an import of the constant's module will only request the public data for the constant, thus completely forfeiting access to that private data.

Further, we may speak of working "at" a given visibility at different points in a module. This specifies which information we have available in the situation at hand (either just the public scope's information or both the public and private scopes' information).

Note: be aware that the notion of some information being "in scope" is not generally well-formed, as whether something is "in scope" will change depending on whatever our current working visibility is.

While a constant's current visibility depends on how it is imported (publicly or privately), it also has an intrinsic visibility, namely which scope of its originating module it lives in. A constant may be made intrinsically public by using the public keyword (either on the declaration itself, e.g. public def, or via public section).

Otherwise, declarations are private by default, which encourages being deliberate about designing the public scope. (The private keyword is only useful in negating an enclosing public section.)

Different pieces of data associated with the constant behave differently with respect to visibility. (Note: we will defer the discussion of code visibility to a later section.)

name: The intrinsic visibility is apparent in the name, since private constants are subject to mangling, and their name will have an autogenerated prefix like _private.Foo.Bar.0.myFoo, where Foo.Bar is the original module of a private def myFoo. Though the current visibility may be reduced from the intrinsic visibility depending on how the constant is imported, the name of a constant is immutable, and never changes no matter where or how it is imported.

type: The type of a constant always has the same visibility as the constant itself.

value: The value of a constant cannot have a greater visibility than the constant itself (it makes no sense to have a public value for a private constant, for example), but it may have a lower visibility. In particular, the type of a constant may be public while the value is private.

In fact, having a private value is the default situation for a public def, and the only situation for a public theorem. Note that the value of a theorem is just its proof, and theorem proofs are always private, since proof irrelevance means they will never be useful downstream (and so there is no reason to make downstream importers load them).

Recall that ordinary imports (i.e. import or public import, without import all) only import the public scope. As such, when importing a public constant with a private value, the value data will simply not be loaded downstream, and thus will be completely inaccessible.

@[expose] #

However, public definitions may, if we so choose, have public values as well. We may raise the intrinsic visibility of a public definition's value to public by attaching @[expose] to the definition. @[expose] is meaningless on a private constant, and Lean will reject it.

The main utility for having a value available is that it effectively provides Lean with a rewrite rule that lets us unfold the constant to that value during definitional equality checks. E.g., if Lean knows the value of foo to be given by foo := 37, then Lean may unfold foo in order to unify foo + 1 with 37 + 1.

Whether this unfolding is possible even in principle depends on whether the value data is available at the working visibility of the definitional equality check. As an example, if the value data is present but is private (i.e. no @[expose]), then Lean could unify foo + 1 with 37 + 1 within a public theorem's proof (a private location, where it can access private data) but not its type (a public location).

Note how, for a non-@[expose]d constant, this yields a significant difference between working in the module it was defined in and working in downstream modules. In the module in which a public non-@[expose]d constant is defined, the value data is present, but private. Even though it can't be used in public positions, we can still unfold the definition when proving public API theorems (since theorem proofs are private).

However, (ordinary) downstream modules never import the private scope, meaning that they cannot unfold the constant at any point, even in principle. The data is simply not there.

(The one exception is if the downstream modules use the discouraged import all, which would give them exactly that private data; note, even then, we would still only be able to unfold when working at the private visibility, since import all does not lift private data to the public scope.)

As such, @[expose] is required for being able to unfold constants downstream.

Note that abbrevs and instances are definitions which are @[expose]d by default.

It is worth noting that Lean further restricts the unfolding of constants via their transparency settings, e.g. @[reducible], @[implicit_reducible], and so on. Transparency settings are subordinate to the module system; thus they are only meaningful when unfolding is already possible. In the typical case, this means they only matter on @[expose]d definitions or else when working at private visibilities in the same file.

Technical note: typechecking down in the kernel always behaves as if it is at the private visibility. However, it still cannot unfold declarations whose values are not imported, as that data is not present.

To recap, the visibility of a constant's value depends on the kind of declaration creating it:

• def: the value is private by default, but can be made public via @[expose] (only) when the constant is also public.
• theorem: the value is its proof, and is always private.
• abbrev, instance: if public, the value is public by default (i.e., these commands attach @[expose]). Note: if Lean notices that a given instance has a Prop type, it will become a theorem with a private value behind the scenes.

Note that while @[expose] and public may be attached directly to the declaration, they may also be attached to section (e.g. @[expose] public section), which simply applies the modifiers to every declaration in the section. Within such sections these modifiers may also be individually negated with @[no_expose] and private.

Phase (meta vs. runtime) #

The meta keyword controls what happens to executable code associated with constants. Specifically, a constant's executable code may be either

1. available for execution during the elaboration of the current module, in which case we call it meta code...
2. ...or not, in which case we call it runtime code.

This state ("meta" or "runtime") is called the phase of the code.

Meta code cannot be referenced from runtime code, and vice versa. Code is only allowed to reference code that has the same phase.

Analogously to visibility, a constant's code has an intrinsic phase determined when the constant is created, and a current phase downstream determined by how it is imported.

By default, a constant's code is intrinsically runtime, unless it is a meta def. Many meta-related commands like syntax, macro, and elab necessarily produce meta defs behind the scenes without manual intervention, since their code must be executable during elaboration.

An ordinary, non-meta import preserves the phases of all code. Code which is already meta will remain meta and executable. Tactics and macros, for example, may be obtained and used by downstream modules via ordinary non-meta imports.

(In these diagrams, we use "IR" interchangeably with "code".)

meta import A lifts all of the runtime code reachable from A to the meta phase. That is, intrinsically runtime code from A is now in the meta phase in the importing module, and so we can use it in any meta code we write in our current module. Meta code from A is still imported under meta import, and stays meta.

(Arrow coloration only shows, redundantly, where the arrows end, to emphasize that runtime IR becomes available in the meta phase under meta imports.)

In fact, having now seen both sorts of imports, we find that a meta modifier on an import only changes whether or not runtime IR is lifted to the meta phase, and does nothing else. Perhaps counterintuitively, its presence or absence does not change what happens to meta code from the imported module.

public meta import A behaves like a public import with the same runtime-to-meta phase lifting behavior as a meta import, but, due to how public imports chain transitively, will also provide that meta-lifted runtime code to downstream modules which import the current module. (We'll visualize this with a refined version of the diagram above.)

The phase of an import only affects the phase of any code that is imported. From a type-theoretic point of view, meta import modifiers do not change which constants are imported or at what visibility (the latter of which is still determined by public). So, a public meta import also functions as a public import for type-theoretic purposes.

Constants #

As has been suggested, constants in Lean, separately from their role as terms in a type theory, are also compiled into code (Lean IR). This code may then be compiled further to C code and then to machine code that runs natively. Or, instead, Lean IR may be executed directly by the Lean interpreter.

It is the interpreter that drives elaboration by executing parsers, elaborators, tactics, and so on. Whenever a constant appears in some piece of code the interpreter is executing, the interpreter must look up the code associated with the constant (preferring native machine code if available), and then execute the code it finds. If it cannot find the code, it errors.

Meta code is exactly code which the interpreter is able to successfully locate while elaborating a Lean file.

Since the phase of code specifies when that code must be available, the phase also determines where that code is stored behind the scenes (in order to be accessible downstream) and puts constraints on the phases of that code's references and how they are imported.

Specifically, the laws and constraints around the meta phase must ensure that any constant referenced by meta code will also, in turn, have locatable code, so that the interpreter never errors. I.e., Lean ensures that meta code only ever references meta code. Further, this must remain true downstream, so (as we will see in more detail) any references must be propagated to importers through transitive chains of imports.

Phase only pertains to executable code, and the meta keyword does not affect any aspects of a constant besides its code.

Note that the phases of constants used in proofs and types are ignored. This is because proofs and types are erased during compilation, and as such do not actually appear in the final executable code. Only dependencies which affect computation are checked for phase correctness.

Not all constants have code; theorems produce no code, and noncomputable defs are permitted to not produce code. (Note: perhaps surprisingly, Lean does still attempt to compile noncomputable defs, and just silences failures.) As such, the phases of constants used by a theorem in both its type and its proof are ignored, and it may use both meta and runtime constants.

Since it would have no effect, Lean rejects the meta keyword on theorems and other declarations that do not produce executable code. (Technical note: certain "code-like" declarations still accept meta, such as structure, even though they do not have code.)

meta visibility constraints #

By and large, runtime code does not interact with the source constant's visibility. In contrast, any constant with intrinsically meta code has a complicated relationship to visibility which is different from that of runtime code.

Recall that a constant has a name (the constant itself), code (if computable), and a type-theoretic type and value. The code is produced by compiling the value, which turns a term of the type theory into Lean IR.

Despite this relationship between the value and code, the visibility rules surrounding a constant's meta code do not behave similarly to those surrounding the value it was compiled from.

Instead, the code of a public meta def should be thought of as somehow "public" itself. This is because the code of a public meta def requires all of its transitive dependencies to both be in the meta phase and come from publicly-imported modules. This is how we ensure the interpreter is always able to find any referenced constant's code in the future, since the public import will preserve the availability of the referenced code downstream.

(Recall that, in contrast, whether the actual value is public is controlled by @[expose], which has no effect on code whatsoever, meta or runtime. Code (both meta and runtime) also has an @[expose]-like notion to enable @[inline] and similar compilation features that rely on the availability of the code downstream, but this is a little-seen technical detail whose behavior is subject to change in the future, and we do not cover it here.)

Perhaps surprisingly (given our experience with visibility), a public meta def is allowed to use private meta defs from the same module—as long as those defs, in turn, only have dependencies which are meta and come from publicly-imported modules.

This leads to situations such as

module

meta import Bar -- privately meta imports `bar`

-- Succeeds
meta def foo := bar

-- Fails, due to `bar` in `foo` not being publicly imported
public meta def fooPublic := foo

The above example succeeds if we instead publicly import bar via public meta import Bar.

As such, framing the code produced by public meta defs as "public" doesn't quite work. Instead, we can conceptualize it this way: rather than saying that meta code is "public" or "private", we use the similar terms "presentable", meaning valid to use downstream, or "unpresentable".

However, rather than always being declared like public or private is, the presentability of code is inferred on the basis of what the code references. By definition, we say that presentable code may only reference presentable code.

We also say that presentability is only a meaningful property of meta code. We consider all runtime code to just be runtime code.

A private meta def's associated code may be presentable or unpresentable. However, a public meta def's code is required to be presentable. If a public meta def uses an unpresentable meta def, the compilation of that public meta def will error, and the error message will point to the private import which must be upgraded to public or public meta to make the code presentable.

We now refine our above diagram into the following final form so that we can visualize presentabilities.

Presentable code may be referenced by unpresentable code, but not vice versa.

Note that there is no arrow either way between runtime IR and meta IR in the same module, since neither may use the other, as per the runtime/meta phase separation. Phase can only be changed at import boundaries (and only to lift runtime IR to meta IR).

(Technical note: to allow public meta defs to use private meta defs, the code from private meta defs is stored in the public *.olean behind the scenes, and their names are recorded in a special public location relevant only to the compiler and interpreter. Their types and values remain private as expected.)

Import visibility modifiers affect presentability analogously to the way they affect scopes: public (meta) import A imports all of the presentable code from A as presentable code in the target module; a (meta) import imports all of the presentable code from A as unpresentable.

Note: like visibility, if the same code is provided transitively in different ways from different imports, it has the maximum presentability among all different ways it is provided. For example, if foo is imported as unpresentable code due to import A' and as presentable code due to public import A'', it is presentable.

If code is imported both as runtime code and as meta code, it is available for use in both phases.

In the following diagrams, the arrows mean "(transitively) referenceable in".

As before, these arrows may be composed, and we show composite arrows in a lighter shade.

Observe that (public) meta import A lifts the runtime code from A (and its dependencies) to the meta phase, making it presentable or unpresentable depending on whether public is or isn't present, respectively. This is what we expect given our earlier discussion of meta imports.

However, even though runtime IR can be raised to the meta phase, importing can never lower meta IR down to runtime IR. Code in the meta phase is stuck there forever.

We also see that code which is already intrinsically meta (i.e. marked meta in the source file) is indeed still brought in as meta code under ordinary imports, and is unaffected by the presence of meta on the import.

We can now see that public meta imports indeed propagate the ability to interpret lifted runtime IR under non-meta downstream imports. This is why, if B in the diagram below defined tactics which used runtime code from A, it may be imported normally by C without breaking anything.

However, meta imports break the chain, and runtime IR from A privately meta imported by B is not loaded as meta IR in C.