Is lean installed properly installed?

Stream: new members

[Victor Miller]

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

[Bryan Gin-ge Chen]

Did you install leanproject and run leanproject get tutorials?

[Bryan Gin-ge Chen]

Oh wait, you said you installed Lean via brew.

[Bryan Gin-ge Chen]

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.

[Victor Miller]

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.

[Bryan Gin-ge Chen]

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

[Julian Berman]

What is type -a lean?

[Victor Miller]

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.

[Bryan Gin-ge Chen]

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.

[Rob Lewis]

What is the output of these three commands?

which elan
which lean
lean --version

[Victor Miller]

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)

[Victor Miller]

And I opened the tutorials directory in VS Code

[Bryan Gin-ge Chen]

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

[Victor Miller]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Victor Miller]

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)

[Kevin Buzzard]

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

[Victor Miller]

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.

[Kevin Buzzard]

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

[Victor Miller]

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.

[Kevin Buzzard]

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.

[Victor Miller]

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?

[Patrick Massot]

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.

[Victor Miller]

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