Zulip Chat Archive

Stream: new members

Topic: Is lean installed properly installed?


view this post on Zulip Victor Miller (Dec 28 2020 at 19:41):

I installed lean on my iMac running Big Sur using brew. I also installed Visual Studio. In looking at first_proofs.lean in vscode, when I hover over the first import I get the messages below. Obviously something is wrong. Any suggestions as to how to fix it?

invalid import: data.option.defs
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)Lean
invalid import: data.option.defs
invalid object declaration, environment already has an object named 'option.elim._main'Lean
invalid import: data.option.defs
invalid object declaration, environment already has an object named 'option.elim._main'Lean
invalid import: data.option.defs
invalid object declaration, environment already has an object named 'option.elim._main'Lean
invalid import: data.option.defs
invalid object declaration, environment already has an object named 'option.elim._main'Lean
invalid import: algebra.group.defs
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)Lean
invalid import: algebra.group.defs
invalid object declaration, environment already has an object named 'left_mul'Lean
invalid import: algebra.group.defs
invalid object declaration, environment already has an object named 'left_mul'Lean
invalid import: order.rel_classes
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)Lean
invalid import: order.lattice
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)Lean
invalid import: data.equiv.basic
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)Lean
invalid import: data.equiv.basic
invalid object declaration, environment already has an object named 'equiv'Lean
invalid import: data.equiv.basic
invalid object declaration, environment already has an object named 'equiv'Lean
invalid import: order.rel_classes
invalid object declaration, environment already has an object named 'is_refl.swap'Lean
invalid import: order.lattice
invalid object declaration, environment already has an object named 'le_antisymm''Lean
invalid import: data.equiv.basic
invalid object declaration, environment already has an object named 'equiv'Lean
invalid import: algebra.group.defs
invalid object declaration, environment already has an object named 'left_mul'Lean
invalid import: order.rel_classes
invalid object declaration, environment already has an object named 'is_refl.swap'Lean
invalid import: order.rel_classes
invalid object declaration, environment already has an object named 'is_refl.swap'Lean
invalid import: order.lattice
invalid object declaration, environment already has an object named 'le_antisymm''Lean
invalid import: data.equiv.encodable.basic
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)Lean
invalid import: data.equiv.basic
invalid object declaration, environment already has an object named 'equiv'Lean
invalid import: order.rel_classes
invalid object declaration, environment already has an object named 'is_refl.swap'Lean
invalid import: data.list.basic
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)Lean
invalid import: order.rel_classes
invalid object declaration, environment already has an object named 'is_refl.swap'Lean
invalid import: data.list.basic
invalid object declaration, environment already has an object named 'list.nil.is_left_id'Lean
invalid import: order.rel_classes
invalid object declaration, environment already has an object named 'is_refl.swap'Lean
invalid import: data.list.basic
invalid object declaration, environment already has an object named 'list.nil.is_left_id'Lean
invalid import: order.rel_classes
invalid object declaration, environment already has an object named 'is_refl.swap'Lean
invalid import: data.list.basic
invalid object declaration, environment already has an object named 'list.nil.is_left_id'Lean
invalid import: data.equiv.basic
invalid object declaration, environment already has an object named 'equiv'Lean
invalid import: data.equiv.basic
invalid object declaration, environment already has an object named 'equiv'Lean
invalid import: algebra.group.defs
invalid object declaration, environment already has an object named 'left_mul'Lean
invalid import: order.rel_classes
invalid object declaration, environment already has an object named 'is_refl.swap'Lean
invalid import: data.list.basic
invalid object declaration, environment already has an object named 'list.nil.is_left_id'Lean
invalid import: data.equiv.basic
invalid object declaration, environment already has an object named 'equiv'Lean
invalid import: order.rel_classes
invalid object declaration, environment already has an object named 'is_refl.swap'Lean
invalid import: data.list.basic
invalid object declaration, environment already has an object named 'list.nil.is_left_id'Lean
invalid import: order.rel_classes
invalid object declaration, environment already has an object named 'is_refl.swap'Lean
invalid import: data.list.basic
invalid object declaration, environment already has an object named 'list.nil.is_left_id'Lean
invalid import: data.equiv.basic
invalid object declaration, environment already has an object named 'equiv'Lean
invalid import: data.equiv.basic
invalid object declaration, environment already has an object named 'equiv'Lean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/order/conditionally_complete_lattice.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/data/nat/enat.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/tactic/norm_num.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/data/rat/cast.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/algebra/char_zero.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/data/fintype/basic.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/data/finset/basic.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/data/multiset/finset_ops.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/data/set/intervals/ord_connected.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/algebra/pointwise.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/algebra/module/basic.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/tactic/abel.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/data/set/finite.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/data/real/cau_seq.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/tactic/linarith/verification.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/tactic/linarith/elimination.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/tactic/linarith/datatypes.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/tactic/ring.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/tactic/linarith/parsing.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/tactic/linarith/preprocessing.lean' uses sorryLean
imported file '/Users/victorsmiller/Programming/Lean/tutorials/_target/deps/mathlib/src/algebra/star/basic.lean' uses sorryLean
Peek Problem (⌥F8)
No quick fixes available

view this post on Zulip Bryan Gin-ge Chen (Dec 28 2020 at 19:44):

Did you install leanproject and run leanproject get tutorials?

view this post on Zulip Bryan Gin-ge Chen (Dec 28 2020 at 19:44):

Oh wait, you said you installed Lean via brew.

view this post on Zulip Bryan Gin-ge Chen (Dec 28 2020 at 19:47):

Unfortunately, using homebrew to install Lean will make it difficult to work with Lean projects, and we haven't managed to fix this yet.

Please see the instructions on this page for our recommended way to install Lean and related tooling.

view this post on Zulip Victor Miller (Dec 28 2020 at 19:50):

When I run the script on the page you linked to, it says that it wants to install homebrew. I already have it installed. I don't want to mess up the current installation. I did try to uninstall lean from homebrew, and it said that it wasn't installed, so I must have installed it some other way.

view this post on Zulip Bryan Gin-ge Chen (Dec 28 2020 at 19:53):

It should be perfectly safe to run the homebrew installation script again, but if you're concerned you can just run the other commands in the script one by one: https://github.com/leanprover-community/mathlib-tools/blob/master/scripts/install_macos.sh

view this post on Zulip Julian Berman (Dec 28 2020 at 19:53):

What is type -a lean?

view this post on Zulip Victor Miller (Dec 28 2020 at 19:59):

I went through the commands one by one in the install_macos.sh script. All of the python packages are installed. Visual Studio Code is already installed. When I tried to install jroesch.lean it said that it's already installed. And I did intall leanproject and installed leanproject get tutorials.

view this post on Zulip Bryan Gin-ge Chen (Dec 28 2020 at 20:00):

Ah, did you open the tutorials directory in VS Code, or just the file 00_first_proofs.lean?

The extension requires that you open a directory containing a Lean project - opening individual Lean files will not work, as explained here.

Sorry, scratch that. If you had opened just the file then you most likely would be getting "not found" errors rather than out-of-memory errors.

view this post on Zulip Rob Lewis (Dec 28 2020 at 20:02):

What is the output of these three commands?

which elan
which lean
lean --version

view this post on Zulip Victor Miller (Dec 28 2020 at 20:24):

Victors-iMac:Lean victorsmiller$ which elan
/Users/victorsmiller/.elan/bin/elan
Victors-iMac:Lean victorsmiller$ which lean
/Users/victorsmiller/.elan/bin/lean
Victors-iMac:Lean victorsmiller$ lean --version
Lean (version 3.23.0, commit ed6accfb611b, Release)

view this post on Zulip Victor Miller (Dec 28 2020 at 20:25):

And I opened the tutorials directory in VS Code

view this post on Zulip Bryan Gin-ge Chen (Dec 28 2020 at 20:37):

What do you see if you navigate to the tutorials folder and run leanproject get-mathlib-cache?

view this post on Zulip Victor Miller (Dec 28 2020 at 20:46):

Victors-iMac:tutorials victorsmiller$ leanproject get-mathlib-cache
Looking for local mathlib oleans
Found local mathlib oleans

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 20:47):

All looks good so far. Can you compile? In the tutorials directory try lean --make src/solutions/00_first_proofs.lean

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 20:48):

It should finish very quickly (within a few seconds), with limited output.

view this post on Zulip Victor Miller (Dec 28 2020 at 20:49):

Victors-iMac:tutorials victorsmiller$ lean --make src/solutions/00_first_proofs.lean
/Users/victorsmiller/Programming/Lean/tutorials/src/solutions/00_first_proofs.le/Users/victorsmiller/Programming/Lean/tutorials/src/solutions/00_first_proofs.leupper_bounds : set ?M_1 → set ?M_1
/Users/victorsmiller/Programming/Lean/tutorials/src/solutions/00_first_proofs.le/Users/victorsmiller/Programming/Lean/tutorials/src/solutions/00_first_proofs.le/Users/victorsmiller/Programming/Lean/tutorials/src/solutions/00_first_proofs.le/Users/victorsmiller/Programming/Lean/tutorials/src/solutions/00_first_proofs.lean: le_limTry this: exact one_div_pos.mpr this
Try this: exact le_abs_self (u N - x)

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 20:50):

That looks great. Your system is working. Just start VS Code in the tutorials directory with code . and it should all work fine.

view this post on Zulip Victor Miller (Dec 28 2020 at 20:57):

Kevin, Thanks. So was the problem that I just started Visual Studio from , and then opened tutorials? I thought that Visual Studio was smart enough to cd to the right directory.

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 20:58):

I get the error you posted every now and again, and I just restart Lean and it goes away.

view this post on Zulip Victor Miller (Dec 28 2020 at 21:40):

Ok. Now I've started visual studio by doing code . in the lftcm2020 directory. However, whenever I hover over anything I just get the message "Parsing at line 1". I've tried restarting lean, but I get the same.

view this post on Zulip Kevin Buzzard (Dec 28 2020 at 21:55):

It sounds like this one isn't compiled. In the lftcm2020 directory try leanproject get-mathlib-cache and then try opening VS Code in that directory again when it's finished.

view this post on Zulip Victor Miller (Dec 28 2020 at 22:00):

More information. If I use code for the tutorials project, everything seems to be ok. For lftcm2020 I did the leanproject get-mathlib-cache and then opened it in VS Code Right now lean is running at 469% (my mac has 8 processors) and has been for a few minutes. It's now apparently finished, but I'm back to the "excessive memory" errors. Is there some configuration setting for lean and/or VS Code that I need to make?

view this post on Zulip Patrick Massot (Dec 28 2020 at 22:04):

You shouldn't have to do all that. I just tried :

  • leanproject get lftcm2020
  • code lftcm2020 and use the file explorer to open an exercise file and it just works perfectly.

view this post on Zulip Victor Miller (Dec 28 2020 at 22:04):

I took the sledgehammer approach. I did a rm -f -r lftcm2020 and the leanproject get lftcm2020. Things seem a bit better now.


Last updated: May 13 2021 at 18:26 UTC