Jannis Limperg (Dec 03 2022 at 16:09):
My weekend project: a little script (written in Lean 4 of course) that cleans up unused toolchains in your
.elan directory. It detects used toolchains by looking for
lean-toolchain files below your home directory (excluding directories starting with
.), then deletes any toolchain not mentioned in a
At the moment there are very few bells and whistles (e.g. you can't customise where it looks for
lean-toolchain files), but maybe someone finds it useful nonetheless.
Matej Penciak (Dec 03 2022 at 19:37):
Works great! Thanks!
Last updated: Aug 03 2023 at 10:10 UTC