After #12001, it was no longer true that `lean_trace(name(...), ...)`
would only perform the name allocation if no trace option was set. This
PR instead avoids the allocation in any case by avoiding this pattern.
This PR changes the default of `enableArtifactCache` to use the
workspace's `enableArtifactCache` setting if the package is a dependency
and `LAKE_ARTIFACT_CACHE` is not set. This means that dependencies of a
project with `enableArtifactCache` set will also, by default, use Lake's
local artifact cache.
This PR adds `simpControl`, a simproc that handles control-flow
expressions such as `if-then-else`. It simplifies conditions while
avoiding unnecessary work on branches that won't be taken.
The key behavior of `simpControl`:
- Simplifies the condition of `if-then-else` expressions
- If the condition reduces to `True` or `False`, returns the appropriate
branch, and continue simplifying.
- If the condition simplifies to a new expression, rebuilds the
`if-then-else` with the simplified condition (synthesizing a new
`Decidable` instance), and mark it as "done". That is, simplifier main
loop will not visit branches.
- Does **not** visit branches unless the condition becomes `True` or
`False`
This is useful for symbolic simplification where we want to avoid
wasting effort
simplifying branches that may be eliminated after the condition is
resolved.
This PR also fixes a bug in `Sym/Simp/EvalGround.lean`, and adds some
helper functions.
This PR adds `Sym.Simp.evalGround`, a simplification procedure for
evaluating ground terms of builtin numeric types. It is designed for
`Sym.simp`.
Key design differences from `Meta.Simp` simprocs:
- Pure value extraction: `getValue?` functions are `OptionT Id` rather
than
`MetaM`, avoiding `whnf` overhead since `Sym` maintains canonical forms
- Specialized predicate lemmas: comparisons use pre-proved lemmas like
`Int.lt_eq_true` applied with `rfl`, avoiding `Decidable` instance
reconstruction at each call site
- Type dispatch via `match_expr`: assumes standard instances, no
synthesis
Supported types: `Nat`, `Int`, `Rat`, `Fin n`, `BitVec n`,
`UInt8/16/32/64`,
`Int8/16/32/64`.
Supported operations: arithmetic (`+`, `-`, `*`, `/`, `%`, `^`), bitwise
(`&&&`, `|||`, `^^^`, `~~~`), shifts (`<<<`, `>>>`), comparisons (`<`,
`≤`,
`>`, `≥`, `=`, `≠`, `∣`), and boolean predicates (`==`, `!=`).
This PR fixes an issue where attributes like `@[irreducible]` would not
be allowed under the module system unless combined with `@[exposed]`,
but the former may be helpful without the latter to ensure downstream
non-`module`s are also affected.
Fixes#12025
Drastically speeds up `isTracingEnabledFor` in the common case, which
has evolved from "no options set" to "`Elab.async` and probably some
linter options set but no `trace`".
## Breaking changes
`Lean.Options` is now an opaque type. The basic but not all of the
`KVMap` API has been redefined on top of it.
Ensure that individual definitions known statically to be unreachable
are stripped out by the linker instead of only whole modules. Achieves
sizeable savings today and will do more so with upcoming module system
compilation refinements.
This PR allows 'Go to Definition' to look through reducible definition
when looking for typeclass instance projections.
Specifically, this means that using 'Go to Definition' on uses of
`GT.gt` will now yield the corresponding `LT` instance as well.
This PR fixe a superliniear behavior in the closed subterm extractor.
Consider an LCNF of the shape:
```
let x1 := f arg
let x2 := f x1
let x3 := f x2
let x4 := f x3
...
```
In this case the previous closed term extraction algorithm would visit
`x1`, then `x2` and `x1`,
then `x3`,`x2`,`x1` and so on, failing each time. We now introduce a
cache to avoid this behavior.
This PR splits up the SCC that the compiler manages into (potentially)
multiple ones after
performing lambda lifting. This aids both the closed term extractor and
the elimDeadBranches pass as
they are both negatively influenced when more declarations than required
are within one SCC.
This PR fixes the pretty-printing of the `extract_lets` tactic.
Previously, the pretty-printer would expect a space after the
`extract_lets` tactic, when it was followed by another tactic on the
same line: for example,
`extract_lets; exact foo`
would be changed to
`extract_lets ; exact foo`.
This PR fixes this oversight. Found by using the pretty-printer for
formatting linting in leanprover-community/mathlib4#30658.
This PR fixes an issue where go-to-definition would jump to the wrong
location in presence of async theorems.
While the elaborator does not explicitly depend on `FVar`s not being
reused between declarations, the language server turned out to do so. As
we would have to split the name generator in any case as soon as we add
any parallelism within proofs, we now do so for any async code in order
to uphold this invariant again.
---------
Co-authored-by: mhuisi <mhuisi@protonmail.com>
This PR adds support for simplifying the arguments of over-applied and
under-applied function application terms in `Sym.simp`, completing the
implementation for all three congruence strategies (fixed prefix,
interlaced, and congruence theorems).
This PR adds missing dependencies in `src/CMakeLists.txt` to ensure that
leanrt_initial-exec, leanrt, and leancpp_1 targets wait for copy-leancpp
to complete before building. Fixes potential build race conditions in
stage 2+ builds on systems with large `nproc`.
Closes https://github.com/leanprover/lean4/issues/11808
This PR removes the need to write `.ofNat` for numeric options in
`lakefile.lean`. Note that `lake translate-config` incorrectly assumed
this was already legal in earlier revisions.
This replaces #11771.
This PR implements support for auto-generated congruence theorems in
`Sym.simp`, enabling simplification of functions with complex argument
dependencies such as proof arguments and `Decidable` instances.
Previously, `Sym.simp` used basic congruence lemmas (`congrArg`,
`congrFun`, `congrFun'`, `congr`) to construct proofs when simplifying
function arguments. This approach is efficient for simple cases but
cannot handle functions with dependent proof arguments or `Decidable`
instances that depend on earlier arguments.
The new `congrThm` function applies pre-generated congruence theorems
(similar to the main simplifier) to handle these complex cases.
This PR fixes the `floatLetIn` pass to not move variables in case it
could break linearity (owned variables being passed with RC 1). This
mostly improves the situation in the parser which previously had many
functions that were supposed to be linear in terms of `ParserState` but
the compiler made them non-linear. For an example of how this affected
parsers:
```lean-4
def optionalFn (p : ParserFn) : ParserFn := fun c s =>
let iniSz := s.stackSize
let iniPos := s.pos
let s := p c s
let s := if s.hasError && s.pos == iniPos then s.restore iniSz iniPos else s
s.mkNode nullKind iniSz
```
previously moved the `let iniSz := ...` declaration into the `hasError`
branch. However, this means that at the point of calling the inner
parser (`p c s`), the original state `s` needs to have RC>1 because it
is used later in the `hasError` branch, breaking linearity. This fix
prevents such moves, keeping `iniSz` before the `p c s` call.
This PR introduces two induction principles for bitvectors, based on the
concat and cons operations. We show how this principle can be useful to
reason about bitvectors by refactoring two population count lemmas
(`cpopNatRec_zero_le` and `toNat_cpop_append`) and introducing a new
lemma (`toNat_cpop_not`).
To use the induction principle we also move `cpopNatRec_cons_of_le` and
`cpopNatRec_cons_of_lt` earlier in the popcount section (they are the
building blocks enabling us to take advantage of the new induction
principle).
---------
Co-authored-by: luisacicolini <luisacicolini@gmail.com>
Co-authored-by: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
This PR adds missing type checking for pattern variables during pattern
matching/unification to prevent incorrect matches.
Previously, the pattern matcher could incorrectly match expressions even
when pattern variable types were incompatible with the matched subterm
types. For example, a pattern like `x` where `x : BitVec 0` could match
any term, ignoring the specific type constraint on `x`.
This PR introduces a two-phase type checking approach:
1. **Static analysis** (`mkCheckTypeMask`): Identifies which pattern
variables require type checking based on their syntactic position.
Variables that appear only as arguments to function applications skip
checking (the application structure already constrains their types),
while variables in function position, binder contexts, or standalone
positions must be checked.
2. **Runtime validation**: During matching, when a pattern variable is
assigned, its type is checked against the matched subterm's type if
flagged by the mask. Checking uses `withReducible` to balance soundness
and performance.
The PR also adds helper functions for debugging (`Sym.mkMethods`,
`Sym.simpWith`, `Sym.simpGoal`) and fixes a minor issue where
`Theorem.rewrite` could return `.step` with identical expressions
instead of `.rfl`.Body:
This PR optimizes congruence proof construction in `Sym.simp` by
avoiding
`inferType` calls on expressions that are less likely to be cached.
Instead of
inferring types of expressions like `@HAdd.hAdd Nat Nat Nat instAdd 5`,
we infer
the type of the function prefix `@HAdd.hAdd Nat Nat Nat instAdd` and
traverse
the forall telescope.
The key insight is that function prefixes are more likely shared across
many call sites
(e.g., all `Nat` additions use the same `@HAdd.hAdd Nat Nat Nat
instAdd`), so they
benefit from `inferType` caching.
Benchmark results show improvements on workloads with shared function
prefixes:
- `many_rewrites_5000`: 48.8ms → 43.1ms (-12%)
- `term_tree_5000`: 53.4ms → 30.5ms (-43%)
This PR implements a new strategy for simplifying `have`-telescopes in
`Sym.simp` that achieves linear kernel type-checking time instead of
quadratic.
## Problem
When simplifying deep `have`-telescopes, the previous approach using
`have_congr'` produced proofs that type-checked in quadratic time. The
simplifier itself was fast, but the kernel became the bottleneck for
large telescopes.
For example, at n=100:
- **Before**: simp = 2.4ms, kernel = **225ms**
- **After**: simp = 3.5ms, kernel = **10ms**
The quadratic behavior occurred because the kernel creates fresh free
variables for each binder when type-checking, destroying sharing and
producing O(n²) intermediate terms.
## Solution
We transform sequential `have`-telescopes into a parallel
beta-application form:
```
have x₁ := v₁; have x₂ := v₂[x₁]; b[x₁, x₂]
↓ (definitionally equal)
(fun x₁ x₂' => b[x₁, x₂' x₁]) v₁ (fun x₁ => v₂[x₁])
```
This parallel form leverages the efficient simplifier for lambdas in
`Sym.simp`. This form enables:
1. Independent simplification of each argument
2. Proof construction using standard congruence lemmas
3. Linear kernel type-checking time
The algorithm has three phases:
1. **`toBetaApp`**: Transform telescope → parallel beta-application
2. **`simpBetaApp`**: Simplify using `congr`/`congrArg`/`congrFun'` and
`simpLambda`
3. **`toHave`**: Convert back to `have` form
## Benchmark Results
### Benchmark 1: Chain with all variables used in body
| n | Before (simp) | Before (kernel) | After (simp) | After (kernel) |
|---|---------------|-----------------|--------------|----------------|
| 50 | 1.2ms | 32ms | 1.6ms | 4.4ms |
| 100 | 2.4ms | **225ms** | 3.5ms | **10ms** |
| 200 | 4.5ms | — | 8.4ms | 27ms |
| 500 | 11.7ms | — | 33.6ms | 128ms |
### Benchmark 3: Parallel declarations (simplified values)
| n | Before (simp) | Before (kernel) | After (simp) | After (kernel) |
|---|---------------|-----------------|--------------|----------------|
| 50 | 0.5ms | 24ms | 0.8ms | 1.8ms |
| 100 | 1.2ms | **169ms** | 1.8ms | **5.3ms** |
| 200 | 2.2ms | — | 3.9ms | 17ms |
| 500 | 5.9ms | — | 12.3ms | 93ms |
### Benchmark 5: Chain with single dependency
| n | Before (simp) | Before (kernel) | After (simp) | After (kernel) |
|---|---------------|-----------------|--------------|----------------|
| 100 | 1.6ms | 6.2ms | 1.8ms | 6.2ms |
| 200 | 2.8ms | 21.6ms | 4.4ms | 16.5ms |
| 500 | 7.3ms | **125ms** | 12.8ms | **72ms** |
Key observations:
- Kernel time is now **linear** in telescope depth (previously
quadratic)
- Simp time increases slightly due to the transformation overhead
- Total time (simp + kernel) is dramatically reduced for large
telescopes
- The improvement is most pronounced when the body depends on many
variables
## Trade-offs
- Proof sizes are larger (more congruence lemma applications)
- Simp time has ~1.5x overhead from the transformation
- For very small telescopes (n < 10), the overhead may not pay off
The optimization targets the critical path: kernel type-checking was the
bottleneck preventing scaling to realistic symbolic simulation
workloads.
