Trouble Installing Mathlib

Stream: new members

[ROCKY KAMEN-RUBIO]

I'm having trouble getting mathlib to work. I make it through the installer ok, but I always get errors when I try to do things like open_locale classical. I've tried reinstalling mathlib several times, I'm doing it in the folder that has my lean package install and the src file, and have tried this on multiple projects. I've also tried restarting my editor, terminal, and computer. Any thoughts would be very much appreciated!

[Johan Commelin]

@ROCKY KAMEN-RUBIO Can you paste code that gives an error?

[Johan Commelin]

open_locale classical also sometimes gives me errors when it comes right after some import statements.

[Johan Commelin]

I think it can be fixed by writing something above it. (I usually put noncomputable theory :slight_smile:)

[Kevin Buzzard]

Are you using VS Code? Did you clone the example project? Did you remember to "open folder" and not "open file"?

[ROCKY KAMEN-RUBIO]

I was using VSCode , cloned a project from github that was working on a friend's computer, and was sure to "open folder" instead of "open file". I tried it again today without having changed anything and it seems to be working ok. I'll keep you all updated if it stops working again. Computers are mysterious creatures.