Understanding `meta import`

Stream: lean4 dev

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hello! I am trying to understand the new meta phase introduced in lean4#8660. For reference, two constraints are delineated there:

1. meta declarations may use any local declaration, imported meta declarations, and any meta imported declarations.
2. non-meta declarations may use a non-meta declaration reachable only through non-meta imports.

meta is a marker that can be put on global constants in an environment (as opposed to e.g. a part of the type system for finer-grained specifications like T meta → T). It behaves like so:

• in their own module, constants are meta iff defined via meta def
• in downstream modules
  • meta imported constants are always meta
  • imported constants are meta iff they were meta in the module we're importing from (in particular if that module in turn used meta import, explaining why 'meta import is transitive')

(If a constant is both imported and meta imported, let's think of it as secretly two constants in the environment.)

Since meta will be used to avoid importing IR that is not needed at compile-time, let's define another marker has_ir that we put on those constants for which the IR is available (in a given environment). This behaves like so:

• in their own module, all constants are has_ir
• in downstream modules, constants are has_ir iff they are meta

We have the restriction that meta defs may only use has_ir constants. This explains constraint 1.

However, constraint 2 is not explained: there is no obstacle to using a has_ir constant in a non-meta declaration; indeed, it must be possible to do that. From past discussions, I am guessing there is a further meaning to meta along the (somewhat circular) lines of 'exclude this code when compiling an object-level/non-meta executable'. Let's have another marker, non_obj, for that. This exactly coincides with meta:

• in its own module, a constant is non_obj iff it's a meta def (?)
• in downstream modules, constants are non_obj iff they are meta

Overall, we have meta == non_obj and meta => has_ir (for upstream constants meta == has_ir).

There is now a restriction that if a declaration uses a non_obj constant, that declaration must itself be non_obj. This explains constraint 2.

It also seems to imply constraint 3: non-meta declarations may not use meta declarations in their values (of course tactics and so on can be used to produce the values).

Now I have a few questions:

• Is this analysis accurate? In particular, will constraint 3 materialize?
• If so, and I did want to include an upstream meta constant in object code, can I "un-meta" it? (I can't just do import and meta import if the thing was originally a meta def.)
• If I want to #eval an upstream constant, or do anything else with its IR, do I have to meta import it?
• How will precompilation of tactics fit into this picture? Will every module have two compilation targets, one for object-level code and one for no_obj code?

[Sebastian Ullrich]

Hey Wojciech, thanks for thinking through this :) . I do appreciate feedback.

exclude this code when compiling an object-level/non-meta executable

Right, this goal was not mentioned in the PR.

In particular, will constraint 3 materialize?

Ah, it already is there: https://github.com/leanprover/lean4/pull/8660/files#diff-d8e303a116f08503ab6b9ca0ce6a643d96c94e3dbf9f96cf239589385786c9c9R137. This follows from constraints 1 and 2 if you see them as exhaustive, but I see how that may have been unclear.

If so, and I did want to include an upstream meta constant in object code, can I "un-meta" it?

You can't. At that point we assume you are working against the intent of the code's author, so you should really work that out with them.

If I want to #eval an upstream constant, or do anything else with its IR, do I have to meta import it?

#eval is special cased in the language server, but it will in fact break on the cmdline without meta (you're not using it there anyway, right?)

How will precompilation of tactics fit into this picture? Will every module have two compilation targets, one for object-level code and one for no_obj code?

Likely, yeah. The current approach shouldn't break since it just includes everything but that would be a future refinement.

[Alex Keizer]

#eval is special cased in the language server, but it will in fact break on the cmdline without meta (you're not using it there anyway, right?)

We sometimes use #guard_msgs in #eval ... for compile-time tests, would those break a lake build in this new system?

[Sebastian Ullrich]

Use the correct meta imports then, or don't make that test a module :)

[Thomas Murrills]

Hopefully this is a good place for more basic questions too! :) I'm wondering simply how meta import Foo behaves. Does it essentially mark all declarations coming from Foo with meta? (If so, transitively, or not?)

If so, is the intended design pattern for e.g. files defining tactics to just mark everything as meta def, or to use typical defs but only ever meta import the file? (Or neither?)

[Thomas Murrills]

Also, are there any prior discussions on this (or documentation, yet) for better familiarizing myself with the idea behind it?