【Lean】VSCode拡張が動かないトラブルの解決

Leanという定理証明支援系 & プログラミング言語には、
Mathlibという数学の定理などが詰め込まれたライブラリがあります。

そしてまた、Microsoft VSCodeには、Leanコードをリアルタイムにコンパイルして結果を出力する拡張があります。

定理証明支援系とは、証明として書かれたプログラムをコンパイルしてその正しさを検証する仕組みですので、
リアルタイムにコンパイルできると、とても使いやすいのです。

しかし、先日、VSCodeの拡張で、Mathlibをインポートすると、「Mathlibがコンパイルできず、VSCode拡張が正常に動作しない」という事態に陥ってしまいました。

原因と解決法は下記の通りで、
① パスを通しているLeanのバージョンが古い(v.4,0.0だった => v4.20.0)
② lakefile.leanのmathlibバージョンが新しすぎる ( v.4.21.0-rc3? => v.4.20.0)
で鬼のように長いMathlibのビルドを終えて、動きました！(丸一日コンパイルしました)

ちなみに、Windowsで使っています。

誰かのお役に立てば…