MIL.Common

Stream: new members

[The Scrungly]

Hello, Im trying to run the tutorial file in VS code, but it needs to download MIL.Common. ive been downloading it for about two hours, and im only halfway done. is that normal?

[Jireh Loreaux]

You're downloading MIL.Common? Or you are building it?

[The Scrungly]

Building it. It started automatically when i opened the file

[Jireh Loreaux]

Right, that's the issue. You'll want to stop the build (killall lean in your terminal should suffice), then run lake exe cache get! (the ! is in case any cached files are corrupted, you don't need to always add that).

[Jireh Loreaux]

After you get the cache, then you'll be able to build the remaining files in MIL much more quickly.

[The Scrungly]

Thank you, but the terminal is saying killall is not recognized as an internal or external command

[The Scrungly]

nevermind, I used taskkill instead and it worked

[Michael Rothgang]

(Often, just closing all open tabs in your VS Code instance also works... but killall and friends make really sure no Lean processes are still running.)