Stream: new members
Topic: Trouble Installing Mathlib
ROCKY KAMEN-RUBIO (Feb 12 2020 at 20:23):
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 (Feb 12 2020 at 20:33):
@ROCKY KAMEN-RUBIO Can you paste code that gives an error?
Johan Commelin (Feb 12 2020 at 20:34):
open_locale classical also sometimes gives me errors when it comes right after some
Johan Commelin (Feb 12 2020 at 20:35):
I think it can be fixed by writing something above it. (I usually put
noncomputable theory :slight_smile:)
Kevin Buzzard (Feb 12 2020 at 21:29):
Are you using VS Code? Did you clone the example project? Did you remember to "open folder" and not "open file"?
ROCKY KAMEN-RUBIO (Feb 14 2020 at 20:36):
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.
Last updated: May 10 2021 at 17:39 UTC