プロジェクトディレクトリ内で elan show すると、そのプロジェクトのツールチェーンがダウンロードしてないと即座にダウンロードをはじめる。困ったもんだ。
elan toolchain list を使うべし!
lake build しても必要ならダウンロードして、elanツールチェーンリストに追加する。
VSCodeも、Leanプロジェクトの.leanファイルを開いた時点で、elanによるツールチェーンのインストールとlakeによるビルドを始める。が、ビルドはなかなかうまくいかない。
プロジェクトディレクトリ内で elan show すると、そのプロジェクトのツールチェーンがダウンロードしてないと即座にダウンロードをはじめる。困ったもんだ。
elan toolchain list を使うべし!
lake build しても必要ならダウンロードして、elanツールチェーンリストに追加する。
VSCodeも、Leanプロジェクトの.leanファイルを開いた時点で、elanによるツールチェーンのインストールとlakeによるビルドを始める。が、ビルドはなかなかうまくいかない。