leanpkg takes forever on Windows

Stream: general

[Kevin Buzzard]

I just typed leanpkg init on Windows, and it sat there for around a minute before saying "you meant leanpkg init name_of_package so please start again". I just typed leanpkg init my_package and in the time it took me to write this the Windows machine still hasn't finished mulling over this command. I've seen this several times before on Windows. What's going on?

[Mario Carneiro]

probably lean core files aren't compiled

[Kevin Buzzard]

They seem to be -- this was from the most recent nightly and there was a bunch of .olean files where there should be..

[Kevin Buzzard]

(I mean in lib with the .lean files)