Garmelon
6a2a884372
chore: migrate pkg tests ( #12889 )
...
Also refactor util.sh in the process, so test scripts become easier to
write (inspired in part by lake's test suite).
2026-03-11 18:55:46 +00:00
Marc Huisinga
168c125cf5
chore: relative lean-toolchains ( #12652 )
...
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>
2026-02-25 10:23:35 +00:00
Sebastian Ullrich
d4a5a2c632
fix: local syntax should create private definitions
2025-08-19 14:49:12 -07:00
Sebastian Ullrich
e28569f2a1
perf: minimize exported codegen data ( #9356 )
...
To be documented
2025-07-22 09:05:49 +00:00
Leonardo de Moura
8d2adf521d
feat: allow duplicate theorems to be imported
2024-03-13 12:57:41 -07:00
tydeu
4ec3d78afa
chore: update tests to account for .lake
2023-11-13 20:31:24 -05:00
Leonardo de Moura
7bd005bbbe
test: add test for local macro in auto tactic
2023-01-04 09:01:02 -08:00
Leonardo de Moura
2b67da2854
fix: fixes #2000
...
We now add the macro scope to local syntax declarations.
2023-01-03 15:28:10 -08:00
Mario Carneiro
583e023314
chore: snake-case attributes (part 2)
2022-10-19 09:28:08 -07:00
Leonardo de Moura
1fb112f84b
test: Environment.addExtraName
2022-09-21 15:03:11 -07:00
