This PR fixes an issue where `beforeElaboration` attributes were not
being run on `inductive`/`structure`/`coinductive` commands. Closes
#13433.
There is also light refactoring of MutualInductive, as well as a mild
performance enhancement to avoid repeated re-elaboration of `variable`s.
This PR makes the elaborator reject `@[foo]` when the module that
registers `foo` is not visibly imported into the current file but merely
loaded as IR. Previously such uses silently elaborated but led to
divergence of cmdline and server behavior and caused `lake shake --fix`
to flip-flop on successive runs (#13599).
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.
This PR changes all `lean-toolchain` to use relative toolchain paths
instead of `lean4` and `lean4-stage0` identifiers, which removes the
need for manually linking toolchains via Elan.
After this PR, at least Elan 4.2.0 and 0.0.224 of the Lean VS Code
extension will be needed to edit core.
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR extends shake with tracking of attribute names passed to
`simp`/`grind`.
On the way there, it also fixes `register_simp/grind_attr` uses outside
`public meta section` as well as go-to-definition on declaration-level
uses of the created attributes (tactic-level goto would be a separate
todo).
This PR implements support for user-defined attributes at
`grind_pattern`. Suppose we have declared the `grind` attribute
```lean
register_grind_attr my_grind
```
Then, we can now write
```lean
opaque f : Nat → Nat
opaque g : Nat → Nat
axiom fg : g (f x) = x
grind_pattern [my_grind] fg => g (f x)
```
This PR implements user-defined `grind` attributes. They are useful for
users that want to implement tactics using the `grind` infrastructure
(e.g., `progress*` in Aeneas). New `grind` attributes are declared using
the command
```lean
register_grind_attr my_grind
```
The command is similar to `register_simp_attr`. After the new attribute
is declared. Recall that similar to `register_simp_attr`, the new
attribute cannot be used in the same file it is declared.
```lean
opaque f : Nat → Nat
opaque g : Nat → Nat
@[my_grind] theorem fax : f (f x) = f x := sorry
example theorem fax2 : f (f (f x)) = f x := by
fail_if_success grind
grind [my_grind]
```
TODO: remove leftovers after update stage0
