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 fixes the documentation of the pipe operator |>, which is
currently (emphasis mine):
> Haskell-like pipe operator `|>`. `x |> f` means **the same as the same
as** `f x`,
> and it chains such that `x |> f |> g` is interpreted as `g (f x)`.
This PR updates the formatting of, and adds explanations for, "unknown
identifier" errors as well as "failed to infer type" errors for binders
and definitions.
It attempts to ameliorate some of the confusion encountered in #1592 by
modifying the wording of the "header is elaborated before body is
processed" note and adding further discussion and examples of this
behavior in the corresponding error explanation.
This PR adjusts the experimental module system to make `private` the
default visibility modifier in `module`s, introducing `public` as a new
modifier instead. `public section` can be used to revert the default for
an entire section, though this is more intended to ease gradual adoption
of the new semantics such as in `Init` (and soon `Std`) where they
should be replaced by a future decl-by-decl re-review of visibilities.
This PR implements signature help support. When typing a function
application, editors with support for signature help will now display a
popup that designates the current (remaining) function type. This
removes the need to remember the function signature while typing the
function application, or having to constantly cycle between hovering
over the function identifier and typing the application. In VS Code, the
signature help can be triggered manually using `Ctrl+Shift+Space`.
### Other changes
- In order to support signature help for the partial syntax `f a <|` or
`f a $`, these notations now elaborate as `f a`, not `f a .missing`.
- The logic in `delabConstWithSignature` that delaborates parameters is
factored out into a function `delabForallParamsWithSignature` so that it
can be used for arbitrary `forall`s, not just constants.
- The `InfoTree` formatter is adjusted to produce output where it is
easier to identify the kind of `Info` in the `InfoTree`.
- A bug in `InfoTree.smallestInfo?` is fixed so that it doesn't panic
anymore when its predicate `p` does not ensure that both `pos?` and
`tailPos?` of the `Info` are present.
This PR makes `#guard_msgs` to treat `trace` messages separate from
`info`, `warning` and `error`. It also introduce the ability to say
`#guard_msgs (pass info`, like `(drop info)` so far, and also adds
`(check info)` as the explicit form of `(info)`, for completeness.
Fixes#8266
This PR provides a basic API for a premise selection tool, which can be
provided in downstream libraries. It does not implement premise
selection itself!
This PR adds a convenience command `#info_trees in`, which prints the
info trees generated by the following command. It is useful for
debugging or learning about `InfoTree`.
This PR modifies structure instance notation and `where` notation to use
the same notation for fields. Structure instance notation now admits
binders, type ascriptions, and equations, and `where` notation admits
full structure lvals. Examples of these for structure instance notation:
```lean
structure PosFun where
f : Nat → Nat
pos : ∀ n, 0 < f n
def p : PosFun :=
{ f n := n + 1
pos := by simp }
def p' : PosFun :=
{ f | 0 => 1
| n + 1 => n + 1
pos := by rintro (_|_) <;> simp }
```
Just like for the structure `where` notation, a field `f x y z : ty :=
val` expands to `f := fun x y z => (val : ty)`. The type ascription is
optional.
The PR also is setting things up for future expansion. Pending some
discussion, in the future structure/`where` notation could have have
embedded `where` clauses; rather than `{ a := { x := 1, y := z } }` one
could write `{ a where x := 1; y := z }`.
This refactors and improves the `#eval` command, introducing some new
features.
* Now evaluated results can be represented using `ToExpr` and pretty
printing. This means **hoverable output**. If `ToExpr` fails, it then
tries `Repr` and then `ToString`. The `eval.pp` option controls whether
or not to try `ToExpr`.
* There is now **auto-derivation** of `Repr` instances, enabled with the
`pp.derive.repr` option (default to **true**). For example:
```lean
inductive Baz
| a | b
#eval Baz.a
-- Baz.a
```
It simply does `deriving instance Repr for Baz` when there's no way to
represent `Baz`. If core Lean gets `ToExpr` derive handlers, they could
be used here as well.
* The option `eval.type` controls whether or not to include the type in
the output. For now the default is false.
* Now things like `#eval do return 2` work. It tries using
`CommandElabM`, `TermElabM`, or `IO` when the monad is unknown.
* Now there is no longer `Lean.Eval` or `Lean.MetaEval`. These each used
to be responsible for both adapting monads and printing results. The
concerns have been split into two. (1) The `MonadEval` class is
responsible for adapting monads for evaluation (it is similar to
`MonadLift`, but instances are allowed to use default data when
initializing state) and (2) finding a way to represent results is
handled separately.
* Error messages about failed instance synthesis are now more precise.
Once it detects that a `MonadEval` class applies, then the error message
will be specific about missing `ToExpr`/`Repr`/`ToString` instances.
* Fixes a bug where `Repr`/`ToString` instances can't be found by
unfolding types "under the monad". For example, this works now:
```lean
def Foo := List Nat
def Foo.mk (l : List Nat) : Foo := l
#eval show Lean.CoreM Foo from do return Foo.mk [1,2,3]
```
* Elaboration errors now abort evaluation. This eliminates some
not-so-relevant error messages.
* Now evaluating a value of type `m Unit` never prints a blank message.
* Fixes bugs where evaluating `MetaM` and `CoreM` wouldn't collect log
messages.
The `run_cmd`, `run_elab`, and `run_meta` commands are now frontends for
`#eval`.
The `#guard_msgs` command runs the command it is attached to as if it
were a top-level command. This is because the top-level command
elaborator runs linters, and we are interested in capturing linter
warnings using `#guard_msgs`. However, the linters will run on
`#guard_msgs` itself, leading sometimes to duplicate warnings (like for
the unused variable linter).
Rather than special-casing `#guard_msgs` in every affected linter, this
PR special-cases it in the top-level command elaborator itself. **Now
linters are only run if the command doesn't contain `#guard_msgs`.**
This way, the linters are only run on the sub-command that `#guard_msgs`
runs itself. This rule also keeps linters from running multiple times in
cases such as `set_option pp.mvars false in /-- ... -/ #guard_msgs in
...`.
We swap the arguments for `Membership.mem` so that when proceeded by a
`SetLike` coercion, as is often the case in Mathlib, the resulting
expression is recognized as eta expanded and reduce for many
computations. The most beneficial outcome is that the discrimination
tree keys for instances and simp lemmas concerning subsets become more
robust resulting in more efficient searches.
Closes `RFC` #4932
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Henrik Böving <hargonix@gmail.com>
the internal constructions for structural and well-founded recursion
use plenty of `PProd` and `MProd`, and reading these, deeply
nested and in prefix notation, is unnecessarily troublesome.
Therefore this introduces notations
```
a ×ₚ b -- PProd a b
a ×ₘ b -- MProd a b
()ₚ -- PUnit.unit
(x,y,z)ₚ -- PProd.mk x (PProd.mk y z)
(x,y,z)ₘ -- MProd.mk x (MProd.mk y z)
```
(This is part 1, the rest will follow in #4730 after a stage0 update.)
Adds a command and tactic to print the `Array <| DiscrTree.Key` for
equalities helping the user to debug perceived `simp` failures.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Complement to #3967 , adds a `(since := "<date>")` field to
`@[deprecated]` so that metaprogramming code has access to the
deprecation date for e.g. bulk removals. Also adds `@[deprecated
"deprecation message"]` to optionally replace the default text
"`{declName}` has been deprecated, use `{newName}` instead".
Adds options to control whitespace normalization and message ordering in
`#guard_msgs`.
Examples:
1. `#guard_msgs (whitespace := lax)` ignores differences in whitespace
completely.
2. `#guard_msgs (whitespace := exact)` requires an exact match for
whitespace (after trimming).
3. `#guard_msgs (ordering := sorted)` sorts the list of messages, to
make it insensitive to message order.
This is a quite substantial tactic.
It also includes the infamour `NatCast` typeclass (which I've equipped
with a module-doc). I wasn't at all sure where that should live, so it
is currently randomly in `Lean/Elan/Tactic/NatCast.lean`: presumably if
we're doing this it will go somewhere in `Init`.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Moves the `@[coe]` attribute and associated elaborators/delaborators
from Std to Lean.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
