Zulip Chat Archive

Stream: new members

Topic: Trouble Installing Mathlib


view this post on Zulip 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!

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:33):

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

view this post on Zulip Johan Commelin (Feb 12 2020 at 20:34):

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

view this post on Zulip 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:)

view this post on Zulip 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"?

view this post on Zulip 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