elan show でダウンロードをはじめる

プロジェクトディレクトリ内で elan show すると、そのプロジェクトのツールチェーンがダウンロードしてないと即座にダウンロードをはじめる。困ったもんだ。

elan toolchain list を使うべし！

lake build しても必要ならダウンロードして、elanツールチェーンリストに追加する。

VSCodeも、Leanプロジェクトの.leanファイルを開いた時点で、elanによるツールチェーンのインストールとlakeによるビルドを始める。が、ビルドはなかなかうまくいかない。