This PR fixes the `workflow_dispatch` path for nightly releases.
Previously,
when a scheduled nightly failed (so no tag was created) and someone
manually
re-triggered the workflow, it would find the most recent existing
nightly tag
(from a previous day) and create a `-revK` revision of that old tag. Now
it
checks if today's nightly tag exists: if not, it creates it directly; if
it
already exists, it creates a `-revK` revision as before.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR adds the `register_sym_simp` command for declaring named
`Sym.simp`
variants with `pre`/`post` simproc chains and optional config overrides.
```
register_sym_simp myVariant where
pre := telescope
post := ground >> rewrite [thm1, thm2] with self
maxSteps := 50000
```
- `SymSimpVariant` structure storing `pre?`/`post?` syntax (elaborated
at use
time in `GrindTacticM`) and `Config` overrides
- `SimpleScopedEnvExtension` for persistent cross-module variant storage
- `register_sym_simp` command syntax with `sym_simp_field` category
- Command elaborator with syntax quotation matching and duplicate field
detection
- `getSymSimpVariant?` lookup function
- `deriving Inhabited` on `Simp.Config` for extension support
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR adds `r == e` guards to the `norm_eq_var` and
`norm_eq_var_const` branches of `Int.Linear.simpEq?`. Without these
guards, `simpEq?` returns a non-trivial proof for already-normalized
equations like `x = -1`, causing `exists_prop_congr` to fire repeatedly
and build an infinitely growing term.
The existing `Nat.simpCnstrPos?` already had the equivalent guard (`if r
!= lhs then ... else return none`).
Closes#12812
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes#12842 where `grind` exhausts memory on goals involving
high-degree polynomials such as `(x + y)^2 = x^128 + y^2` over `Fin 2`.
The root cause is that `incSteps` in the ring module's Groebner basis
engine increments the step counter by 1 per simplification, regardless
of polynomial size. For high-degree polynomials (e.g., degree 128),
intermediate results can have hundreds of terms, making each operation
extremely expensive — but the flat counter cannot catch this before
memory is exhausted.
The fix weights each step by `Poly.numTerms` of the result polynomial
and increases the default `ringSteps` from 10 000 to 100 000 to
accommodate the new cost model.
Note: the example from #12842 will not be *proved* by `grind` even after
this fix, because Frobenius / Fermat's little theorem (`x^p = x` in `Fin
p`) is not available in core Lean. The long-term plan is to introduce a
type class in core stating this property, with an instance provided by
Mathlib, so that `grind` can exploit it when Mathlib is imported.
Closes #12842🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes a nondeterministic crash in `grind` caused by a
`BEq`/`Hashable` invariant
violation in the congruence table. `congrHash` uses each expression's
own `funCC` flag to
compute its hash (one-level decomposition for `funCC = true`, full
recursive decomposition
for `funCC = false`), but `isCongruent` only checked the stored
expression's flag. When two
expressions with mismatched `funCC` flags accidentally hash-collided
(via pointer-based
`ptrAddrUnsafe` hashing), `isCongruent` could declare them congruent
despite different
argument counts, leading to an assertion failure in `mkCongrProof`.
The fix requires matching `funCC` flags in `isCongruent`. The PR also
fixes the debug
invariant checker (`checkParents`) to skip `funCC` parents and adds a
regression test for
funCC congruence.
Observed as a nondeterministic crash in Mathlib at
`Analysis/ODE/PicardLindelof.lean`.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds the infrastructure for simproc and discharger DSLs used to
specify `pre`/`post` simproc chains and conditional rewrite dischargers
in `Sym.simp` variants.
**Syntax categories** (`src/Init/Sym/Simp/SimprocDSL.lean`):
- `sym_simproc` with primitives (`ground`, `telescope`, `rewrite`,
`self`, `none`) and combinators (`>>`, `<|>`)
- `sym_discharger` with primitives (`self`, `none`) for the `with`
clause of `rewrite`
**Elaboration attributes**
(`src/Lean/Elab/Tactic/Grind/SimprocDSL.lean`):
- `builtin_sym_simproc` / `sym_simproc` mapping syntax to `Syntax →
GrindTacticM Simproc`
- `builtin_sym_discharger` / `sym_discharger` mapping syntax to `Syntax
→ GrindTacticM Discharger`
- `elabSymSimproc`, `elabSymDischarger`, and `elabWithClause`
dispatchers
Built-in elaborators for each primitive/combinator will follow in a
subsequent PR after the stage0 update.
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR fixes an issue where `grind` could prove each conjunct
individually but failed on the conjunction. The root cause:
`solverAction`'s `.propagated` path calls `processNewFacts` which drains
the `newFacts` queue, but the resulting propagation cascade (congruence
closure, or-propagation, `propagateForallPropDown`) can call
`addNewRawFact`, enqueuing to the separate `newRawFacts` queue. These
raw facts were never drained.
The fix moves `Solvers.mkAction` from `Types.lean` to `Intro.lean` where
it can compose the core solver action with `assertAll`, unconditionally
draining `newRawFacts` after every solver step.
Closes#12581
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds named theorem sets for `Sym.simp` with associated
attributes, following the same pattern as `Meta.simp`'s
`register_simp_attr`.
- `register_sym_simp_attr my_set` creates a named set with its own
`PersistentEnvExtension` and attribute
- `@[my_set] theorem ...` adds a rewrite theorem
- `@[my_set] def ...` adds equation theorems from the definition
- `builtin_initialize symSimpExtension` registers a default
`@[sym_simp]` set
- `getSymSimpTheorems` / `getSymSimpExtension?` retrieve theorem sets at
tactic time
New files:
- `Sym/Simp/Attr.lean`: attribute logic (`mkSymSimpAttr`,
`registerSymSimpAttr`)
- `Sym/Simp/RegisterCommand.lean`: `register_sym_simp_attr` macro
Tests:
- `tests/pkg/sym_simp_attr/`: package test with user-defined set
(`my_sym_simp`)
- `tests/elab/sym_simp_set.lean`: tests for the builtin `@[sym_simp]`
set
This PR makes errors in `lake cache get` / `lake cache put` artifact
transfers more verbose, which helps with debugging. It also fixes an
issue with error reporting when downloading artifacts on demand.
This PR removes the custom `M`/`State` monad from structural recursion
elaboration, replacing it with plain `MetaM`. This simplifies the code
and makes the control flow more explicit, in preparation for #12987
which
introduces named `_f` auxiliary definitions for structural recursion.
Key changes:
- Remove `State`/`M` types from `Structural.Basic`, use `MetaM`
throughout
- Extract `withRecFunsAsAxioms` helper for adding recursive functions as
temporary axioms
- Split `tryAllArgs` into `findRecArgCandidates` (analysis) and
`tryCandidates` (backtracking execution)
- Move `withoutModifyingEnv` into each phase that needs it
- For inductive predicates, return matchers from `mkIndPredBRecOnF`
instead of accumulating in state
- Pass `fnTypes` explicitly to `mkBRecOnMotive` instead of re-inferring
This is a pure refactoring with no behavior changes (except matcher
numbering in `inductive_pred` test due to changed
`saveState`/`restoreState` boundaries).
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR further enforces that all modules used in compile-time execution
must be meta imported in preparation for enabling
https://github.com/leanprover/lean4/pull/10291
# Breaking changes
Metaprograms that call `compileDecl` directly may now need to call
`markMeta` first where appropriate, possibly based on the value of
`isMarkedMeta` of existing decls. `addAndCompile` should be split into
`addDecl` and `compileDecl` for this in order to insert the call in
between.
This PR increases Lean's default stack size, including for the main
thread of Lean executables, to 1GB.
As stack pages are allocated dynamically, this should not change the
memory usage of programs but can prevent them from stack overflowing.
The stack size (of any Lean thread) can now be customized via the
`LEAN_STACK_SIZE_KB` environment variable. `main` can be prevented from
running on a new thread by setting `LEAN_MAIN_USE_THREAD=0`, in which
case the default OS stack size management applies to the main thread
again.
This PR enables support for respecting user provided borrow annotations.
This allows user to mark arguments of their definitions or local
functions with `(x : @&Ty)` and have the borrow inference try its best
to preserve this annotation, thus potentially reducing RC pressure. Note
that in some cases this might not be possible. For example, the compiler
prioritizes preserving tail calls over preserving borrow annotations. A
precise reasoning of why the compiler chose to make its inference
decisions can be obtained with `trace.Compiler.inferBorrow`.
The implementation consists of two parts:
1. A propagator in ToLCNF. This is required because the elaborator does
not place the borrow annotations in the function binders themselves but
just in type annotations of let binders/global declarations while LCNF
expects them in the lambda variable binders themselves. Thus ToLCNF now
implements a (very weak but strong enough for this purpose) propagator
of the borrow annotations of a type annotation into the variable binders
of the term affected by the annotations
2. A weakening of the InferBorrow heuristic. It now has a set of
"forced" and "non-forced" reasons to mark a variable as owned instead of
borrowed. If a variable is user annotated as borrowed, it will only be
marked as owned if the reason is a forced one, e.g. preservation of tail
calls.
This PR speeds up some benchmarks when run as tests by lowering their
workload. It also stops testing some of the more expensive benchmarks
that can't be easily made smaller.
The ultimate goal of this work is to turn production of `.ir` files into
separate build step so that it does not block non-`meta` imports and can
be skipped entirely when not needed. This PR implements the main logic
of this new `leanir` compiler executable and runs it after `lean` inside
the same Lake build step but leaves its use disabled behind a
`compiler.postponeCompile` flag until further Lake adjustments move it
to a separate facet so that its use can be actually beneficial.
---------
Co-authored-by: Joscha <joscha@plugh.de>
This PR reorganizes the instances `ToString Int` and `Repr Int` so that
they both point at a common definition `Int.repr` (the same setup is
used for `Nat`). It then verifies the functions `Int.repr`,
`String.isInt` and `String.toInt`.
In particular, for `a : Int` we get `a.repr.toInt? = some a`, which
implies that `Int.repr` is injective.
This PR adds per-result `contextDependent` tracking to `Sym.Simp.Result`
and splits the simplifier cache into persistent (context-independent)
and transient (context-dependent, cleared on binder entry). This
replaces the coarse `wellBehavedMethods` flag.
Key changes:
- Add `contextDependent : Bool := false` to `Result.rfl` and
`Result.step`
- Split `State.cache` into `persistentCache` and `transientCache`
- Remove `wellBehavedMethods` from `Methods`
- Replace `withoutModifyingCacheIfNotWellBehaved` with
`withFreshTransientCache`
- Change `DischargeResult` to an inductive (`.failed`/`.solved`)
- Add `dischargeAssumption` (context-dependent discharger for testing)
- Add `sym.simp.debug.cache` trace class
- Propagate `contextDependent` through all combinators (congruence,
transitivity, control flow, arrows, rewriting)
- Add `mkRflResult`/`mkRflResultCD` to avoid dynamic allocation of rfl
results
- Fix `isRfl` to ignore `contextDependent` (was silently broken by the
extra field)
Propagation invariant: when combining sub-results, `cd` is the
disjunction of ALL sub-results' flags — including `.rfl` results. If
`simp` returned `.rfl (contextDependent := true)`, it means `simp` might
take a completely different code path in another local context, so all
downstream results must be marked context-dependent.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR introduces the `URI` data type.
This contains the same code as #10478, divided into separate pieces to
facilitate easier review.
The pieces of this feature are:
- Core data structures: #12126
- Headers: #12127
- URI: #12128
- Body: #12144
- H1: #12146
- Server: #12151
- Client:
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR introduces the functions `String.Slice.skipPrefix?`,
`String.Slice.Pos.skip?`, `String.Slice.skipPrefixWhile`,
`String.Slice.Pos.skipWhile` and redefines `String.Slice.takeWhile` and
`String.Slice.dropWhile` to use these new functions.
This PR fixes an issue where the `induction` and `cases` tactics would
swallow diagnostics (such as unsolved goals errors) when the `using`
clause contains a nested tactic.
Closes#12815
This PR renames the function `ForwardPattern.dropPrefix?` to
`ForwardPattern.skipPrefix`?
This function `(s : String.Slice) -> Option s.Pos` is not to be confused
with `String.Slice.dropPrefix? : (s : String.Slice) -> Option
String.Slice`.
This PR fixes the interaction between `cbv_opaque` and
`inline`/`always_inline` annotations, to make sure that inlined
definitions marked as `cbv_opaque` are not unfolded during the
preprocessing stage of `cbv` tactic.
This PR redefines the `String.isNat` function to use less state and
perform short-circuiting. It then verifies the `String.isNat` and
`String.toNat?` functions.
Recall that `isNat` and `toNat?` allow `_` as a digit separator. This is
why we get the complicated statement
```lean
public theorem isNat_iff {s : String} :
s.isNat = true ↔
s ≠ "" ∧
(∀ c ∈ s.toList, c.isDigit ∨ c = '_') ∧
¬ ['_', '_'] <:+: s.toList ∧
s.toList.head? ≠ some '_' ∧
s.toList.getLast? ≠ some '_'
```
For `toNat?`, we prove the fully general
```lean
public theorem toNat?_eq_some_ofDigitChars {s : String} (h : s.isNat = true) :
s.toNat? = some (Nat.ofDigitChars 10 (s.toList.filter (· != '_')) 0)
```
as well as the useful `(Nat.repr n).toNat? = some n` (and the corollary
that `Nat.repr` is injective).
For people implementing formatting routines that involve digit
separators, we have
```lean
public theorem isNat_of_isDigit {s : String} (hne : s ≠ "")
(hdigit : ∀ c ∈ s.toList, c.isDigit) : s.isNat = true
public theorem isNat_append_underscore_append {s t : String}
(hs : s.isNat = true) (ht : t.isNat = true) :
(s ++ "_" ++ t).isNat = true
public theorem toNat?_append_underscore_append_eq_some {s t : String} {n m : Nat}
(hs : s.toNat? = some n) (ht : t.toNat? = some m) :
(s ++ "_" ++ t).toNat? =
some (10 ^ (t.toList.filter (· != '_')).length * n + m)
```
The missing bit here is `(s.leftpad k '0').toNat? = s.toNat?`, which is
missing because we don't have `String.leftpad` (yet). For any reasonable
definition of `leftpad`, this will follow from
`toNat?_eq_some_ofDigitChars` since we prove the necessary ingredients
about `ofDigitChars`.
There are some rough edges around `ofDigitChars`, and in the future it
will be nice to connect this all to mathlib's `Nat.digits` and
`Nat.ofDigits`, which are similar but different.
This PR makes `#print` show the full internal private name (including
module prefix) in the declaration signature when `pp.privateNames` is
set to true. Previously, `pp.privateNames` only affected names in the
body but the signature always stripped the private prefix.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes a series of errors in docstrings.
This includes:
- incorrect gramar
- errant reference to "dependent" in the non-dependent `HashMap` files
- reference to expression metavariables as universe level metavariables
- outdated reference to `usizeSz` instead of `USize.size`
- syntax errors in code examples
- a broken link to a paper
---------
Co-authored-by: Derrik Petrin <derrik.petrin@pm.me>
