installation problems

Stream: new members

[Kevin Buzzard]

I have said before that I really just want one place to point to anyone who says "how do I install lean?" but doesn't tell me which OS they're on. I don't want to have to say "look at the bottom of this page"

[Kevin Buzzard]

I want a page which says "lean and mathlib tools installation instructions" in big letters at the top and then has three highly visible links for Mac, Windows, Linux and then all the nerdy stuff in small letters below

[Kevin Buzzard]

And then I link to this from everywhere until Google understands that this is what people want

[Kevin Buzzard]

Thorsten is no fool and the fact that we pointed him to a web page and then he unsurprisingly started reading it from the top in an indication that we're doing something wrong

[Damiano Testa]

To chime in, supporting Kevin's comments: I did not find installing Lean especially easy. I could download it, I followed the outlined steps, but I was never really sure that what I was doing was correct. Also, in the end, VSC did not just work, it still needed a little extra love. I cannot remember if it did not have a correct path or something. The final lingering feeling, is that installing Lean felt harder than installing Linux Mint on my computer.

[Scott Morrison]

Yeah, it's clear we're not there yet. That said --- an enormous amount of effort has already gone into making installation as painless as possible, all volunteer effort by people with many other things to do. This is an issue that has previously caused strife here, so please everyone let's be as nice as possible to each other while working on installation issues! (I'm not complaining about anything in the current conversation, just trying to keep things on track. :-)

[Scott Morrison]

I think two questions we should resolve soon, and act on, are:

[Scott Morrison]

Should we keep the "maybe a couple of nights" install options available? Or just jump straight to the regular install?

[Scott Morrison]

How should we bundle "Lean" in package managers?

1. not-at-all
2. under the name lean, but actually install elan
3. under the name elan
   (The other option, which is what we have at the moment in brew, but I think is worse than nothing, is to bundle a fixed version of lean under the name lean.)

[Damiano Testa]

Also, I want to point out that the difficulties in installing Lean were resolved in matters of seconds on the Zulip chat, thanks to the incredibly supportive community!

As for the installation, I do not know the difference between lean and elean, but I can say that I did not use the "couple of nights". For me, the actual options were:

1. using it on the web;
2. full install.

I do not know how other people might feel about this.

[Scott Morrison]

I've made a new thread at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/abandoning.20the.20.22trylean.22.20bundles.3F for discussion of "maybe a couple of nights".

[Scott Morrison]

And there's existing discussion of the brew issue at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Homebrew.20Tap

[Thorsten Altenkirch]

Thank you. I tried to reinstall lean using the script on
https://leanprover-community.github.io/install/macos.html
I did say "brew uninstall lean" before but I still get an error on

import tactic

namely

1:1: file 'tactic' not found in the search path

Maybe the problem is that the tools didn't get updated, at the end f the installation I got:

'mathlibtools' already seems to be installed. Not modifying existing installation in '/Users/psztxa/.local/pipx/venvs/mathlibtools'. Pass '--force' to force installation.

I get the following version form the command line:

lean --version
Lean (version 3.19.0, commit 67783e68a6a9, Release)

[Kenny Lau]

#backticks

[Kenny Lau]

@Patrick Massot looks like that script doesn't install mathlib?

[Kevin Buzzard]

The version of lean looks good though

[Thorsten Altenkirch]

So how do I install math lib? Thanks Kevin for pointing me to the community page ;-) but it seems the information there is buggy.

[Kenny Lau]

@Thorsten Altenkirch I apologize for the unclear install instructions. What you installed seems to be the core Lean library, which does not include the mathematical components (called mathlib). If you work on a new project / install an existing project, using leanproject, you'll get mathlib automatically. See https://leanprover-community.github.io/install/project.html

[Kevin Buzzard]

You have to open a lean project. You can't just edit a file -- imports don't work then

[Thorsten Altenkirch]

I don't want to start a "project" I just want to use lean with math lib, in particular I want to use the ring solver.

[Kevin Buzzard]

So make a new project with leanproject new my-project and make the file in there

[Kevin Buzzard]

And then open the project in VS code and with any luck it'll work fine

[Thorsten Altenkirch]

I am using emacs. Do I now have to use VS code?

[Thorsten Altenkirch]

I said:

leanproject new examples

in the directory where my file is but I still get an error. Maybe I have somehow to add the file to the "project"?

[Kevin Buzzard]

No, but you will have to make a project. It should work in emacs too.

[Kevin Buzzard]

The way it's set up is that each project contains its own version of mathlib

[Thorsten Altenkirch]

Ah hang on it actually created a new directory...

[Thorsten Altenkirch]

Hurray. It works. My file is now in a subdirectories of a subdirectory which I don't like but I can use the ring tactic. I would have preferred if I could have done this without creating a "project".

[Thorsten Altenkirch]

I mean I understand that it is a good idea that projects have their own copy of the lib but there should be a way to use the lib without starting a project.

[Kevin Buzzard]

There is no global installation of the mathlib library. The library changes at an alarming rate, with several PR's accepted per day, This is why I'm here -- I see fast progress.

[Kevin Buzzard]

see #rss

[Kevin Buzzard]

so the philosophy is that each project comes with its own mathlib,and occsaionally you update. Nothing is backwards compatible though, so updating mathlib can break stuff. We live on the edge.

[Patrick Massot]

Thorsten Altenkirch said:

So how do I install math lib? Thanks Kevin for pointing me to the community page ;-) but it seems the information there is buggy.

You mean the sentence "After this installation procedure, it is crucial to read how to start or get a Lean project. "? Should we add "even if you are Thorsten Altenkirch"?

[Patrick Massot]

Or did you follow the link but missed the sentences "This page describes the basic use of this tool, and should be sufficient for everyday use. If this is not enough for your purposes, you can read the full leanproject documentation."?

[Patrick Massot]

This full documentation includes https://leanprover-community.github.io/leanproject.html#global-mathlib-install explaining how to use mathlib outside of a project.

[Thorsten Altenkirch]

Hej hej no reason to be sarky. I went through a number of pages and didn't read everything as most people don't. In particular since I only wanted to experiment I didn't feel that I should find out how to start a "lean project".
I installed lean according to the description and then Kevin advised me to "import tactics" which didn't work. He said "you haven't installed it properly" and then I reinstalled it. Eventually people point out to me that I need to start a project. I have used proof assistants before and I never needed to "start a project" to use the standard library. Maybe the lean project global-install should be part of the installation script.

[Mario Carneiro]

The global install approach causes weird issues that newbies are not prepared to deal with

[Patrick Massot]

Many people are indeed eager to start playing instead of reading the instructions, this is very natural. The key trick when this doesn't work is to conceive the idea that maybe you did something wrong. After taking this crucial step, you can either go back to read more carefully or ask questions in a way suggesting you got the key trick. This happened countless times and leads to the slow improvement of the overall installation process, which will probably never ends since this kind of software will probably remain tricky to use forever.

[Bryan Gin-ge Chen]

Because mathlib is changing so rapidly, working outside of projects makes it quite inconvenient to share code. If you want to share a Lean file that depends on some version of mathlib, you have to also specify the Lean version and the precise commit of mathlib that it was developed with somehow, otherwise there's a decently high probability your code won't work. The leanpkg.toml file in a project makes that much easier, esp. with the leanproject tooling.

[Frédéric Dupuis]

I think it might be good to include a big warning against the global install in the installation instructions. My first instinct was also to do this when I started and of course it didn't work out too well!

[Jon Eugster]

Today when I opened VSCode it crashed immediately (probably memory overload) and from there on the lean extension didnt work, like I didnt see the infoview and nothing happened when opening a .lean file. Trying to restart lean resulted in the following error:

Command 'Lean: Restart' resulted in an error (command 'lean.restartServer' not found)

I didn't knowingly change anything on my computer since it worked to last time. Any ideas what that could be and how to investigate further?

[Alex J. Best]

Which version of lean are you trying to use 3/4. Do you have the plugin for that lean version (and only that version) activated in vscode. And are you opening a lean project folder in vscode rather than just a lean file?

[Jon Eugster]

Its Lean 3.4.2 on Ubuntu 20. And the VSCode extension is "lean" v0.16.45, so not the lean4 one.

And yes, I was opening the folder, for example running code . inside the leanproject folder

[Eric Rodriguez]

Lean 3.4.2 :shock: do you have elan installed?

[Jon Eugster]

yep, elan 0.10.3
Maybe I haven't updated lean in a while, that's at least the lean that is first in my path (which lean)

[Jon Eugster]

Is there a concise way to update everything to the most recent versions again?

[Eric Rodriguez]

what does elan show show?

[Julian Berman]

(Show us what type -a lean says too if you can.)

[Jon Eugster]

Updated now with elan update.

~$ elan show
installed toolchains
--------------------

stable (default)
leanprover-community-lean-3.26.0
leanprover-community-lean-3.30.0
leanprover-community-lean-3.38.0
3.4.2

active toolchain
----------------

stable (default)
Lean (version 3.39.1, commit 1781ded0d006, Release)

and

$ type -a lean
lean is /home/USER/.elan/bin/lean
lean is /home/USER/.elan/bin/lean

[Jon Eugster]

But still nothing happening after restarting VSCode

[Arthur Paulino]

(probably memory overload)

Did you check you memory consumption?

[Jon Eugster]

Arthur Paulino said:

(probably memory overload)

Did you check you memory consumption?

No, but the computer froze for a few seconds then VSCode crashed. My computer used to freeze a lot if lean was busy with a bad statement, so I just thought it was normal

[Jon Eugster]

"Restart Lean" should bring up the infoview automatically if it worked, right?

[Eric Rodriguez]

were you trying to run mathlib or somethinjg?

[Jon Eugster]

It's a leanproject that has mathlib in it, but it should have all the cached olean files.

[Eric Rodriguez]

what is the elan which lean in that repository? maybe it's worth reinstalling that Lean toolchain

[Jon Eugster]

I see VSCode was updated today (5554b12a, updated 08/02/2022, via Ubuntu Software Centre), so maybe that has something to do with it?

[Jon Eugster]

Eric Rodriguez said:

what is the elan which lean in that repository? maybe it's worth reinstalling that Lean toolchain

/home/USER/.elan/toolchains/leanprover-community--lean---3.38.0/bin/lean

[Jon Eugster]

How would I do that?

[Julian Berman]

Maybe I missed it, but does leanproject build work from inside your directory? It's just VSCode that sees a different version of Lean? Or do both end up trying to use 3.4.2?

[Jon Eugster]

Julian Berman said:

Maybe I missed it, but does leanproject build work from inside your directory? It's just VSCode that sees a different version of Lean? Or do both end up trying to use 3.4.2?

I mean it does something, it just returns "exit status 1" because the project was in-progress and still had errors in it.
The lean 3.4 was from lean -v (just put into bash), which I've now updated with elan update so it is now 3.38.0

[Jon Eugster]

and inside VSCode lean -v gives 3.39.1 --- Update: it doesnt, I guess it depends if there is a project open.

[Julian Berman]

Can you show us a screenshot of your VSCode with the project open?

[Julian Berman]

Though I see you said you're sure you've opened it correctly:

And yes, I was opening the folder, for example running code . inside the leanproject folder

[Jon Eugster]

Julian Berman said:

Though I see you said you're sure you've opened it correctly:

And yes, I was opening the folder, for example running code . inside the leanproject folder

no, Im not sure about anything :sweat_smile: (but yes, I believe that is the correct way?)

[Jon Eugster]

.

[Jon Eugster]

Screenshot-from-2022-02-08-16-59-47.png

[Julian Berman]

I think that seems ok -- can you show your leanpkg.toml contents too, it should hopefully say it wants 3.38.0

[Julian Berman]

Other than that the only other thing I can think of personally would be the VSCode "trusted workspace" functionalitiy (maybe you don't have it marked trusted)

[Jon Eugster]

[package]
name = "direct_summand"
version = "0.1"
lean_version = "leanprover-community/lean:3.38.0"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "f99af7da35d1f52405e28de99b810e68243b11c0"}

[Julian Berman]

OK, that looks good too.

[Jon Eugster]

Julian Berman said:

Other than that the only other thing I can think of personally would be the VSCode "trusted workspace" functionalitiy (maybe you don't have it marked trusted)

If I search "Workapce Trust" on Cmd+Shift+P it says "You trust this folder"

[Jon Eugster]

Well thanks for the help, maybe I can figure it out

[Julian Berman]

So it says it's trusted already?

[Julian Berman]

Just to be 100% sure, do File > Open Folder and again select your direct_summand folder perhaps, from the running VSCode

[Julian Berman]

But yeah after that I'm out of ideas personally

[Julian Berman]

Oh. I guess it looks like Eric had one you could try (reinstalling). Can't hurt if stuff is still broken.

[Jon Eugster]

Julian Berman said:

So it says it's trusted already?

Yes it does, the folder .../Lean is added as trusted folder and this project is .../Lean/direct_summand.

[Arthur Paulino]

Jon Eugster said:

yep, elan 0.10.3
Maybe I haven't updated lean in a while, that's at least the lean that is first in my path (which lean)

I have elan 1.3.1. Wanna try updating it with elan self update?

[Arthur Paulino]

I don't know if it's related, but 0.10.3 looks a bit old if compared to 1.3.1 (I'm a new Lean user too)

[Jon Eugster]

Good shout, I updated elan to 1.3.1, didn't really change anything though

[Jon Eugster]

Julian Berman said:

Oh. I guess it looks like Eric had one you could try (reinstalling). Can't hurt if stuff is still broken.

like uninstalling everything? How would I do that?

[Julian Berman]

I'd start first with reinstalling the VSCode Lean extension

[Julian Berman]

From the menu in VSCode

[Jon Eugster]

Hmm deleting & reinstalling VSCode seemed to have done the trick. Thank you everybody for the help!

[mathcat]

hi

[mathcat]

I'm on windows, and "leanproject" doesn't seem to work for me

[Henrik Böving]

You're gonna have to be a little more precise on what you did to get there and what doesnt work for you means.

[Alex J. Best]

Did you install it following https://leanprover-community.github.io/install/windows.html#get-python down to get scripts?

[mathcat]

yes. lean and elan are working, they're on path, but leanproject gives 'leanproject' is not recognized as an internal or external command, operable program or batch file.

[Yakov Pechersky]

What does pip list | grep mathlib say, if you have a bash-like shell?

[Yakov Pechersky]

If you are using powershell, pip list | Select-String "mathlib". If just CMD, pip list | findstr /c:"mathlib".

[mathcat]

it says mathlibtools 1.1.0 and the text turns yellow.

[Yakov Pechersky]

From your error, it seems you are using CMD. So, do you also get a similar error for pip list | findstr /c:"mathlib"?

[Yakov Pechersky]

Great, so you have the library installed, but somehow the executable itself isn't being found.

[Yakov Pechersky]

Do you have a "Git bash" installed on your machine?

[mathcat]

yes, opened it

[Yakov Pechersky]

Try leanproject in there first

[mathcat]

It says bash: leanproject: command not found too

[Yakov Pechersky]

In Git bash, pip install mathlibtools -U

[mathcat]

It says Requirements already satisfied and still doesn't work.

[mathcat]

I tried leanpkg and it created a .toml file. Is that good?

[Yakov Pechersky]

Try pip install mathlibtools --force-reinstall

[Yakov Pechersky]

We want to make sure your leanproject works. pip install mathlibtools is how one usually gets it. the problem you're seeing is that it does get installed, but likely in a location that the rest of your system is not aware of, for finding executable commands

[Yakov Pechersky]

If doing this pip install mathlibtools --force-reinstall does not make leanproject "work", then that means we need to figure out how to get your system to know where leanproject lives. That will mean modifying the environment variable $PATH. First, we'll check what your $PATH is, check we know where leanproject really lives, and then combining that.

[mathcat]

Doesn't work, but I know now where mathlibtools is installed. I can also see a file called leanproject.py there.

[Yakov Pechersky]

And where is that?

[mathcat]

C:\Users\[User]\AppData\Roaming\Python\Python310\site-packages\mathlibtools

[Yakov Pechersky]

What do you see when you try ls "C:\Users\[User]\AppData\Roaming\Python\Python310\Scripts" in your Git bash?

[mathcat]

it shows leanproject.exe! Shall I add it to PATH?

[Yakov Pechersky]

First, let's confirm that running it works. what happens when you run "C:\Users\[User]\AppData\Roaming\Python\Python310\Scripts\leanproject" (note, no command before the first quotation mark)

[mathcat]

Works, prints a description.

[mathcat]

I'll try new

[Yakov Pechersky]

Wonderful. You can add "C:\Users\[User]\AppData\Roaming\Python\Python310\Scripts" to your windows PATH:

Right click on the "Computer", "My Computer" or "This PC" icon → select "Properties". Click on "Advanced system settings" (on the left side). (Enter your administrator password when requested.) In the "System Properties" window, click on "Environment Variables" (near the bottom). In the "Environment Variables" window, search for PATH under "System Variables". Select it and click on "Edit…". Add a semicolon (";") to the variable value and paste the path we figured out.

(rephrased from https://superuser.com/a/1558227)

[mathcat]

Working, thanks!

[mathcat]

btw, I'm folllowing this tutorial, and it seems data.nat.prime doesn't exist anymore. Where is it now?

[Ruben Van de Velde]

The file should still exist - you may run into fact being renamed

[mathcat]

strange, it says could not resolve import: data.nat.prime but eg. init.data.nat.basic works

[mathcat]

It's also not in .elan\toolchains\stable\lib\lean\library\init\data\nat

[Ruben Van de Velde]

The files under .elan are from core lean; data.nat.prime is in mathlib, so it makes sense that it isn't there. Did you add mathlib to your project?

[mathcat]

no, how can I add it?

[mathcat]

actually, it's in dependencies in leanpkg.toml

[mathcat]

In _target/deps/mathlib I can see a prime.lean file, but Lean in not recognizing it

[Yakov Pechersky]

mathcat, at this point, you should now use leanproject! so delete leanpkg.toml, and run leanproject get mathlib. That should create a new folder called mathlib

[Yakov Pechersky]

Or leanproject new my_new_proj and open my_new_proj (the folder!) in VSCode

[mathcat]

Yakov Pechersky said:

Or leanproject new my_new_proj and open my_new_proj (the folder!) in VSCode

That's what I did

[Yakov Pechersky]

what happens when you are in the my_new_proj folder and run leanproject get-m?

[mathcat]

one sec brb

[mathcat]

it says files extracted: 2143 [00:19, 108.40/s]

[mathcat]

but the lean infoview still errors

[mathcat]

btw when I type lean --path as it suggests, it also shows C:\\Users\\[user]\\[folder]\\Lean\\Primes\\infinitude-of-primes\\_target/deps/mathlib/src

[Yakov Pechersky]

Can you restart the vscode by closing it and reopening it?

[mathcat]

Tried, many times (closing, reload, logging out, reloading extension) but didn't work. Maybe I'll restart the computer.

[mathcat]

It's working! Thanks everyone

[mathcat]

Ruben Van de Velde said:

The file should still exist - you may run into fact being renamed

what's it now?

[mathcat]

nvm, got it

[David Landsberg]

David Landsberg: Hi, very new to this! Have a very basic problem installing lean. I followed the instructions on the video (below), but when I try the #eval 2+2 in VS code, I just get the message "Waiting for Lean server to start ... " in the Lean infoview. (... the video I used is posted in the Lean community installation instruction page, and is here https://www.youtube.com/watch?v=y3GsHIe4wZ4)

David Landsberg: So any advice would be hugely appreciated!

[Mario Carneiro]

Note that this is a pretty old video; make sure that your installation steps look like the latest and greatest advice at https://leanprover-community.github.io/get_started.html

[David Landsberg]

Thanks Mario! Will do

[Mario Carneiro]

actually looking at it again it seems most of the things there are still true

[Mario Carneiro]

If you open the terminal and type lean what do you get?

[David Landsberg]

I get the following... Usage: lean [OPTIONS] COMMAND [ARGS]...

The Lean CLI by QuantConnect.

Options:
--version Show the version and exit.
--help Show this message and exit.
... and then a lot of options

[David Landsberg]

It looks like i didn't install elan correctly perhaps, I'm going to uninstall lean and reinstall elan as a first step

[Mario Carneiro]

oh yikes, who's QuantConnect?

[Mario Carneiro]

Haha we have a competitor https://www.lean.io/

[Reid Barton]

Good thing the name of our system isn't LEAN.

[Arthur Paulino]

I had seen it before. I thought it would be vastly known by the community! :joy:

[Mario Carneiro]

I've literally never heard about it

[Mario Carneiro]

although I was informed about a lean subreddit that I regret investigating

[Mario Carneiro]

it's got 3 times more github stars than leanprover :surprise:

[David Landsberg]

Mario - got it to work - thanks for your prompt about the instructions it was kind of you to help! :smile: :+1:

[Ernst Herzhöfer]

a newbie question, how do I get leanproject command available?

[Eric Rodriguez]

please move this to another thread, but the installation instructions are here

[Ernst Herzhöfer]

i have installed lean by install elan first, now I have lean command available but not leanproject

[Ernst Herzhöfer]

where is the source of this leanproject so I can install separately from elan? I can't find "leanproject" in my path after install elan

[Patrick Massot]

This is all explained in the installation instructions

[Eric Rodriguez]

what operating system are you using?

[Ernst Herzhöfer]

Im using ubuntu20, btw the installation instruction is mostly a oneliner, and i coudnt figure out where is leanproject from that script

[Ernst Herzhöfer]

from the looks of it, leanproject should be contained in the installation of elan.

[Ernst Herzhöfer]

~ elan show
stable (default)
Lean (version 3.39.2, commit 402f41cdedbd, Release)

[Eric Rodriguez]

leanproject is separate from elan, it's a python package. you can either reinstall with the explicit ubuntu instructions, or this page mentions how to get leanproject separately

[Ernst Herzhöfer]

aha, so pipx install mathlibtools installs leanproject? thats a little bit confusing.

[Patrick Massot]

Right above that one liner there is a link to a more detailed webpage for people who don't like easy installation procedures.

[Patrick Massot]

leanproject is a tool for people who want to use mathlib, hence the name. If you are not interested in mathlib then leanproject won't do anything useful to you.

[Ernst Herzhöfer]

I came from the tutorial when there was this command "leanproject get ImperialCollegeLondon/M40001_lean" , so my first impression is this was a remote client for getting repositories. now I understand, thanks!

[chensc]

Hey guys, having some installation problems, is this the right place to look for help?

[Notification Bot]

Johan Commelin has marked this topic as unresolved.

[Johan Commelin]

@chensc this is a better thread for your question, I think

[chensc]

I have tried and failed installing LEAN manually, so think of trying the "trylean" alternative presented in the "get started" page. However I'm afraid my previous installations might cause some problems, is it indeed the case?

[Jakub Kądziołka]

I don't think they would, I'd suggest you try trylean and if it doesn't work we'll try to fix it. What OS are you on?

[chensc]

Ubuntu

[chensc]

Ok, I'll give it a try

[Kevin Buzzard]

I recently got a new Ubuntu machine and the one-line install procedure worked fine for me

[Kevin Buzzard]

wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

[Patrick Massot]

Kevin, the trylean alternative is not this, it gets everything in a single folder with no installation at all.

[Patrick Massot]

This the technology that was originally intended for teaching only.

[Patrick Massot]

But of course the recommended move is the one-line full install that Kevin wrote above.

[chensc]

OK, so I'm trying Kevin's line

[chensc]

From here, how should I run the tutorials? just "code tutorials"?

[chensc]

Or , is this one line installation does not include the tutorial project?

[chensc]

All pipx binary directories have been added to PATH. If you are sure you want to proceed, try again with the
'--force' flag.

Otherwise pipx is ready to go! :sparkles: :glowing_star: :sparkles:
'mathlibtools' already seems to be installed. Not modifying existing installation in
'/home/chen/.local/pipx/venvs/mathlibtools'. Pass '--force' to force installation.

[chensc]

This is the output. Should I type this "--force" flag?

[Jakub Kądziołka]

Probably not. Could you link the documentation/tutorial you're following?

[chensc]

https://leanprover-community.github.io/install/debian.html
Might be important to note that I have already installed lean 4 before, maybe it caused the problem
Then, I moved to here, "Working on an existing project":
https://leanprover-community.github.io/install/project.html

[Jakub Kądziołka]

you mentioned something about lean being unresponsive in a private message to me. could you describe that more? or perhaps you could post a screen recording? that way someone might notice a smoking gun that you wouldn't think to mention yourself

[chensc]

Screenshot-from-2022-03-04-17-38-45.png

[chensc]

So this Is the result I get when trying the tutorials

[chensc]

Screenshot-from-2022-03-04-17-40-11.png

[chensc]

And on the other hand, this is the result I get when trying the "mathematics_in_lean" project

[Eric Rodriguez]

what happens if you hover over the errors in the tutorials? and in the mathematics in Lean, have you tried the "Lean: Restart Server" command?

[chensc]

"Error updating: excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold" - in some of the errors in the tutorials

[Eric Rodriguez]

try run leanproject get-m in the command line below and restart the server after

[Eric Rodriguez]

this usually means Lean is having to try and recompile everything from scratch which isn't scalable

[chensc]

tutorials git:(master) ✗ leanproject get-m
Looking for mathlib oleans for 5449ffa41
locally...
remotely...
Found remote mathlib oleans
Located matching cache
5449ffa41: 62%|█████████████████████████████████████████████████████████▎ | 36.6M/58.8M [03:32<00:33, 696kB/s] 5449ffa41: 100%|████████████████████████████████████████████████████████████████████████████████████████████| 58.8M/58.8M [04:30<00:00, 228kB/s]
Applying cache
files extracted: 2094 [00:05, 377.04/s]
➜ tutorials git:(master) ✗ Lean: Restart Server
zsh: command not found: Lean:

[chensc]

I run "leanproject get-m" as you said, but it seems the terminal cant find "Lean: Restart Server"

[Eric Rodriguez]

that second command isn't a terminal command, but a VSCode command (and one you'll use pretty often with Lean, to be frank)

[chensc]

Sorry - My ignorance. Where should I type it than? I can't see another input field for commands

[chensc]

Screenshot-from-2022-03-04-18-01-24.png

[Eric Rodriguez]

press (command / ctrl) + shift + p

[Eric Rodriguez]

(whilst focused on the text field)

[Eric Rodriguez]

you can also just restart VSCode itself

[chensc]

It seems like its working!

[John Nicol]

Hi, I'm also attempting to install LEAN per the https://leanprover-community.github.io/install/debian.html instructions. It seemed to work (generally) fine, although this error message seems concerning and is causing problems after trying the tutorial:
leanproject get tutorials
Cloning from git@github.com:leanprover-community/tutorials.git
Error cloning via SSH, trying HTTPS...
Cloning from https://github.com/leanprover-community/tutorials.git
[Errno 2] No such file or directory: 'leanpkg'

[John Nicol]

Ah, never mind! This appears to be caused by not running "source ~/.profile." I thought opening a new shell tab would have picked this up, but strangely not.

[Jannis Limperg]

.profile is often only read on login, that's probably what happened.

[John Nicol]

For future reference, I also got the "excessive memory consumption" output -- which took so long to happen I thought the server wasn't configured -- but the steps above ("leanproject get -m" and "Lean: Restart") fixed it.

[Nischal Karki]

hi everyone
i am having some problems installing lean4 via elan in vscode . plz help me

[Julian Berman]

@Nischal Karki please share some information about what you ran and what errors you're seeing.

[Nischal Karki]

the terminal reads the following:

PS C:\Users\HP> Invoke-WebRequest -Uri "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1" -OutFile elan-init.ps1
The term 'Invoke-WebRequest' is not recognized as the name of a cmdlet, function, script file, or operable program. Check the spelling of the name
, or if a path was included, verify that the path is correct and try again.
At line:1 char:18

• Invoke-WebRequest <<<< -Uri "https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1" -OutFile elan-init.ps1
  + CategoryInfo : ObjectNotFound: (Invoke-WebRequest:String) [], CommandNotFoundException
  + FullyQualifiedErrorId : CommandNotFoundException

PS C:\Users\HP> $rc = .\elan-init.ps1 -NoPrompt 1 -DefaultToolchain leanprover/lean4:nightly
The term '.\elan-init.ps1' is not recognized as the name of a cmdlet, function, script file, or operable program. Check the spelling of the name,
or if a path was included, verify that the path is correct and try again.
At line:1 char:22

• $rc = .\elan-init.ps1 <<<< -NoPrompt 1 -DefaultToolchain leanprover/lean4:nightly
  + CategoryInfo : ObjectNotFound: (.\elan-init.ps1:String) [], CommandNotFoundException
  + FullyQualifiedErrorId : CommandNotFoundException

PS C:\Users\HP> Write-Host "elan-init returned [$rc]"
elan-init returned []
PS C:\Users\HP> del .\elan-init.ps1
Remove-Item : Cannot find path 'C:\Users\HP\elan-init.ps1' because it does not exist.
At line:1 char:4

• del <<<< .\elan-init.ps1
  + CategoryInfo : ObjectNotFound: (C:\Users\HP\elan-init.ps1:String) [Remove-Item], ItemNotFoundException
  + FullyQualifiedErrorId : PathNotFound,Microsoft.PowerShell.Commands.RemoveItemCommand

PS C:\Users\HP> if ($rc -ne 0) {

Read-Host -Prompt "Press ENTER to continue"

}

[Julian Berman]

Which page / installation instructions are you following?

[Nischal Karki]

Julian Berman said:

Which page / installation instructions are you following?

as mentioned in the official documentation https://leanprover.github.io/lean4/doc/quickstart.html

[Mauricio Collares]

What's your Windows version? And what is your PowerShell version?

[Nischal Karki]

Mauricio Collares said:

What's your Windows version? And what is your PowerShell version?

windows 7 powershell of 2009

[Nischal Karki]

it also says: Error: spawn lean ENONENT

[Nischal Karki]

i would really appreciate any help. anyone?

[Mauricio Collares]

You can probably solve your installation error by updating PowerShell, but even if you do that I think Lean 4 requires Windows 10

[Nischal Karki]

Is windows 10 a must ? Aren't there any other options. anyone?

[Julian Berman]

Running Linux in a VM is of course another.

[Jorge Medina]

Hi everyone, new member here. im having trouble initiating a new project.
After leanproject new my_project in bash. I got the error, "cannot execute binary file"
i could download the tutorials though.
Any idea on whats happening? or suggestions to go around it?

[Anne Baanen]

Jorge Medina said:

After leanproject new my_project in bash. I got the error, "cannot execute binary file"

This might mean that you have a version of Lean that is not compiled for your current machine, or many other things. What is the full output of the command? In particular, the error message should look more like /usr/bin/lean: cannot execute binary file, and that first part is important.

[Suvendu Kar]

Hello!

I am very new in the community and gathered a keen interest on lean porting.

I am in stuck with my very first code.In VS Code it is showing: Waiting for Lean server to start...

please help me to resolve.( I am working on windows 11, lean 4 version 0.0.102)

[Kevin Buzzard]

Have you opened the root directory of the Lean project you are working on with VS Code's "open folder" functionality?

[Suvendu Kar]

Now I am getting the error: ModuleNotFoundError: No module named 'Lean' (under terminal)

[Eric Wieser]

That error is from Python. If sounds like you opened a python terminal not a regular terminal

[Suvendu Kar]

Please help me with possible solutions.From last day, I am facing same problem continuously.No progress.
Screenshot-70.png

[Eric Wieser]

Your command line says python.exe. Why did you run that?

[Suvendu Kar]

To check whether lean 4 works properly in my device or not. I followed the guideline as per lean website and at last there they provided that code to run to check whether I all set or not.Please guide me what should I do? I am in stuck from last day

[Eric Wieser]

Which instructions did you read that told you to write python.exe your_lean_file.lean?

[Eric Wieser]

Note also that you should rename your file from lean4 to lean4.lean

[Suvendu Kar]

I actually installed earlier lean 3 and may be that is effecting.Kindly guide properly, what should I now to fix the issue

[Alex J. Best]

Did you rename the file yet? To lean4.lean? What happens then?

[One An]

hello, I'm currently trying to download lean and git bash says it cannot verify the security when I try to download elan. Is there a fix to this issue?

[Alex J. Best]

I would search the precise error message in a search engine and see if there is any advice there, possibly this is an issue with curl on your machine?