Error when creating a new mathlib project

Stream: new members

[Luiz Kazuo Takei]

I tried to create a new Mathlib project (in VS Code, I clicked on the ∀ symbol and selected "New Project"). It started creating things and the last few lines showed this:

✔ [20/21] Built Cache.Main:c.o (4.8s)
✔ [21/21] Built cache:exe (21s)
uncaught exception: no such file or directory (error code: 2)
error: mathlib: failed to fetch cache
=> Operation failed. Exit code: 1.

Could someone help me fix this?

[Kevin Buzzard]

Are you behind a firewall? If you're on Windows try switching off your antivirus.

[Luiz Kazuo Takei]

Thanks for the quick reply!

I am on Windows but it's my college's computer so I don't have the option to turn off antivirus. :(

Is there any other way around this? Could I create my project using some online Lean thingy and download the project later? (When I clone a git repository containing a Mathlib project, it works fine.)

[Kenny Lau]

yeah i think there are instructions to use command line to set up a new lean project that depends on mathlib

[Kevin Buzzard]

You can try

$ lake new <name_of_project> math
$ cd <name_of_project>
$ lake exe cache get

and then try changing <name_of_project>/<name_of_project>.lean to something like

import Mathlib.Data.Real.Basic

#check Real

[Luiz Kazuo Takei]

Thank you very much @Kevin Buzzard but it gave me a similar (same?) error message:

info: Cli: checking out revision 'b62fd39acc32da6fb8bb160c82d1bbc3cb3c186e'
info: mathlib: running post-update hooks
uncaught exception: no such file or directory (error code: 2)
error: mathlib: failed to fetch cache

I am trying something else. I created a new Mathlib project using Github Codespaces and inserted the code you suggested

import Mathlib.Data.Real.Basic

#check Real

Now I just cloned the repository on my computer and opened the project using VS Code.

I am now waiting for my computer (super slow) to import the things from Mathlib. It seems like this will work.

[Luiz Kazuo Takei]

A million years later... :sweat_smile:

Yes, it finished importing all the stuff (I am not sure exactly what, a bunch of Mathlib stuff) and now it works!

Thanks again!

[Aaron Liu]

Luiz Kazuo Takei said:

A million years later... :sweat_smile:

Yes, it finished importing all the stuff (I am not sure exactly what, a bunch of Mathlib stuff) and now it works!

Thanks again!

Sounds like you were building part of mathlib