getting mathlib cache on windows

Stream: new members

[Jeremy Avigad]

I am with a student who is trying to use mathlib with Windows. leanproject get somehow fails to get the mathlib cache, and leanproject get-mathlib-cache does nothing: the prompt returns in about a second, with no error messages, but the cache has not been fetched.

Does this sound familiar? Any thoughts about how to debug?

[Jeremy Avigad]

Never mind! The student reinstalled mathlibtools, and now it seems to work.