This PR ensures the new code generator produces code for `opaque`
definitions that are not tagged as `@[extern]`.
Remark: This is the behavior of the old code generator.
This PR adds the `--error=kind` option (shorthand: `-Ekind`) to the
`lean` CLI. When set, messages of `kind` (e.g.,
`linter.unusedVariables`) will be reported as errors. This setting does
nothing in interactive contexts (e.g., the server).
Closes#5194.
The spelling `--error` was chosen instead of the common `-Werror` both
for practical and behavioral reasons. Behaviorally, this option effects
not just warnings, but informational messages as well. Practically,
`-Werror` conflicts with the existing `-W` option for the worker and
`lean` also does not currently use long single-hyphen option names.
This PR ensures that the configuration in `Simp.Config` is used when
reducing terms and checking definitional equality in `simp`.
closes#5455
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR fixes a bug in the simplifier. It was producing terms with loose
bound variables when eliminating unused `let_fun` expressions.
This issue was affecting the example at #6374. The example is now timing
out.
This PR makes it harder to create "fake" theorems about definitions that
are stubbed-out with `sorry` by ensuring that each `sorry` is not
definitionally equal to any other. For example, this now fails:
```lean
example : (sorry : Nat) = sorry := rfl -- fails
```
However, this still succeeds, since the `sorry` is a single
indeterminate `Nat`:
```lean
def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds
```
One can be more careful by putting parameters to the right of the colon:
```lean
def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails
```
Most sources of synthetic sorries (recall: a sorry that originates from
the elaborator) are now unique, except for elaboration errors, since
making these unique tends to cause a confusing cascade of errors. In
general, however, such sorries are labeled. This enables "go to
definition" on `sorry` in the Infoview, which brings you to its origin.
The option `set_option pp.sorrySource true` causes the pretty printer to
show source position information on sorries.
**Details:**
* Adds `Lean.Meta.mkLabeledSorry`, which creates a sorry that is labeled
with its source position. For example, `(sorry : Nat)` might elaborate
to
```
sorryAx (Lean.Name → Nat) false
`lean.foo.12.8.12.13.8.13._sorry._@.lean.foo._hyg.153
```
It can either be made unique (like the above) or merely labeled. Labeled
sorries use an encoding that does not impact defeq:
```
sorryAx (Unit → Nat) false (Function.const Lean.Name ()
`lean.foo.14.7.13.7.13.69._sorry._@.lean.foo._hyg.174)
```
* Makes the `sorry` term, the `sorry` tactic, and every elaboration
failure create labeled sorries. Most are unique sorries, but some
elaboration errors are labeled sorries.
* Renames `OmissionInfo` to `DelabTermInfo` and adds configuration
options to control LSP interactions. One field is a source position to
use for "go to definition". This is used to implement "go to definition"
on labeled sorries.
* Makes hovering over a labeled `sorry` show something friendlier than
that full `sorryAx` expression. Instead, the first hover shows the
simplified ``sorry `«lean.foo:48:11»``. Hovering over that hover shows
the full `sorryAx`. Setting `set_option pp.sorrySource true` makes
`sorry` always start with printing with this source position
information.
* Removes `Lean.Meta.mkSyntheticSorry` in favor of `Lean.Meta.mkSorry`
and `Lean.Meta.mkLabeledSorry`.
* Changes `sorryAx` so that the `synthetic` argument is no longer
optional.
* Gives `addPPExplicitToExposeDiff` awareness of labeled sorries. It can
set `pp.sorrySource` when source positions differ.
* Modifies the delaborator framework so that delaborators can set Info
themselves without it being overwritten.
Incidentally closes#4972.
Inspired by [this Zulip
thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Is.20a.20.60definition_wanted.60.20keyword.20possible.3F/near/477260277).
This PR makes all message constructors handle pretty printer errors.
Prior to this change, pretty printer errors in messages were not
uniformly handled. In core, some printers capture their errors (e.g.,
`ppExprWithInfos` and `ppTerm` ) and some do not (e.g., `ppGoal` and
`ppSignature`) propagate them to whatever serializes the message (e.g.,
the frontend).
To resolve this inconsistency and uniformly handle errors, the signature
for `ofLazy` now uses `BaseIO`. As such, all printers been adapted to
capture any errors within them and print similar messages to
`ppExprWithInfos` and `ppTerm` on such errors.
This PR adjusts the way the pretty printer unresolves names. It used to
make use of all `export`s when pretty printing, but now it only uses
`export`s that put names into parent namespaces (heuristic: these are
"API exports" that are intended by the library author), rather than
"horizontal exports" that put the names into an unrelated namespace,
which the dot notation feature in #6189 now incentivizes.
Closes the already closed#2524
This PR adds docstrings to `Expr.hasLooseBVars` and `Expr.hasLooseBVar`,
to clarify the difference between these functions, and to document that
the former traverses the expression, while the latter is constant-time,
using cached information.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR removes the deprecated aliases `Int.div := Int.tdiv` and
`Int.mod := Int.tmod`. Later we will rename `Int.ediv` to `Int.div` and
`Int.emod` to `Int.mod`.
This PR removes unnecessary parameters from the funcion induction
principles. This is a breaking change; broken code can typically be adjusted
simply by passing fewer parameters.
Part 2, adjusting after stage0 update.
Closes#6320
This PR removes unnecessary parameters from the funcion induction
principles. This is a breaking change; broken code can typically be adjusted
simply by passing fewer parameters.
Part 1, before stage0 update.
Closes#6320
This PR upstreams the `ToLevel` typeclass from mathlib and uses it to
fix the existing `ToExpr` instances so that they are truly universe
polymorphic (previously it generated malformed expressions when the
universe level was nonzero). We improve on the mathlib definition of
`ToLevel` to ensure the class always lives in `Type`, irrespective of
the universe parameter.
This implements part one of the plan to upstream a derive handler for
`ToExpr`, as discussed in #5906 and #5909.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This PR moves `IO.Channel` and `IO.Mutex` from `Init` to `Std.Sync` and
renames them to `Std.Channel` and `Std.Mutex`.
Note that the original files are retained and the deprecation is written
manually as we cannot import `Std` from `Init` so this is the only way
to deprecate without a hard breaking change. In particular we do not yet
move `Std.Queue` from `Init` to `Std` both because it needs to be
retained for this deprecation to work but also because it is already
within the `Std` namespace and as such we cannot maintain two copies of
the file at once. After the deprecation period is finished `Std.Queue`
will find a new home in `Std.Data.Queue`.
This PR uses Lean.RArray in bv_decide's reflection proofs. Giving
speedups on problems with lots of variables.
Implement like #6068, speedup:
```
# before
λ hyperfine "lean +nightly-2024-12-02 tests/lean/run/bv_reflection_stress.lean"
Benchmark 1: lean +nightly-2024-12-02 tests/lean/run/bv_reflection_stress.lean
Time (mean ± σ): 1.939 s ± 0.007 s [User: 1.549 s, System: 0.104 s]
Range (min … max): 1.928 s … 1.947 s 10 runs
# after
λ hyperfine "lean tests/lean/run/bv_reflection_stress.lean"
Benchmark 1: lean tests/lean/run/bv_reflection_stress.lean
Time (mean ± σ): 1.409 s ± 0.006 s [User: 1.058 s, System: 0.073 s]
Range (min … max): 1.401 s … 1.419 s 10 runs
```
This PR runs all linters for a single command (together) on a separate
thread from further elaboration, making a first step towards
parallelizing the elaborator.
This PR ensure `bv_decide` uses definitional equality in its reflection
procedure as much as possible. Previously it would build up explicit
congruence proofs for the kernel to check. This reduces the size of
proof terms passed to kernel speeds up checking of large reflection
proofs.
This PR fixes a bug in structure instance field completion that caused
it to not function correctly for bracketed structure instances written
in Mathlib style.
This PR fixes a bug that could cause the `injectivity` tactic to fail in
reducible mode, which could cause unfolding lemma generation to fail
(used by tactics such as `unfold`). In particular,
`Lean.Meta.isConstructorApp'?` was not aware that `n + 1` is equivalent
to `Nat.succ n`.
Closes#5064
This PR puts code in terms of syntax quotations now that there has been
a stage0 update. Fixes a lingering bug in StructInst where some
intermediate syntax was malformed, but this had no observable effects
outside of some debug messages.
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 PR implements `Simp.Config.implicitDefEqsProofs`. When `true`
(default: `true`), `simp` will **not** create a proof term for a
rewriting rule associated with an `rfl`-theorem. Rewriting rules are
provided by users by annotating theorems with the attribute `@[simp]`.
If the proof of the theorem is just `rfl` (reflexivity), and
`implicitDefEqProofs := true`, `simp` will **not** create a proof term
which is an application of the annotated theorem.
The default setting does change the existing behavior. Users can use
`simp -implicitDefEqProofs` to force `simp` to create a proof term for
`rfl`-theorems. This can positively impact proof checking time in the
kernel.
This PR also fixes an issue in the `split` tactic that has been exposed
by this feature. It was looking for `split` candidates in proofs and
implicit arguments. See new test for issue exposed by the previous
feature.
---------
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR fixes a performance issue where the Lean language server would
walk the full project file tree every time a file was saved, blocking
the processing of all other requests and notifications and significantly
increasing overall language server latency after saving.
This issue was originally reported at
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Compiling.20too.20slow/near/484386515
and uncovered in a lengthy investigation. The performance bug that
causes the Lean language server to walk the full project file tree when
the file watcher for .ilean files is triggered was introduced when the
.ileans were first introduced, whereas the specific issue of file saving
also triggering the walk was introduced by #3247 in 4.8.0 and the use of
the file watcher for .lean files, which would then also trigger the
directory walk. Combining this with VS Code's auto-save feature causes
the language server to walk the full project file tree on every change
of the document.
It somehow hasn't really been much of an issue until now, but we still
do way too much work in the watchdog main loop. I'll look into resolving
that more general issue in the future.
This PR ensures that nesting trace nodes are annotated with timing
information iff `trace.profiler` is active.
The previous connection to the otherwise unrelated `profiler` option was
a remnant from before `trace.profiler` existed; if users want to
annotate explicitly activated trace classes only, they can instead
increase `trace.profiler.threshold`.
This PR adds the builtin simproc `USize.reduceToNat` which reduces the
`USize.toNat` operation on literals less than `UInt32.size` (i.e.,
`4294967296`).
This PR deprecates `Fin.ofNat` in favour of `Fin.ofNat'` (which takes an
`[NeZero]` instance, rather than returning an element of `Fin (n+1)`).
After leaving the deprecation warning in place for some time, we will
then rename `ofNat'` back to `ofNat`.
This PR adds `Lean.loadPlugin` which exposes functionality similar to
the `lean` executable's `--plugin` option to Lean code.
This will allow custom Lean frontends (e.g., Lake, the Lean language
server) to also load plugins.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
