lean4-htt

max/lean4-htt

Fork 0

Commit graph

Author	SHA1	Message	Date
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	c8cdb57c4b	feat: move non-essential metadata into .olean.server (#8068 ) This PR ensures that for modules opted into the experimental module system, we do not import module docstrings or declaration ranges. Excluding declaration docstrings as well would require some more work to make `[inherit_doc]` leave a mere reference to the other declaration instead of copying its docstring eagerly.	2025-04-24 08:12:26 +00:00

Author

SHA1

Message

Date

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

c8cdb57c4b

feat: move non-essential metadata into .olean.server (#8068 )

This PR ensures that for modules opted into the experimental module
system, we do not import module docstrings or declaration ranges.

Excluding declaration docstrings as well would require some more work to
make `[inherit_doc]` leave a mere reference to the other declaration
instead of copying its docstring eagerly.

2025-04-24 08:12:26 +00:00

2 commits