Zulip Chat Archive

Stream: new members

Topic: installation problems


Kevin Buzzard (Sep 05 2020 at 06:18):

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 (Sep 05 2020 at 06:19):

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 (Sep 05 2020 at 06:20):

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

Kevin Buzzard (Sep 05 2020 at 06:21):

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 (Sep 05 2020 at 06:26):

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 (Sep 05 2020 at 07:14):

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 (Sep 05 2020 at 07:14):

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

Scott Morrison (Sep 05 2020 at 07:15):

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

Scott Morrison (Sep 05 2020 at 07:16):

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 (Sep 05 2020 at 07:24):

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 (Sep 05 2020 at 07:25):

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 (Sep 05 2020 at 07:31):

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

Thorsten Altenkirch (Sep 05 2020 at 13:09):

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 (Sep 05 2020 at 13:10):

#backticks

Kenny Lau (Sep 05 2020 at 13:13):

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

Kevin Buzzard (Sep 05 2020 at 13:19):

The version of lean looks good though

Thorsten Altenkirch (Sep 05 2020 at 13:20):

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 (Sep 05 2020 at 13:20):

@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 (Sep 05 2020 at 13:20):

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

Thorsten Altenkirch (Sep 05 2020 at 13:21):

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 (Sep 05 2020 at 13:22):

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

Kevin Buzzard (Sep 05 2020 at 13:22):

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

Thorsten Altenkirch (Sep 05 2020 at 13:23):

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

Thorsten Altenkirch (Sep 05 2020 at 13:27):

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 (Sep 05 2020 at 13:27):

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

Kevin Buzzard (Sep 05 2020 at 13:28):

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

Thorsten Altenkirch (Sep 05 2020 at 13:28):

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

Thorsten Altenkirch (Sep 05 2020 at 13:31):

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 (Sep 05 2020 at 13:32):

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 (Sep 05 2020 at 13:33):

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 (Sep 05 2020 at 13:34):

see #rss

Kevin Buzzard (Sep 05 2020 at 13:35):

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 (Sep 05 2020 at 14:14):

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 (Sep 05 2020 at 14:15):

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 (Sep 05 2020 at 14:15):

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 (Sep 05 2020 at 14:24):

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 (Sep 05 2020 at 14:31):

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

Patrick Massot (Sep 05 2020 at 14:31):

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 (Sep 05 2020 at 14:33):

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 (Sep 05 2020 at 14:42):

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 (Feb 08 2022 at 16:13):

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 (Feb 08 2022 at 16:16):

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 (Feb 08 2022 at 16:20):

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 (Feb 08 2022 at 16:25):

Lean 3.4.2 :shock: do you have elan installed?

Jon Eugster (Feb 08 2022 at 16:26):

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 (Feb 08 2022 at 16:27):

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

Eric Rodriguez (Feb 08 2022 at 16:28):

what does elan show show?

Julian Berman (Feb 08 2022 at 16:30):

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

Jon Eugster (Feb 08 2022 at 16:31):

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 (Feb 08 2022 at 16:32):

But still nothing happening after restarting VSCode

Arthur Paulino (Feb 08 2022 at 16:34):

(probably memory overload)

Did you check you memory consumption?

Jon Eugster (Feb 08 2022 at 16:36):

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 (Feb 08 2022 at 16:39):

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

Eric Rodriguez (Feb 08 2022 at 16:40):

were you trying to run mathlib or somethinjg?

Jon Eugster (Feb 08 2022 at 16:42):

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

Eric Rodriguez (Feb 08 2022 at 16:43):

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

Jon Eugster (Feb 08 2022 at 16:44):

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 (Feb 08 2022 at 16:45):

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 (Feb 08 2022 at 16:45):

How would I do that?

Julian Berman (Feb 08 2022 at 16:53):

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 (Feb 08 2022 at 16:57):

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 (Feb 08 2022 at 16:58):

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

Julian Berman (Feb 08 2022 at 16:58):

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

Julian Berman (Feb 08 2022 at 16:59):

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 (Feb 08 2022 at 17:00):

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 (Feb 08 2022 at 17:01):

.

Jon Eugster (Feb 08 2022 at 17:03):

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

Julian Berman (Feb 08 2022 at 17:06):

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

Julian Berman (Feb 08 2022 at 17:06):

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 (Feb 08 2022 at 17:07):

[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 (Feb 08 2022 at 17:08):

OK, that looks good too.

Jon Eugster (Feb 08 2022 at 17:09):

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 (Feb 08 2022 at 17:09):

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

Julian Berman (Feb 08 2022 at 17:10):

So it says it's trusted already?

Julian Berman (Feb 08 2022 at 17:12):

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

Julian Berman (Feb 08 2022 at 17:12):

But yeah after that I'm out of ideas personally

Julian Berman (Feb 08 2022 at 17:14):

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

Jon Eugster (Feb 08 2022 at 17:16):

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 (Feb 08 2022 at 17:16):

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 (Feb 08 2022 at 17:18):

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 (Feb 08 2022 at 17:18):

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

Jon Eugster (Feb 08 2022 at 17:19):

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 (Feb 08 2022 at 17:19):

I'd start first with reinstalling the VSCode Lean extension

Julian Berman (Feb 08 2022 at 17:20):

From the menu in VSCode

Jon Eugster (Feb 08 2022 at 17:28):

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

mathcat (Feb 08 2022 at 20:20):

hi

mathcat (Feb 08 2022 at 20:21):

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

Henrik Böving (Feb 08 2022 at 20:35):

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 (Feb 08 2022 at 20:36):

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

mathcat (Feb 09 2022 at 13:46):

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 (Feb 09 2022 at 13:55):

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

Yakov Pechersky (Feb 09 2022 at 13:58):

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

mathcat (Feb 09 2022 at 14:00):

it says mathlibtools 1.1.0 and the text turns yellow.

Yakov Pechersky (Feb 09 2022 at 14:00):

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 (Feb 09 2022 at 14:01):

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

Yakov Pechersky (Feb 09 2022 at 14:03):

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

mathcat (Feb 09 2022 at 14:03):

yes, opened it

Yakov Pechersky (Feb 09 2022 at 14:04):

Try leanproject in there first

mathcat (Feb 09 2022 at 14:04):

It says bash: leanproject: command not found too

Yakov Pechersky (Feb 09 2022 at 14:04):

In Git bash, pip install mathlibtools -U

mathcat (Feb 09 2022 at 14:06):

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

mathcat (Feb 09 2022 at 14:08):

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

Yakov Pechersky (Feb 09 2022 at 14:10):

Try pip install mathlibtools --force-reinstall

Yakov Pechersky (Feb 09 2022 at 14:10):

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 (Feb 09 2022 at 14:12):

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 (Feb 09 2022 at 14:19):

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

Yakov Pechersky (Feb 09 2022 at 14:21):

And where is that?

mathcat (Feb 09 2022 at 14:22):

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

Yakov Pechersky (Feb 09 2022 at 14:24):

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

mathcat (Feb 09 2022 at 14:25):

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

Yakov Pechersky (Feb 09 2022 at 14:26):

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 (Feb 09 2022 at 14:28):

Works, prints a description.

mathcat (Feb 09 2022 at 14:29):

I'll try new

Yakov Pechersky (Feb 09 2022 at 14:29):

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 (Feb 09 2022 at 14:35):

Working, thanks!

mathcat (Feb 09 2022 at 14:36):

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

Ruben Van de Velde (Feb 09 2022 at 14:40):

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

mathcat (Feb 09 2022 at 14:42):

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

mathcat (Feb 09 2022 at 14:47):

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

Ruben Van de Velde (Feb 09 2022 at 14:51):

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 (Feb 09 2022 at 14:51):

no, how can I add it?

mathcat (Feb 09 2022 at 14:52):

actually, it's in dependencies in leanpkg.toml

mathcat (Feb 09 2022 at 14:56):

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

Yakov Pechersky (Feb 09 2022 at 14:56):

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 (Feb 09 2022 at 14:56):

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

mathcat (Feb 09 2022 at 14:57):

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 (Feb 09 2022 at 14:57):

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

mathcat (Feb 09 2022 at 14:58):

one sec brb

mathcat (Feb 09 2022 at 15:22):

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

mathcat (Feb 09 2022 at 15:22):

but the lean infoview still errors

mathcat (Feb 09 2022 at 15:23):

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 (Feb 09 2022 at 15:56):

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

mathcat (Feb 09 2022 at 16:03):

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

mathcat (Feb 09 2022 at 16:25):

It's working! Thanks everyone

mathcat (Feb 09 2022 at 16:41):

Ruben Van de Velde said:

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

what's it now?

mathcat (Feb 09 2022 at 16:43):

nvm, got it

David Landsberg (Feb 10 2022 at 03:50):

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 (Feb 10 2022 at 03:51):

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 (Feb 10 2022 at 03:52):

Thanks Mario! Will do

Mario Carneiro (Feb 10 2022 at 03:55):

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

Mario Carneiro (Feb 10 2022 at 03:55):

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

David Landsberg (Feb 10 2022 at 04:00):

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 (Feb 10 2022 at 04:01):

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 (Feb 10 2022 at 04:02):

oh yikes, who's QuantConnect?

Mario Carneiro (Feb 10 2022 at 04:03):

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

Reid Barton (Feb 10 2022 at 04:04):

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

Arthur Paulino (Feb 10 2022 at 04:04):

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

Mario Carneiro (Feb 10 2022 at 04:05):

I've literally never heard about it

Mario Carneiro (Feb 10 2022 at 04:05):

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

Mario Carneiro (Feb 10 2022 at 04:06):

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

David Landsberg (Feb 10 2022 at 04:13):

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

Ernst Herzhöfer (Feb 22 2022 at 12:44):

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

Eric Rodriguez (Feb 22 2022 at 12:45):

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

Ernst Herzhöfer (Feb 22 2022 at 12:47):

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

Ernst Herzhöfer (Feb 22 2022 at 12:54):

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 (Feb 22 2022 at 12:58):

This is all explained in the installation instructions

Eric Rodriguez (Feb 22 2022 at 12:58):

what operating system are you using?

Ernst Herzhöfer (Feb 22 2022 at 13:04):

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 (Feb 22 2022 at 13:05):

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

Ernst Herzhöfer (Feb 22 2022 at 13:06):

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

Eric Rodriguez (Feb 22 2022 at 13:07):

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 (Feb 22 2022 at 13:08):

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

Patrick Massot (Feb 22 2022 at 13:09):

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 (Feb 22 2022 at 13:10):

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 (Feb 22 2022 at 13:13):

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 (Mar 04 2022 at 13:01):

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

Notification Bot (Mar 04 2022 at 13:02):

Johan Commelin has marked this topic as unresolved.

Johan Commelin (Mar 04 2022 at 13:02):

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

chensc (Mar 04 2022 at 13:08):

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 (Mar 04 2022 at 13:10):

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 (Mar 04 2022 at 13:10):

Ubuntu

chensc (Mar 04 2022 at 13:10):

Ok, I'll give it a try

Kevin Buzzard (Mar 04 2022 at 13:18):

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

Kevin Buzzard (Mar 04 2022 at 13:19):

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 (Mar 04 2022 at 13:21):

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

Patrick Massot (Mar 04 2022 at 13:21):

This the technology that was originally intended for teaching only.

Patrick Massot (Mar 04 2022 at 13:21):

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

chensc (Mar 04 2022 at 13:23):

OK, so I'm trying Kevin's line

chensc (Mar 04 2022 at 13:24):

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

chensc (Mar 04 2022 at 13:25):

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

chensc (Mar 04 2022 at 13:26):

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 (Mar 04 2022 at 13:28):

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

Jakub Kądziołka (Mar 04 2022 at 14:01):

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

chensc (Mar 04 2022 at 14:45):

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 (Mar 04 2022 at 15:12):

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 (Mar 04 2022 at 15:39):

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

chensc (Mar 04 2022 at 15:39):

So this Is the result I get when trying the tutorials

chensc (Mar 04 2022 at 15:40):

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

chensc (Mar 04 2022 at 15:40):

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

Eric Rodriguez (Mar 04 2022 at 15:43):

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 (Mar 04 2022 at 15:44):

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

Eric Rodriguez (Mar 04 2022 at 15:45):

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

Eric Rodriguez (Mar 04 2022 at 15:45):

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

chensc (Mar 04 2022 at 15:52):

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 (Mar 04 2022 at 15:54):

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

Eric Rodriguez (Mar 04 2022 at 15:55):

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 (Mar 04 2022 at 16:01):

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

chensc (Mar 04 2022 at 16:01):

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

Eric Rodriguez (Mar 04 2022 at 16:01):

press (command / ctrl) + shift + p

Eric Rodriguez (Mar 04 2022 at 16:02):

(whilst focused on the text field)

Eric Rodriguez (Mar 04 2022 at 16:02):

you can also just restart VSCode itself

chensc (Mar 04 2022 at 16:04):

It seems like its working!

John Nicol (Mar 04 2022 at 19:25):

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 (Mar 04 2022 at 19:29):

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 (Mar 04 2022 at 19:40):

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

John Nicol (Mar 04 2022 at 19:59):

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 (Jul 12 2022 at 11:29):

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

Julian Berman (Jul 12 2022 at 11:30):

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

Nischal Karki (Jul 12 2022 at 11:31):

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

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 (Jul 12 2022 at 11:33):

Which page / installation instructions are you following?

Nischal Karki (Jul 12 2022 at 11:35):

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 (Jul 12 2022 at 11:36):

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

Nischal Karki (Jul 12 2022 at 11:40):

Mauricio Collares said:

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

windows 7 powershell of 2009

Nischal Karki (Jul 12 2022 at 11:47):

it also says: Error: spawn lean ENONENT

Nischal Karki (Jul 12 2022 at 11:55):

i would really appreciate any help. anyone?

Mauricio Collares (Jul 12 2022 at 12:04):

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 (Jul 12 2022 at 13:55):

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

Julian Berman (Jul 12 2022 at 20:32):

Running Linux in a VM is of course another.

Jorge Medina (Jul 12 2022 at 20:42):

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 (Jul 13 2022 at 12:09):

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 (May 20 2023 at 12:07):

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 (May 20 2023 at 12:39):

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

Suvendu Kar (May 21 2023 at 05:54):

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

Eric Wieser (May 21 2023 at 06:41):

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

Suvendu Kar (May 21 2023 at 07:34):

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

Eric Wieser (May 21 2023 at 07:40):

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

Suvendu Kar (May 21 2023 at 09:01):

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 (May 21 2023 at 09:08):

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

Eric Wieser (May 21 2023 at 09:09):

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

Suvendu Kar (May 21 2023 at 09:46):

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 (May 22 2023 at 04:53):

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

One An (May 24 2023 at 12:16):

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 (May 24 2023 at 13:28):

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?


Last updated: Dec 20 2023 at 11:08 UTC