feat: slightly extend meta phase section
#626
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Feedback welcome |
|
I don't think I broke that example |
|
#628 should fix the CI for the example here. A merge or rebase on |
| A `meta` definition may access (and thus invoke) any `meta` or non-`meta` definition of the current module. | ||
| For accessing imported definitions, the definition must either have been marked as `meta` when it was declared or the import must be marked as such (`meta import` when the accessing definition is in the private scope and `public meta import` otherwise). | ||
|
|
||
| A `meta` definition may access (and thus invoke) other `meta` definitions only; a non-`meta` definition likewise may only access other non-`meta` definitions. |
There was a problem hiding this comment.
Suggested change
| A `meta` definition may access (and thus invoke) other `meta` definitions only; a non-`meta` definition likewise may only access other non-`meta` definitions. | |
| A `meta` definition may only access (and thus invoke) other `meta` definitions; a non-`meta` definition likewise may only access other non-`meta` definitions. |
On a first read-through, the adverb came as a surprise
| A `meta` definition may access (and thus invoke) other `meta` definitions only; a non-`meta` definition likewise may only access other non-`meta` definitions. | ||
| For imported definitions, the `meta` marker can be added after the fact using `meta import`. | ||
| `meta import`ing a definition already in the meta phase leaves it in that phase. | ||
| In addition, the import must be public if the imported definition may be compile-time executed outside the current module, i.e. if it is reachable from some public `meta` definition in the current module: use `public meta import` or, if already `meta`, `public import`. |
There was a problem hiding this comment.
Suggested change
| In addition, the import must be public if the imported definition may be compile-time executed outside the current module, i.e. if it is reachable from some public `meta` definition in the current module: use `public meta import` or, if already `meta`, `public import`. | |
| In addition, the import must be public if the imported constant may be executed at compile time outside the current module. | |
| In other words, if the imported `meta` constant is reachable from some public `meta` definition in the current module, then use `public meta import`. | |
| If the constant is already `meta`, then `public import` is sufficient. |
There was a problem hiding this comment.
I usually prefer "declaration" over "constant" in user-facing text, is there some canonized stance on that?
| For imported definitions, the `meta` marker can be added after the fact using `meta import`. | ||
| `meta import`ing a definition already in the meta phase leaves it in that phase. | ||
| In addition, the import must be public if the imported definition may be compile-time executed outside the current module, i.e. if it is reachable from some public `meta` definition in the current module: use `public meta import` or, if already `meta`, `public import`. | ||
| This is usually the case, unless a definition was imported solely for use in `local` metaprograms. |
There was a problem hiding this comment.
Why is local annotated as code here?
| For convenience, `meta` also implies `partial`. | ||
| This can be overriden by giving an explicit `termination_by` metric (such as one suggested by `termination_by?`), which may be necessary when the type of the definition is not known to be `Nonempty`. | ||
|
|
||
| As a guideline, it is usually preferable to apply `meta` as late as possible. |
There was a problem hiding this comment.
I think this text is a bit ambiguous: should it be applied late in the development process when Lean complains, or should it be done via import instead of an explicit modifier? It's the latter, but I think readers might be confused.
| This can be overriden by giving an explicit `termination_by` metric (such as one suggested by `termination_by?`), which may be necessary when the type of the definition is not known to be `Nonempty`. | ||
|
|
||
| As a guideline, it is usually preferable to apply `meta` as late as possible. | ||
| Thus helper definitions not directly registered as metaprograms do not need to be marked if they are located in a separate module. |
There was a problem hiding this comment.
Suggested change
| Thus helper definitions not directly registered as metaprograms do not need to be marked if they are located in a separate module. | |
| In particular, helper definitions that are not directly registered as metaprograms do not need to be marked if they are located in a separate module. |
I think this is more of a "here's the important detail" sentence than an expression of causality/implication, right?
|
|
||
| As a guideline, it is usually preferable to apply `meta` as late as possible. | ||
| Thus helper definitions not directly registered as metaprograms do not need to be marked if they are located in a separate module. | ||
| Only the final module(s) actually registering metaprograms then should use `public meta import` to import those helpers and define its metaprograms using built-in syntax like `elab`, using `meta def`, or using `meta section`. |
There was a problem hiding this comment.
Suggested change
| Only the final module(s) actually registering metaprograms then should use `public meta import` to import those helpers and define its metaprograms using built-in syntax like `elab`, using `meta def`, or using `meta section`. | |
| Only the final module that actually registers a metaprogram needs the helpers as `meta` definitions. | |
| It should use `public meta import` to import those helpers and then define its metaprograms using built-in syntax like `elab`, using `meta def`, or using `meta section`. |
I think two sentences makes this easier to parse.
Can we motivate this? I see two reasons: that it enables re-use and independent non-meta testing of these helpers, and that things are generally just easier when not in meta-mode. Is there a third reason?
Kha
commented
Oct 24, 2025
| A `meta` definition may access (and thus invoke) other `meta` definitions only; a non-`meta` definition likewise may only access other non-`meta` definitions. | ||
| For imported definitions, the `meta` marker can be added after the fact using `meta import`. | ||
| `meta import`ing a definition already in the meta phase leaves it in that phase. | ||
| In addition, the import must be public if the imported definition may be compile-time executed outside the current module, i.e. if it is reachable from some public `meta` definition in the current module: use `public meta import` or, if already `meta`, `public import`. |
There was a problem hiding this comment.
I usually prefer "declaration" over "constant" in user-facing text, is there some canonized stance on that?
| For imported definitions, the `meta` marker can be added after the fact using `meta import`. | ||
| `meta import`ing a definition already in the meta phase leaves it in that phase. | ||
| In addition, the import must be public if the imported definition may be compile-time executed outside the current module, i.e. if it is reachable from some public `meta` definition in the current module: use `public meta import` or, if already `meta`, `public import`. | ||
| This is usually the case, unless a definition was imported solely for use in `local` metaprograms. |
There was a problem hiding this comment.
Suggested change
| This is usually the case, unless a definition was imported solely for use in `local` metaprograms. | |
| This is usually the case, unless a definition was imported solely for use in local metaprograms such as `local syntax/macro/elab/...`. |
There was a problem hiding this comment.
@david-christiansen Is this clearer?
Comment on lines
+149
to
+150
| As a guideline, it is usually preferable to apply `meta` as late as possible. | ||
| Thus helper definitions not directly registered as metaprograms do not need to be marked if they are located in a separate module. |
There was a problem hiding this comment.
Suggested change
| As a guideline, it is usually preferable to apply `meta` as late as possible. | |
| Thus helper definitions not directly registered as metaprograms do not need to be marked if they are located in a separate module. | |
| As a guideline, it is usually preferable to keep the amount of `meta` annotations as small as possible in order to not lock reusable declarations into the meta phase unless necessary as well as to help the build system avoid more rebuilds. | |
| Thus non-trivial amounts of code that does not contain registered metaprograms per se but that a registered metaprogram depends on should be located in a separate module and not marked `meta`. |
|
Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit fc2268d. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.