This PR fixes an issue that may sporadically trigger ASAN to got into a
deadlock when running a subprocess through the `IO.Process.spawn`
framework.
The general issue here is that we run `fork()` and then perform an
allocation in the child before going to `execvp` (for allocating the
arguments to `execvp`). As it turns out, doing this can cause a race
condition in ASAN that ultimately causes a deadlock in the child. This
was fixed upstream but then rolled back (see
https://github.com/google/sanitizers/issues/774). Thus, we must avoid
allocating any memory in between `fork` and `execvp`.
This PR fixes the verso hint that appears when using `sorry` in an
example block. It previously said: `` The `+error` flag indicates that
warnings are expected: +warning `` This PR replaces `error` with
`warning`. Fixes#12064
This PR revives the ability to specify modules in dependencies via the
basic `+mod` target key.
Implementation-wise, this removes deprecation of `BuildKey.module` and
once again uses it for `+mod` target keys. It also adds a test for
depending on a module of a dependency via `needs`.
This PR fixes the `lake query` output for targets which produce an
`Array` or `List` of a value with a custom `QueryText` or `QueryJson`
instance (e.g., `deps` and `transDeps`).
The most important change is that all bench scripts now must always
output to `measurements.jsonl` instead of being allowed to output
results on stdout/err.
This PR implements iteration over ranges for `Fin` and `Char`.
To this end, we introduce machinery for pulling back lawfulness of
`UpwardEnumerable` along an injective map and study the function
`Char.ordinal : Char -> Fin Char.numCodePoints`.
This PR fixes two Lake cache issues: a bug where a failed upload would
not produce an error and a mistake in the `--wfail` checks of the cache
commands.
This PR adds a comparison between `MetaM` and `SymM` for a benchmark was
proposed during the Lean@Google Hackathon.
### Benchmark description
In this benchmark, we define the semantics of a very simple imperative
language using an inductive predicate
```
Exec prog events mem lctx post
```
The predicate holds if, when executing the program `prog` with an
initial list of events `events`, memory `mem`, and local context `lctx`,
the postcondition `post` holds.
We then consider the following program:
```
input b
a := b
a := a + a
a := a - b
...
a := a + a
a := a - b
```
That is, after reading an input value `b`, the program repeatedly
updates the variable `a` by doubling it and then subtracting `b`.
We prove that, for any initial memory `m` and local context `l`, and
starting from the empty list of events, the following postcondition
holds:
```
fun t' m' l' =>
m' = m ∧ -- memory did not change
∃ v : Word,
t' = [IOEvent.IN v] ∧ -- exactly one input event
l'.get "a" = some v -- `a` contains the input value
```
In other words, executing the program produces exactly one input event,
leaves the memory unchanged, and ensures that the final value of `a` is
equal to the input value.
### Symbolic simulation benchmark (problem size `n`, with `2·n + 2`
instructions)
| Problem size (n) | MetaM time (ms) | MetaM kernel (ms) | SymM time
(ms) | SymM kernel (ms) | Total speedup |
|------------------|------------------|-------------------|----------------|------------------|---------------|
| 10 | 94.83 | 6.60 | 7.04 | 6.18 | ~13.5× |
| 20 | 218.92 | 13.33 | 14.15 | 13.02 | ~15.5× |
| 30 | 375.10 | 22.95 | 26.51 | 19.81 | ~14.2× |
| 40 | 563.82 | 34.99 | 40.42 | 29.55 | ~14.0× |
| 50 | 815.89 | 53.78 | 60.84 | 42.25 | ~13.4× |
| 60 | 1081.09 | 73.46 | 80.99 | 53.52 | ~13.3× |
| 70 | 1400.80 | 102.70 | 106.02 | 68.61 | ~13.2× |
| 80 | 1772.19 | 126.65 | 134.23 | 87.64 | ~13.2× |
| 90 | 2203.41 | 161.68 | 168.26 | 115.52 | ~13.1× |
| 100 | 2474.09 | 191.23 | 209.13 | 143.86 | ~11.8× |
<img width="580" height="455" alt="image"
src="https://github.com/user-attachments/assets/bc7058fa-e71a-4c2c-be28-860f39166965"
/>
### Symbolic simulation with extra simplification (SymM)
Problem size `n` corresponds to a program with `2·n + 2` instructions.
| n | Total time (ms) | Kernel time (ms) | Non-kernel time (ms) |
|-----|------------------|------------------|----------------------|
| 10 | 6.33 | 3.97 | 2.36 |
| 20 | 10.30 | 5.59 | 4.71 |
| 30 | 13.72 | 7.38 | 6.34 |
| 40 | 17.85 | 8.84 | 9.01 |
| 50 | 21.90 | 10.63 | 11.27 |
| 60 | 27.00 | 12.56 | 14.44 |
| 70 | 32.02 | 14.04 | 17.98 |
| 80 | 37.25 | 15.76 | 21.49 |
| 90 | 42.55 | 17.95 | 24.60 |
| 100 | 49.30 | 20.03 | 29.27 |
| 200 | 125.56 | 38.21 | 87.36 |
| 300 | 293.58 | 66.79 | 226.79 |
| 400 | 361.87 | 78.96 | 282.91 |
| 500 | 518.51 | 102.51 | 416.00 |
| 600 | 716.63 | 122.81 | 593.82 |
This PR fixes a bug where a `lake build --no-build` would exit with code
`3` if the optional job to fetch a GitHub or Reservoir release for a
package failed (even if nothing else needed rebuilding).
This PR fixes the procedure for finding the mangled symbol name of boxed
variants of native functions. Previously, the wrong symbol name has been
used for names ending in `_`: For example `test_` mangles to `l_test__`
but `test_._boxed` mangles to `l_test___00__boxed`, not
`l_test_____boxed` which the compiler would previously wrongly use.
This probably didn't affect anybody though since the failure condition
is pretty rare: the name of a native function that the interpreter tries
to execute would've had to end in `_`.
This PR adds the debugging helper functions `Expr.checkMaxShared` and
`MVarId.checkMaxShared` to `Sym`, and fixes a bug when visiting
telescopes in `Sym.simp`.
This PR adds additional debugging information to a run of `lake build
--no-build` via a `.nobuild` trace file. When a build fails due to
needing a rebuild, Lake emits the new expected trace next as `.nobuild`
file next to the build's old `.trace`. The inputs recorded in these
files can then be compared to debug what caused the mismatch.
To help keep the build directory clean, the `.nobuild` trace file is
removed on the next successful build.
This PR makes the automatic first token detection in tactic docs much
more robust, in addition to making it work in modules and other contexts
where builtin tactics are not in the environment. It also adds the
ability to override the tactic's first token as the user-visible name.
Previously, first token detection would look up the parser descriptor in
the environment and process its syntax. This would be incorrect for
builtin parsers, as well as for modules in which the definition is not
loaded. Now, it instead consults the Pratt parsing table for the
`tactic` syntax category. Tests are added that ensure this keeps working
in modules, and also that the first token of all tactics that ship with
Lean are either detected unambiguously or annotated to remove ambiguity.
Closes#12038.
This PR fixes a bug where the unknown identifier code actions were
broken in NeoVim due to the language server not properly setting the
`data?` field for all code action items that it yields.
This PR adds support for offset terms in `SymM`. This is essential for
handling equational theorems for functions that pattern match on natural
numbers in `Sym.simp`. Without this, it cannot handle simple examples
such as
```lean
def pw (n : Nat) : Nat :=
match n with
| 0 => 1
| n+1 => 2 * pw n
example : pw 4 = 16 := by
sym_simp [pw.eq_1, pw.eq_2]
example : pw (a + 2) = 2 * (2 * pw a) := by
sym_simp [pw.eq_2]
```
This PR adds `lake shake` as a built-in Lake command, moving the shake
functionality from `script/Shake.lean` into the Lake CLI.
## Motivation
Per discussion with @Kha and @tydeu, having shake as a top-level Lake
command is preferable to `lake exe shake` because:
- Avoids the awkwardness of accessing core tools via `lake exe`
- Compiles shake into the Lake binary, avoiding lakefile issues
- No benefit to lazy compilation on user machines for this tool
## Changes
- Move shake logic from `script/Shake.lean` to
`src/lake/Lake/CLI/Shake.lean`
- Add `lake shake` command dispatch in `Lake/CLI/Main.lean`
- Add help text in `Lake/CLI/Help.lean`
- Remove the standalone shake executable from `script/lakefile.toml`
## Usage
```
lake shake [OPTIONS] [<MODULE>...]
```
See `lake shake --help` for full documentation.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude <noreply@anthropic.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
