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	950a2b7896	chore: ensure every pkg/ test has a correct lean-toolchain file (#11782 )	2025-12-23 17:17:22 +00:00
Kim Morrison	c7652413db	feat: link docstrings for diamond inheritance (#11122 ) This PR fixes a problem for structures with diamond inheritance: rather than copying doc-strings (which are not available unless `.server.olean` is loaded), we link to them. Adds tests.	2025-11-10 01:05:01 +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

950a2b7896

chore: ensure every pkg/ test has a correct lean-toolchain file (#11782 )

2025-12-23 17:17:22 +00:00

Kim Morrison

c7652413db

feat: link docstrings for diamond inheritance (#11122 )

This PR fixes a problem for structures with diamond inheritance: rather
than copying doc-strings (which are not available unless `.server.olean`
is loaded), we link to them. Adds tests.

2025-11-10 01:05:01 +00:00

3 commits