Getting started

Stream: new members

[Marijn Stollenga]

Hi, how do I get started with lean? There is plenty of documentation, but it seems to need some bootstrapping. E.g. simple things like building instructions seem to point to the download page which points to the github with points to the download page :O

[Rob Lewis]

There are installation directions in the readme here: https://github.com/leanprover-community/mathlib

[Marijn Stollenga]

Thanks, right now i build and installed it after finding the cmake files in src/
I also found the https://leanprover.github.io/tutorial/ so I'll try that

[Marijn Stollenga]

Is there a good initial proof the check out in the library perhaps?

[Rob Lewis]

That tutorial is for Lean 2, which hasn't been supported since 2016. If you're really using Lean 2, you're on your own.

[Marijn Stollenga]

Ok is there anything for lean 3?

[Rob Lewis]

Yes, Theorem Proving in Lean is linked here: https://leanprover.github.io/documentation/ I have no idea where you even found the link to the old version.

[Marijn Stollenga]

Somehow Google brought me there

[Marc Huisinga]

it shows up when googling "lean tutorial"

[Marijn Stollenga]

Indeed, so is https://leanprover.github.io/introduction_to_lean/ the right one?

[Bryan Gin-ge Chen]

No, that is also out of date. See Theorem Proving in Lean.

[Marijn Stollenga]

Btw, how do I interpret the Π ? Some of these things show up but are not really explained, at least I don't know where.

[Marc Huisinga]

https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#dependent-types

[Kevin Buzzard]

You get started by finding a nice supply of simple questions and then getting stuck 100 times and asking here how to get unstuck :D

[Marc Huisinga]

that and TPIL ;)

[Bryan Gin-ge Chen]

Logic & Proof is also good, though it's not just about Lean.

[Kevin Buzzard]

Cheat sheet: http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/tactics/guide.html

[Marijn Stollenga]

I like the cheat sheet

[Marijn Stollenga]

I saw mentioned that the fundamental arithmetic theorem is proved somewhere in the repo? Where is that?

[Kevin Buzzard]

If you're just doing basic logic and learning the basics, it can be helpful. I remember running into an analogous cheat sheet for Coq when I was figuring out the basics of that.

[Bryan Gin-ge Chen]

It looks like the Fundamental theorem of arithmetic is here.

[Bryan Gin-ge Chen]

If by chance you'd prefer to see how one proves that the integers are a unique factorization domain using mathlib, see the discussion on the fundamental theorem of arithmetic in @Floris van Doorn's "100 theorems" branch.

[Marijn Stollenga]

very interesting; if something mentions irreducible does it mean the prover takes it as a fact?

[Floris van Doorn]

No, irreducible is just a hint to Lean to say "please don't unfold this definition" (sorry is used to omit a proof of something - it is not used in mathlib)

[Marijn Stollenga]

Are there also some pointers to learn more about the kernel and it's implementation?

[Kevin Buzzard]

Mario Carneiro's MSc thesis https://github.com/digama0/lean-type-theory explains Lean's type theory. As for the kernel, note that it is currently being completely rewritten; we all use Lean 3 but Lean 4 is becoming more usable as time goes on.

[Marijn Stollenga]

Thanks! Yeah heard lean 4 will integrate LLVM? very interesting

[Kevin Buzzard]

I think it might do this already?

[Marijn Stollenga]

I also found this YouTube series: https://www.youtube.com/watch?v=LIv17t6HRQY
The audio is low, but it's really clear and explains things that I didn't see clearly explained in the docs. Even simple things like what the := means, are not clear and kind of hidden in the doc.

[Alex J. Best]

I definitely agree that a good video can be a lot better than the docs when getting started, I learnt a lot from the demos (videos + code) at lean-together https://lean-forward.github.io/lean-together/2019/

[Alex J. Best]

The tutorials there specifically!

[Marijn Stollenga]

That is a smooth site, video with slides works great!

[Golol]

Hi

[Golol]

Are there any fundamental difference between lean and mizar? I'm very excited to get into a proof verifier.

[Johan Commelin]

What do you mean with "fundamental". They are very different in a lot of senses.

[Johan Commelin]

Maybe the only thing that they have in common is that it is generally believed that you can formalize all of mathematics in both of them

[Kevin Buzzard]

The tutorials there specifically!

That is a bit terrifying. I remember helping out several beginners at Lean Together but I don't remember trying to leave behind a coherent trail for others.

[Scott Morrison]

@Golol, Lean is a functional programming language (rather like Haskell), which has a dependent type theory (like Coq, and Agda) which is sufficiently expressive that you can "do most maths" in it in a fairly natural way. You can write proofs either in "term mode" (like programming) or in "tactic mode" (more like a declarative script telling Lean how to manipulate the proof goals). It is being actively developed (Lean 4 is coming along, and the mathematical library, mathlib, is being worked on by lots of people here).

[Scott Morrison]

I've in the past found https://www.cl.cam.ac.uk/~jrh13/papers/joerg.pdf quite useful as a comparison on the older theorem provers. (Mizar is definitely one of the older ones...) I've never actually used it, so won't attempt a one-paragraph summary. :-)

[vtrandal]

I am new to leanprover (but I am not new to the concepts). I am looking for instructions how to install in Linux and run leanprover on a trivial example. Does that information exist anywhere?

[Scott Morrison]

https://github.com/leanprover-community/mathlib#installation

[vtrandal]

Thank you. About an hour ago I started here https://github.com/leanprover/lean and cloned the repository as follows
git clone https://github.com/leanprover/lean.git

[Kevin Buzzard]

I would suggest that you follow Scott's link, even if you are not interested in mathlib. We've had countless experiences with users who don't do this and then have problems down the line.

[Mario Carneiro]

If you want to compile from source, there are instructions at https://github.com/leanprover-community/lean/blob/master/doc/make/index.md

[Kevin Buzzard]

I think there might even be issues with compiling Lean 3 on certain modern compilers, Lean 4 isn't really ready for beginner use, and lean 3 is not being maintained, so if you go your own way then be prepared for frustration.

[vtrandal]

Thank you. Yes, I am compiling from source as I always do for just about any project.

[Mario Carneiro]

(FYI, leanprover/lean is EOL'd, you should use leanprover-community/lean)'

[Mario Carneiro]

I recently compiled lean on a fresh linux install based on those instructions and it went pretty smoothly

[Kevin Buzzard]

If you know what you're doing then you might want to look at the scripts which are run in the mathlib installation process. We usually use elan for Lean (which is our rustup)

[Mario Carneiro]

I recommend using ninja instead of make; there is a note a bit later on the page about adding -G Ninja to the cmake command to make it work

[Kevin Buzzard]

Perhaps the only other issue you might have is integrating with VS Code (if you're using VS Code); there used to be a problem with Windows users having a space in their usernames

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib#installation

[vtrandal]

I use only Linux.

[Scott Morrison]

The other advantage of the instructions is that they give you a pre-compiled copy of mathlib. You can of course compile mathlib yourself once you have Lean up and running, but it's about 100 minutes (single core), so usually preferable to avoid doing yourself.

[Mario Carneiro]

to clarify scott's parenthetical, lean is multithreaded and very parallelizable so if you have more cores it will scale well

[vtrandal]

What is VS Code? I said, "I use only Linux," because I assumed VS Code is a Microsoft thing (VS as in Visual Studio).

[Patrick Massot]

https://code.visualstudio.com/download

[Patrick Massot]

You can use it on Linux

[Patrick Massot]

And really, if you simply want to have a look at Lean, compiling everything from source is purely masochistic.

[Patrick Massot]

On https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian.md you can find a one line install procedure that allow you to play with Lean after 1 minute wait.

[vtrandal]

Thanks, Patrick. I am compiling leanprover from source as a preliminary step to modifying the source code.

[Mario Carneiro]

in that case you should definitely use the community edition of lean

[vtrandal]

Mario, I probably will do that very soon (when I'm ready for an infrastructure).

[vtrandal]

Many thanks to everyone who answered my questions: Kevin, Scott, Patrick, Mario (I hope I did not forget anyone). It's indeed a privilege to be able to ask questions and get help here. Thank you.

[Marko Grdinić]

Hello. Windows user here.

I've gotten Lean up and running already with VS Code. Because I had no idea ahead of time that the plugin would offer to install Lean itself, rather than letting the plugin install elan, I got the binaries ahead of time and pointed the plugin at it instead. So that is all fine and good.

However, I am having difficulty figuring out how to install the Lean mathlib. Yes, I know that there are install instructions here: https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md. However, I am reluctant to go all the way with them for the following reasons.

All the installation instructions are essentially messing around with a Linux shell that I am not familiar with. I am somewhat familiar with the Windows Powershell, but now with the Bash shell and I have no idea what most of these commands do.

To show why this is an issue...suppose I open that Git Bash shell and run curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh. Will this install elan somewhere even though I already have Lean installed? If I do not do this, will it break one of the future steps?

Then the instructions say to install Python. I already have several Python 3 versions in my system (such as from Visual Studio's Anaconda install), and do not want to add any more to PATH. Right now the one that I have in PATH is 2.7 which is linked to Emacs. If I change that to 3.7 will it break the Emacs installation?

At any rate, what I wrote is moot as running curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash which I anticipate should get the compiled library and put it I-do-not-know-where fails. Even if I put one of the Python 3 version into PATH, it fails to detect it from the shell, offers to install it and when I agree runs into issues with Chocolatey (which is kind of like apt-get for Windows) and aborts after too many errors. At first it asks me to go into administrator mode, but fails from there too with a huge pileup of text. I could paste it here, but I do not think that would get us anywhere constructive.

I'd like to have some clear instruction on how to install the library starting with cloning the repo and moving from there. I hate the Linux style of installation where I am forced to mess with configuration files by hand and playing around with weird commands. Every time I tried something like that it has been an incredible waste of time to get the tools to work as it is now.

I already tried just separating the folders inside src from the rest and putting them into the LEAN_PATH environment variable, but that is not working for me even though it seems them in autocomplete. It keeps looking for the init file and there are some errors with line endings apparently.

What should I do here?

[Kevin Buzzard]

Why not just try installing Lean and mathlib following the instructions on the mathlib page (the thing you don't want to do) and just optimistically hope that it doesn't break anything which you've already set up? I'm sure that we would be keen to hear about any breakage (and would fix the scripts if possible). You don't have to understand the command line incantations, you just have to do what you're told. You do this every time you click "install this thing" on Windows and it replies "sure, type in your admin password and I'll sort it out". Surely every time you install some other software on Windows you don't ask exactly what it is doing? You will have to engage with the command line here, every time you clone a lean project from github you will have to type some incantations on the command line to make the project download the correct version of mathlib and then download all the binary mathlib files which mean you don't have to spend 15 minutes with your CPU on 100% while it compiles. An uncompiled mathlib is very painful. You don't just "download mathlib", that's not how it works. You work on a project, and the project has its own mathlib, and this mathlib needs to be compiled or it is painful. That's what all the magic incantations will make easy.

[Mario Carneiro]

If you don't want to fiddle with configuration stuff, then Kevin's suggestion of just starting from scratch using the mathlib install instructions are the right idea. Issues always come up due to system configuration when you try to "save time" by using what you already have instead of what the scripts are expecting. You can go this route but in that case I wouldn't use any of the scripts, I would use the underlying commands

[Kevin Buzzard]

While we're here, can we point new users to any example of a simple project (i.e. not the perfectoid project) with mathlib as a dependency (i.e. not mathlib) and clear installation instructions? Is there one kicking around somewhere?

[Kevin Buzzard]

Oh! Maybe this one https://github.com/ImperialCollegeLondon/M40001_lean will do for now. This is rather less intimidating.

[Alex J. Best]

I think whatever example project should have some non-trivial mathlib imports, so people can see how that works, I didn't see any in MA0001, maybe https://github.com/ImperialCollegeLondon/M1P1-lean is better in that sense (and less mathematically intense than perfectoids)

[Kevin Buzzard]

I added installation instructions to that project (and bumped mathlib to the point where update-mathlib worked). I will resurrect this project this year I guess.

[Kevin Buzzard]

I even got the project compiling again ;-)

[Marko Grdinić]

@Kevin Buzzard I did as you suggested and the installation did go through, almost without a hitch.

leanpkg new my_project
cd my_project
leanpkg add leanprover-community/mathlib
update-mathlib

For some reason the shell is not recognizing the update-mathlib command. But though it took it a while to do what it needs to under the hood in order to go through with the import, the test fragment seems to be working.

What is update-mathlib supposed to be doing? Is it a problem that I haven't done that step properly?

[Marko Grdinić]

Also it is strange that a library would be harder to install than the language itself. Just what is going on that makes it so complicated?

[Kevin Buzzard]

Yup. update-mathlib is a custom script installed by the incantations that you ignore, which takes a project, looks at which version of mathlib it compiles with, and then fetches precompiled binaries from a stash in the cloud and downloads them and puts them in the right place. Saves you 15 minutes of 100% CPU hammering.

[Kevin Buzzard]

It's not harder to install, you can compile the project yourself without update-mathlib, just make sure your device is plugged into the mains and you have something else to do for 30 minutes, and every time the maintainers decide to bump the version of mathlib you'll have the same problem.

[Reid Barton]

Well, since it's your own project in this case, it's really every time you decide to bump to the newest version of mathlib, but otherwise yeah.

[Kevin Buzzard]

You could instead just go into the project and type lean --make

[Kevin Buzzard]

you should get some warnings (because not all proofs are complete) but no errors.

[Kevin Buzzard]

The extra work is not because installing the library is hard, it's because compiling the library is painful. The extra stuff is to make your life easier.

[Marko Grdinić]

Any idea why update-mathlib is not being recognized by the shell? I did follow the instructions exactly as far as I could this time.

Why would compiling the library be painful? I remember in one of the slides reading that the array data type is implemented in C++. Does the library have C++ dependencies it needs to compile directly or something?

[Kevin Buzzard]

Oh -- you did the incantations? Then it should work. Compiling the library is painful because it is a large amount of Lean code and it's got to the point where it's painful. There are some short proofs that take 20 seconds to compile because mathlib pushes Lean's type class resolution system to its limits.

[Kevin Buzzard]

Very short Lean files can force the kernel to deal with absolutely gigantic terms, because mathematics is good at bundling stuff like fields up into neat packages but Lean has to deal with what's actually going on.

[Kevin Buzzard]

Lean 4 might change all this, but Lean 4 is not quite ready.

[Kevin Buzzard]

(I mean, it's ready to play around with, but there is no tactic framework and no type class resolution system)

[Mario Carneiro]

you might have to write ./update-mathlib or ./update-mathlib.sh

[Mario Carneiro]

(I assume it's a shell script)

[Kevin Buzzard]

If Marko has followed the instructions to the letter it should just all work, right? Do you know precisely which line installs the update-mathlib script? Marko could try that one again and report on output.

[Mario Carneiro]

The issue isn't C++ dependencies, it is Lean itself. Mathlib is composed of several hundred large lean files, which all need to be run through lean. This involves running a bunch of tactics and each file takes a few seconds to minutes

[Marko Grdinić]

Marko@Lain MINGW64 /e/TheoremProving/lean/my_project (lean-3.4.2)
$ ./update-mathlib
bash: ./update-mathlib: No such file or directory

Marko@Lain MINGW64 /e/TheoremProving/lean/my_project (lean-3.4.2)
$ ./update-mathlib.sh
bash: ./update-mathlib.sh: No such file or directory

Indeed, the files are not in the directory just as the errors indicated. On Windows the ./ prefix means to run the thing in the current dir. I am not sure how it is on Linux.

[Mario Carneiro]

it means that in linux too

[Mario Carneiro]

I guess you need to add something to your PATH

[Kevin Buzzard]

What is the output of curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash ? That's surely the line that installs update-mathlib :D

[Mario Carneiro]

reading the script, it looks like it tells you to run source ~/.profile at the end

[Marko Grdinić]

@Mario Carneiro

The issue isn't C++ dependencies, it is Lean itself. Mathlib is composed of several hundred large lean files, which all need to be run through lean. This involves running a bunch of tactics and each file takes a few seconds to minutes

If it is like that, then I could have let the VS Code plugin install elan directly rather than running the scripts? Is Python also a real dependency?

@Kevin Buzzard

$ curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash
Installing python dependencies (at user level)
/c/Users/Marko/AppData/Local/Programs/Python/Python37-32/Scripts/pip3
Requirement already up-to-date: setuptools in c:\users\marko\appdata\roaming\python\python37\site-packages (41.4.0)
You are using pip version 19.0.3, however version 19.2.3 is available.
You should consider upgrading via the 'python -m pip install --upgrade pip' command.
Requirement already up-to-date: toml in c:\users\marko\appdata\roaming\python\python37\site-packages (0.10.0)
Requirement already up-to-date: PyGithub in c:\users\marko\appdata\roaming\python\python37\site-packages (1.43.8)
Requirement already up-to-date: certifi in c:\users\marko\appdata\roaming\python\python37\site-packages (2019.9.11)
Requirement already up-to-date: gitpython in c:\users\marko\appdata\roaming\python\python37\site-packages (3.0.3)
Requirement already up-to-date: requests in c:\users\marko\appdata\roaming\python\python37\site-packages (2.22.0)
Requirement already satisfied, skipping upgrade: deprecated in c:\users\marko\appdata\roaming\python\python37\site-packages (from PyGithub) (1.2.6)
Requirement already satisfied, skipping upgrade: pyjwt in c:\users\marko\appdata\roaming\python\python37\site-packages (from PyGithub) (1.7.1)
Requirement already satisfied, skipping upgrade: gitdb2>=2.0.0 in c:\users\marko\appdata\roaming\python\python37\site-packages (from gitpython) (2.0.6)
Requirement already satisfied, skipping upgrade: chardet<3.1.0,>=3.0.2 in c:\users\marko\appdata\roaming\python\python37\site-packages (from requests) (3.0.4)
Requirement already satisfied, skipping upgrade: urllib3!=1.25.0,!=1.25.1,<1.26,>=1.21.1 in c:\users\marko\appdata\roaming\python\python37\site-packages (from requests) (1.25.6)
Requirement already satisfied, skipping upgrade: idna<2.9,>=2.5 in c:\users\marko\appdata\roaming\python\python37\site-packages (from requests) (2.8)
Requirement already satisfied, skipping upgrade: wrapt<2,>=1.10 in c:\users\marko\appdata\roaming\python\python37\site-packages (from deprecated->PyGithub) (1.11.2)
Requirement already satisfied, skipping upgrade: smmap2>=2.0.0 in c:\users\marko\appdata\roaming\python\python37\site-packages (from gitdb2>=2.0.0->gitpython) (2.0.5)
You are using pip version 19.0.3, however version 19.2.3 is available.
You should consider upgrading via the 'python -m pip install --upgrade pip' command.
Fetching the update-mathlib script
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100  3255  100  3255    0     0   3011      0  0:00:01  0:00:01 --:--:--  3011
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100  4961  100  4961    0     0  14421      0 --:--:-- --:--:-- --:--:-- 14421
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100   508  100   508    0     0   1439      0 --:--:-- --:--:-- --:--:--  1435
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100  1241  100  1241    0     0   3760      0 --:--:-- --:--:-- --:--:--  3760
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100  1078  100  1078    0     0   3053      0 --:--:-- --:--:-- --:--:--  3053
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100   493  100   493    0     0   1507      0 --:--:-- --:--:-- --:--:--  1507
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100   475  100   475    0     0   1422      0 --:--:-- --:--:-- --:--:--  1422
installing it in $HOME/.mathlib/bin
mathlib scripts are already added to $PATH in .profile

Hmmmm...is mathlib scripts are already added to $PATH in .profile the part where the scripts should be located. I'll check it out. Let me try restarting first. Be right back.

[Kevin Buzzard]

Just source .profile

[Kevin Buzzard]

Or restarting -- that will hopefully also fix it.

[Mario Carneiro]

restarting your shell, that is

[Mario Carneiro]

I don't think you have to restart your session

[Marko Grdinić]

I am back. I just finished restarting. Either way, it still cannot find update-mathlib unfortunately. To make matters worse, it seems that Lean is not caching the library and it is taking long to typecheck that basic fragment. You can really feel the effort based on how long it takes the shell to react to my typing. So I am going to have to figure out how to do this. Any advice how I can go from here?

I see that update-mathlib is a Python script so I guess that answers one of my questions.

[Kevin Buzzard]

If the issue is as simple as not being able to find the python file then post your PATH variable (in linux it would be something like echo $PATH) and see if you can use the Windows search tools to find a file called update-mathlib somewhere on your system.

[Rob Lewis]

update-mathlib was installed to ~/.mathlib/bin/ on my system. Does that directory exist for you? Is the script there?

[Kevin Buzzard]

If you just type update-mathlib then the idea is that the OS looks through all the directories in the $PATH system variable and sees if it can find a file called update-mathlib in any of them.

[Kevin Buzzard]

Judging by the output of what you posted above, $HOME/.mathlib/bin would be a good place to start (and Rob confirms that it's there in his).

[Marko Grdinić]

@Rob Lewis

Yeah, it is there. Echoing the PATH, it does not seem that .profile is adding the required directories to PATH. Let me try adding it to PATH manually.

[Kevin Buzzard]

source ~/.profile should add it automatically.

[Kevin Buzzard]

Are you using the terminal which is recommended by the mathlib install instructions, by the way?

[Kevin Buzzard]

We recommend that you use git bash and not msys2, since installing the supporting tools (below) causes issues in msys2.

[Marko Grdinić]

@Kevin Buzzard Yes. I am using it from VS Code rather than directly though.

[Marko Grdinić]

As an aside, for some reason the which command got broken in the Powershell by the recent installations. I have no idea what to make of that.

[Kevin Buzzard]

I have no idea whether that changes things but it seems to me that we have located the source of the problem.

[Kevin Buzzard]

You could just run update-mathlib directly from that path, e.g. by typing ~/.mathlib/bin/update-mathlib from the root of the project folder.

[Kevin Buzzard]

I have absolutely no understanding of path variables in windows nor of which incantations of shells read .profile files but if the python file is there, just run it in the root directory of the project folder [I see from the above that you seem to have a Lean project].

[Kevin Buzzard]

Your project folder should have files in it called things like leanpkg.toml and leanpkg.path and directories _target and src by this point.

[Marko Grdinić]

@Kevin Buzzard Thank you very much for the help so far.

I've added it to PATH and have just run update-mathlib. We'll see how it goes. I'll try figuring out why .profile is not working after that.

[Kevin Buzzard]

And the output looked good? If so then create a file in src called test.lean and write something like import data.real.basic at the top. It's essential that you used the "open folder" command in VS Code and opened the project folder.

[Kevin Buzzard]

If test.lean gives you an error saying it can't find the import, that's bad. If it gives you an error saying "can't find the import data.real.basi" and then there is an orange bar at the left side of the window which doesn't go away, that's bad (it means Lean did find data.real.basic but will now spend 2 minutes compiling it). If the orange bar goes away after a few seconds, that's good.

[Kevin Buzzard]

(the reason for the missing c is that when you were typing, Lean was compiling frantically, and the error was the last import that failed)

[Marko Grdinić]

@Kevin Buzzard That is what I've been doing.

Marko@Lain MINGW64 /e/TheoremProving/lean/my_project (lean-3.4.2)
$ "C:/Program Files (x86)/Microsoft Visual Studio/Shared/Anaconda3_64/Scripts/activate"
/c/Program Files (x86)/Microsoft Visual Studio/Shared/Anaconda3_64/etc/profile.d/conda.sh: line 56: /c/Program: No such file or directory

Marko@Lain MINGW64 /e/TheoremProving/lean/my_project (lean-3.4.2)
$ conda activate Anaconda3_64
bash: conda: command not found

Marko@Lain MINGW64 /e/TheoremProving/lean/my_project (lean-3.4.2)

This is what happens when I try to open a terminal in VS Code right now. It seems there is something left over from the old version of the shell where it is setup to activate the Anaconda distro. Things like this happens when you just plop stuff in. Maybe that is why it did not just work out of the box.

[Kevin Buzzard]

You do not need to be opening terminals in VS Code if you have run update-mathlib. Your terminal days are over.

[Kevin Buzzard]

The fact that your OS cannot deal with spaces in path names is not my problem ;-)

[Marko Grdinić]

It can deal with spaces in path names just fine, I have no idea why you had issues with that. :)

I made a mistake trying to run update-mathlib in the root. What happened was that it seemed like it has started running something but there was no output. I see now that when I run it in the project folder I actually get some response.

Marko@Lain MINGW64 ~
$ cd E:/TheoremProving/lean/my_project

Marko@Lain MINGW64 /e/TheoremProving/lean/my_project (lean-3.4.2)
$ update-mathlib
Info: No github section found in 'git config', we will use GitHub with no authentication
Querying GitHub...
Downloading nightly...
Extracting nightly...

This should be fine, right? Let me give it a try.

[Kevin Buzzard]

Your output in the last thing you pasted had an error caused by a space in a file name.

[Kevin Buzzard]

line 56: /c/Program: No such file or directory

[Kevin Buzzard]

Yes, the update-mathlib output looks perfect. I am cautiously optimistic.

[Kevin Buzzard]

We do have a Windows machine at home and I actually renamed C:\Program Files to C:\Program_Files because I got so sick of that issue

[Mario Carneiro]

wow, I'm surprised you didn't brick your system doing that

[Kevin Buzzard]

Oh I haven't explained what I did correctly. I'm sure it would have bricked it. What I did was made a new directory Program_Files right at the start and then installed everything into that.

[Marko Grdinić]

Oh, lol. I assure you, native Windows programs do not have that issue.

At any rate, it seems that now the project is loading and typechecking instantly. Great.

I am going to dig around a bit more to see if I can figure out why .profile is not adding the directory to PATH properly.

[Kevin Buzzard]

:D . I'm off for lunch because I can't help with anything else ;-) Happy leaning!

[Marko Grdinić]

Ok, I see what is going on.

(Git shell run directly from the shortcut)

Marko@Lain MINGW64 ~
$ echo $PATH
/c/Users/Marko/.elan/bin:/c/Users/Marko/.mathlib/bin:/c/Users/Marko/bin:/mingw64/bin:/usr/local/bin:/usr/bin:/bin:/mingw64/bin:/usr/bin:/c/Users/Marko/bin:/c/emacs-26.2-x8...

(Git shell run via VS Code)

$ echo $PATH
/mingw64/bin:/usr/bin:/c/Users/Marko/bin:/c/emacs-26.2-x86_64/bin...

(Powershell)

PS C:\Users\Marko\.mathlib\bin> $Env:Path
C:\emacs-26.2-x86_64\bin....

I replaced the cutoff parts with ... by hand. It seems that .profile only gets run when Git Bash is ran via the shortcut. Running it from VS Code will not have the .elan and mathlib directories be added to the PATH variable. That explains that.

With this I've finally successfully setup the project. I started work on this at 10am and it is nearly 3pm now. It should definitely be a priority for the devs to make it so that one can just clone the repo and point the compiler at the library. Even if it would take 10m to compile, that would still beat having to go through all these hoops.

I understand that the reason it took so long is partly my fault as I've given into the temptation of trying to save time by not following the instruction properly, but good installation instructions should not produce such temptation in the first place.

Nonetheless, I let me offer my thanks for helping me with this once again. Cyao.

[Mario Carneiro]

it takes closer to an hour to compile

[Mario Carneiro]

but I agree that we should have directions on how to compile mathlib yourself

[Mario Carneiro]

I guess there is not much to say though; this should work:

leanpkg new my_project
cd my_project
leanpkg add leanprover-community/mathlib
lean --make .target/mathlib/src

[Mario Carneiro]

you don't even have to clone mathlib first, leanpkg takes care of that

[Mario Carneiro]

it's more an issue of getting the tooling environment set up usually

[Nicolás Ojeda Bär]

For what is worth, this is what I did, works nicely and does not require setting up your PATH, etc.

[Patrick Massot]

With this I've finally successfully setup the project. I started work on this at 10am and it is nearly 3pm now. It should definitely be a priority for the devs to make it so that one can just clone the repo and point the compiler at the library. Even if it would take 10m to compile, that would still beat having to go through all these hoops.

Hi, I think you missed a couple of important points. First who do you think are "devs" here? Do you mean the creator of Lean? He is a scholar engaged in a ten years research project, and he wrote everywhere that Lean is not ready for unadventurous users. Taking care of users has never been his job, and it will probably never be. You can have a look at https://leanprover.github.io/documentation/ for instance, and the FAQ linked there.

Then there is the user community which you can meet here, and maintains everything at https://github.com/leanprover-community/, in particular mathlib. We do think Lean is already very nice to use, and we try to help people doing so. There are two kinds of users that are easy to help. Clueless users who blindly follows the instructions, and it works. Power users won't follow any instructions but will read the source code of scripts that clueless users are instructed to run, understand what they do, and do whatever they want (including compiling Lean itself from sources). This also work. Clueless users that refuse to follow instructions are much harder to help, especially when they use an exotic OS.

That being said, we still have a lot of work to do to improve installation instructions. And I'm sure that Kevin and Mario are happy that they could help you. But complaining that it took too long to satisfy you is probably not the wisest thing to do.

[Mario Carneiro]

personally I find 5 hours to troubleshoot and fix a configuration error on an unfamiliar software to be about average

[Marc Huisinga]

i'm also running windows and i use the git terminal + leanpkg for setting stuff up. i've found that building mathlib isn't so bad if you only do it once every few months

[Patrick Massot]

Do you use only one Lean project?

[Marc Huisinga]

yes ;)

[Patrick Massot]

We should certainly have instructions for people like you.

[Marc Huisinga]

so far, i've installed lean on three windows machines and iirc my process is the following:
- install git
- install elan via sebastian's elan-init.sh
- install python3 (i did not have to do any file renaming as suggested in the mathlib windows.md so far)
- install vscode and the leanprover extension
- set up dependencies via leanpkg
- run leanpkg build

[Andrew Ashworth]

I am surprised leanpkg and lean --make is not the default instruction. In some ways distributing binary artifacts via shell script is kind of weird, at least when it comes to compiled languages. Although I totally understand the motivation. I have been using Lean+MinGW for years now with no problems.

[Andrew Ashworth]

It has been a few months since I have recompiled mathlib. I am not at Lean right now, but isn't there an option to do a user-wide install of mathlib? Then it is compile once, use in many projects

[Andrew Ashworth]

Of course, avoiding compilation time is a desirable feature. I wonder if modifications to leanpkg would be welcome at this point? Properly speaking, this should be a responsibility of the package manager

[Andrew Ashworth]

Also, are .olean files even portable across systems? I recall reading that there were issues on ARM regarding this.

[Mario Carneiro]

There were rumors about that but after writing olean-rs I can't find anything processor dependent in it, and we've been sharing olean files for a while now without issue

[Reid Barton]

The most likely thing would be ints stored in native byte order

[Mario Carneiro]

is ARM big endian? I think not

[Mario Carneiro]

it's bi-endian...?

[Reid Barton]

I think it depends, maybe? I forget

[Mario Carneiro]

LGBT processors

[Andrew Ashworth]

ah, i found the original issue: https://github.com/leanprover/lean/issues/1679

[Reid Barton]

this bug looks amazing