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>
This PR changes `lake cache get` and `lake cache put` to transfer
artifacts in parallel (using `curl --parallel`) when uploading or
eagerly downloading artifacts. Transfers are still recorded one-by-one
in the output -- no progress meter yet.
This PR removes the obsolete `Lean.Environment.replay` from
`src/Lean/Replay.lean` and replaces it with the improved version from
`src/LeanChecker/Replay.lean`, which includes fixes for duplicate
theorem handling and Quot/Eq dependency ordering. The primed names
(`Replay'`, `replay'`) are renamed back to `Replay` and `replay`.
A test for the original issue (nested inductives failing with `replay`)
is added as `tests/elab/issue12819.lean`.
Closes#12819🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `sym =>` tactic that enters an interactive symbolic
simulation
mode built on `grind`. Unlike `grind =>`, it does not eagerly introduce
hypotheses or apply by-contradiction, giving users explicit control over
`intro`, `apply`, and `internalize` steps.
New tactics available in `sym =>` mode:
- `intro` / `intros`: introduce binders and internalize into the E-graph
by
default. Use `intro~` or `intro (internalize := false)` to skip
internalization.
- `apply t`: apply backward rules with caching for `repeat`.
- `internalize` / `internalize_all`: internalize hypotheses into the
E-graph.
- `by_contra`: apply proof by contradiction, negating the target.
Satellite solvers (`lia`, `ring`, `linarith`) automatically introduce
remaining
binders and apply by-contradiction in `sym =>` mode, matching their
behavior in
default tactic mode. All existing `grind =>` tactics (`finish`,
`instantiate`,
`cases`, etc.) also work in `sym =>` mode. The sym-specific tactics are
guarded
and rejected in regular `grind =>` mode.
```lean
example (x : Nat) : myP x → myQ x := by
sym [myP_myQ] =>
intro h
finish
example (x y z : Nat) : x > 1 → x + y + z > 0 := by
sym =>
lia
```
This PR fixes an issue where `realizeConst` would generate auxiliary
declarations
(like `_sparseCasesOn`) using the original defining module's private
name prefix
rather than the realizing module's prefix. When two modules
independently realized
the same imported constant, they produced identically-named auxiliary
declarations,
causing "environment already contains" errors on diamond import.
The fix re-privatizes the constant name under the current module before
passing it
to `withDeclNameForAuxNaming`, ensuring each realizing module generates
distinctly
named auxiliary declarations.
Fixes#12825
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes a build failure on macOS introduced by #12540. macOS BSD
`ar` does not support the `@file` response file syntax that #12540
enabled unconditionally. On macOS, when building core (i.e., `bootsrap
:= true`), `recBuildStatic` now uses `libtool -static -filelist`, which
handles long argument lists natively.
Includes a `stage0/src/stdlib_flags.h` trigger so CI will automatically
run `update-stage0` after merge.
🤖 Prepared with Claude Code
Implementation adjusted by @tydeu
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR fixes a regression introduced in Lean 4.29.0-rc2 where `simp` no
longer simplifies inside type class instance arguments due to the
`backward.isDefEq.respectTransparency` change. This breaks proofs where
a term like `(a :: l).length` appears both in the main expression and
inside implicit instance arguments (e.g., determining a `BitVec` width).
**The problem:** After `simp only [List.length_cons]`, the main
expression has `l.length + 1` but instances still have `(a ::
l).length`. Since `simp` no longer simplifies inside instances, and
`isDefEq` won't unfold `List.length` at the default transparency,
subsequent lemma applications fail.
**Reproducer** (from Son Ho, reported by Sebastian Ullrich):
```lean
theorem BitVec.getElem!_eq_testBit_toNat {w : Nat} (x : BitVec w) (i : Nat) :
x[i]! = x.toNat.testBit i := by sorry
example (l : List Nat) (a : Nat) (j : Nat) :
(0#((a :: l).length))[j]! = (0#((a :: l).length)).toNat.testBit j := by
simp only [List.length_cons]
simp only [BitVec.getElem!_eq_testBit_toNat] -- works in 4.28.0-rc1, fails in 4.29.0-rc6
```
**The fix:** Mark `List.length` as `@[implicit_reducible]`, allowing
`isDefEq` to unfold it when checking implicit arguments. Several proofs
that previously needed a trailing `rfl` after `simp` now close directly,
since `simp` can see through `List.length` in more positions.
**Longer term:** The root cause is that `GetElem` carries complex proof
obligations in its type class instances, making implicit arguments
sensitive to definitional equality of collection sizes. We are
considering a redesign with a noncomputable `GetElemV` variant based on
`Nonempty` that avoids these casts entirely, but that is a larger change
planned for a future release.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds simp lemmas equating kernel-friendly function names with
their operator notation equivalents: `Nat.land_eq`, `Nat.lor_eq`,
`Nat.xor_eq`, `Nat.shiftLeft_eq'`, `Nat.shiftRight_eq'`, and
`Bool.rec_eq`. These are useful when proofs involve reflection and need
to simplify kernel-reduced terms back to operator notation.
Closes#12716
Co-authored-by: Claude <noreply@anthropic.com>
This PR changes the Lake `CacheMap` data structure to track the
platform-dependence of outputs. Platform-independent packages will no
longer include platform-dependent mappings in the output files produced
by `lake build -o`.
This PR ensures that when a function is marked `export` its borrow
annotations (if present) are always ignored.
This was the previous behavior in the C++ version of this file but
slightly modified when porting to the old IR and thus subsequently
ported to LCNF wrongly as well.
This PR moves `RequestCancellationToken` from `IO.Ref` to
`IO.CancelToken`.
They consist of the same data, but the constructor of `CancelToken` is
private. Hence there is no way to take the `Ref` in a
`RequestCancellationToken` and turn it into a `CancelToken`. This in
turn means that we can't set `Core.Context.cancelTk?` to be the one in
`RequestContext` when launching `CoreM` tasks in request handlers.
This PR fixes some process signals that were incorrectly numbered.
From what I can tell, the code used signals and signal numbers for
Alpha/SPARC, not x86/ARM. The test was also broken and always green,
hiding the mistake.
This PR changes the interaction between `@[cbv_opaque]` and
`@[cbv_eval]`
attributes in the `cbv` tactic. Previously, `@[cbv_opaque]` completely
blocked
all reduction including `@[cbv_eval]` rewrite rules. Now, `@[cbv_eval]`
rules
can fire on `@[cbv_opaque]` constants, allowing users to provide custom
rewrite
rules without exposing the full definition. Equation theorems, unfold
theorems,
and kernel reduction remain suppressed for opaque constants.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR introduces the `Headers` data type, that provides a good and
convenient abstraction for parsing, querying, and encoding HTTP/1.1
headers.
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 fixes a segfault when running `idbgClientLoop`. `@[extern]`
expects that the function doesn't include erased arguments in the
signature; however, `@[export]` exports the function with all arguments,
including erased ones. This causes a function signature mismatch between
`idbgClientLoopImpl` and `idbgClientLoop`, causing segfaults. However,
instead of solving the deeper problem that `@[extern]` - `@[export]`
pairs can cause such problems, this PR removes the erased arguments from
`idbgClientLoopImpl` and replaces occurrences of `α` with `NonScalar`.
This PR extends Lake's use of response files (`@file`) from Windows-only
to all platforms, avoiding `ARG_MAX` limits when invoking `clang`/`ar`
with many object files.
Lake already uses response files on Windows to avoid exceeding CLI
length limits. On macOS and Linux, linking Mathlib's ~15,000 object
files into a shared library can exceed macOS's `ARG_MAX` (262,144
bytes). Both `clang` and `gcc` support `@file` response files on all
platforms, so this is safe to enable unconditionally.
Reported as a macOS issue at
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/The.20clang.20command.20line.20with.20all.20~15.2C000.20Mathlib.20.2Ec.2Eo.2Eexport/near/574369912:
the Mathlib cache ships Linux `.so` shared libs but not macOS `.dylib`
files, so `precompileModules` on macOS triggers a full re-link that
exceeds `ARG_MAX`.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds the `fixedToolchain` Lake package configuration option.
Setting this to `true` informs Lake that the package is only expected to
function on a single toolchain (like Mathlib). This causes Lake's
toolchain update procedure to prioritize its toolchain and avoids the
need to separate input-to-output mappings for the package by toolchain
version in the Lake cache.
The tests need to run with certain environment variables set that only
cmake really knows and that differ between stages. Cmake could just set
the variables directly when running the tests and benchmarks, but that
would leave no good way to manually run a single benchmark. So cmake
generates some stage-specific scripts instead that set the required
environment variables.
Previously, those scripts were sourced directly by the individual
`run_*` scripts, so the env scripts of different stages would overwrite
each other. This PR changes the setup so they can instead be generated
next to each other. This also simplifies the `run_*` scripts themselves
a bit, and makes `tests/bench/build` less of a hack.
