This PR refines and clarifies the `meta` phase distinction in the module
system.
* `meta import A` without `public` now has the clarified meaning of
"enable compile-time evaluation of declarations in or above `A` in the
current module, but not downstream". This is now checked statically by
enforcing that public meta defs, which therefore may be referenced from
outside, can only use public meta imports, and that global evaluating
attributes such as `@[term_parser]` can only be applied to public meta
defs.
* `meta def`s may no longer reference non-meta defs even when in the
same module. This clarifies the meta distinction as well as improves
locality of (new) error messages.
* parser references in `syntax` are now also properly tracked as meta
references.
* A `meta import` of an `import` now properly loads only the `.ir` of
the nested module for the purposes of execution instead of also making
its declarations available for general elaboration.
* `initialize` is now no longer being run on import under the module
system, which is now covered by `meta initialize`.
This PR adds documentation to builtin attributes like `@[refl]` or
`@[implemented_by]`.
Closes#8432
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: David Thrane Christiansen <david@lean-fro.org>
This PR unifies various ways of naming auxiliary declarations in a
conflict-free way and ensures the method is compatible with diverging
branches of elaboration such as parallelism or Aesop-like
backtracking+replaying search.
This PR removes functions from compiling decls from Environment, and
moves all users to functions on CoreM. This is required for supporting
the new code generator, since its implementation uses CoreM.
- Add support for reserved declaration names. We use them for theorems
generated on demand.
- Equation theorems are not private declarations anymore.
- Generate equation theorems on demand when resolving symbols.
- Prevent users from creating declarations using reserved names. Users
can bypass it using meta-programming.
See next test for examples.
This makes sure we can properly quote e.g. `deriving` clauses and avoids
a suspicious `eraseMacroScopes` call (though not at `Elab.Syntax`, since
categories do not have to be declaration names)
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
@Kha This one required a bunch of manual fixes. The main issue is that
before we added the string interpolation feature, we created
`MessageData`s using `++` and coercions. For example, given
`(e : Expr)`, we would write
```
let msg : MessageData := "type: " ++ e
```
and rely on the coercions `String -> MessageData` and
`Expr -> MessageData`, and the instance `Append MessageData`.
However, heterogeneous operators "block" the expected type propagation downwards.
This kind of code is obsolete now since we can write a more compact
version using string interpolation
```
let msg := m!"type: {e}"
```
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
Also, refuse to evaluate an `[init]` decl in the same module (since we don't know whether the initialization is
backtrackable) and always use native symbol of a `[builtinInit]` decl
