elan icon indicating copy to clipboard operation
elan copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Reuse already downloaded toolchain

Open iacore opened this issue 2 years ago • 0 comments

Currently, lake/leanpkg doesn't reuse toolchain versions.

How to reproduce

  1. elan default leanprover/lean4:nightly
  2. lake init foo which produce lean-toolchain with 4.0.0-nightly-2022-07-19 (which is the same version already installed)
  3. lake build It's downloading the same nightly version again

iacore avatar Jul 19 '22 13:07 iacore