- Revamp toolchain resolution and storage
- Toolchain references are now always resolved to a fixed
<owner>/<repo>:<version>
format before downloading, resolving the issue of having the same toolchain installed as e.g.stable
,v4.9.0
, andleanprover/lean4:v4.9.0
and ensuring that e.g.stable
has the same meaning for everyone at a given point in time. - Accordingly,
elan update
has been removed as updates of non-fixed toolchains are now implicit. - This also fixes
lake +stable new ...
putting an unadvisableleanprover/lean4:stable
reference inlean-toolchain
. - The configured default toolchain name is stored unresolved (and not immediately installed) but
is resolved before every use. This also means that passing
--default-toolchain none
to the elan install script is not necessary anymore to speed up installation. - In case of a network error resolving a toolchain, elan falls back to the previous resolution if any and prints a warning.
- The
update-hashes/
directory is not used anymore, deletingtoolchains/
or direct subdirectories does not break elan anymore.
- Toolchain references are now always resolved to a fixed
- More useful download and installation info messages
- Experimental
elan toolchain gc
command. Seeelan toolchain gc --help
for documentation.lean-toolchain
files will only be known to the GC after being used at least once with this version of elan.
- Fix update check
- Fix partial toolchains potentially being left in place when unpacking is aborted (#121)
- Check for elan updates during toolchain downloads (#122)
- Default to stable toolchain again in time for first Lean 4 stable release (#104)
- Fix download progress display on Windows (#101)
-
Support toolchain reference
<origin>:lean-toolchain
that refers to the toolchain referred to by the contents of the given GitHub file (#99) -
Default to Lean 4 (#98)
- Avoid dependency on the VC++ Redistributable on Windows (#97)
- Fix self update on Apple Silicon (only?) (#78)
- Update dependencies
- Avoid setting
(DY)LD_LIBRARY_PATH
(#90)
- Fix downloading Lean releases again
- Actual support for ARM64 macOS (M1)
- Support for ARM64 macOS (M1)
- Update dependencies
- Support for zstd-compressed tarballs
- Support for ARM64 Linux
- Remove another "press any key to exit"
- Remove "press any key to exit" step from Windows installation not needed for VS Code or PowerShell method
- Add
lake
Lean 4 executable
- Fix
elan self update
on not-Linux, again
- Default to respective toolchain inside of
~/.elan
(#36)
- Fix
elan self update
on not-Linux and build from cmdline
- Run extension-less tools such as
leanc
usingsh
on Windows (and hope for the best...)
- Update suggestion when no default toolchain is configured (#31)
- Fix
elan show
when no default toolchain is configured (#33)
- Fix
elan self update
download URL on Linux
- Fix installation from non-default repos
- Fix updating channels from non-default repos (e.g.
leanprover/lean4:nightly
) This change affects the store location of such toolchains, so you will have to re-install them first.$ elan toolchain uninstall leanprover-lean4-nightly $ elan toolchain install leanprover/lean4:nightly
- Move to
leanprover/elan
- Make
elan
a static executable on Linux - Improve
leanpkg.toml
error handling (#26) - Make downloaded files read-only (on Linux/macOS) (#27)
- Hopefully fix Lean 4 leanpkg on Windows
- Hopefully actually restore
elan toolchain link
functionality
- Hopefully restore
elan toolchain link
functionality
- Accept (almost) arbitrary release tag names in addition to version numbers
- Add
leanc
,leanmake
Lean 4 executables
- stable/nightly now refer to leanprover-community, Lean's community fork. This includes the toolchain installed by default (stable).
- Fix release lookup once more with feeling
- Fix self-update always triggering
- Fix lookup of latest Github release of both Lean and elan
- Fix name check in
elan toolchain link
(#17)
- elan will now warn if there are other Lean installations in the PATH before installing
- Fix mtimes not being restored from installation archives
- Fix invoking leanpkg on Windows
- Version specifiers can now point to custom forks of Lean, such as
khoek/klean:3.4.1
(#8)
- An explicit version passed to a proxy command like in
leanpkg +nightly build
will now be installed automatically when necessary - Full toolchain names and their directories do not mention the operating system (the "target triple", to be exact) any more. You may want to delete your old toolchains from
~/.elan/toolchains
to save space.
leanpkg.toml
andlean-toolchain
files can now reference custom toolchains (those added byelan toolchain link
)
leanchecker
proxy
curl | sh
installation and instructions
- Fix
elan toolchain link
(#1) - Fix self-update
- De-rustify docs
Minimum viable product release
- Building on Rustup's code, implement installing and managing Lean toolchains
- Have leanpkg.toml files override the Lean version