3.4, elan, and mathlib

Stream: general

[Johan Commelin]

I just installed elan. Succesfully it seems. I then ran mkdir ~/mess/leantest and inside that directory, I ran elan toolchain install nightly. This provided me with a leanpkg command, and I ran leanpkg add https://github.com/leanprover/mathlib. After cloning from github, it complained cannot find revision lean-3.4.0 in repository _target/deps/mathlib. I guess this is somehow expected, because mathlib is not 3.4.0 ready. Right?

[Johan Commelin]

So which permutation of command should I run, to get the most up to date version of lean + mathlib on my box?

[Mario Carneiro]

do you have a leanpkg.toml file? What is in it?

[Sebastian Ullrich]

You're probably using Lean stable, which is installed by elan by default - see lean -v or elan show

[Mario Carneiro]

What do I need to do to make this work?

[Mario Carneiro]

Is it just adding a tag with the name lean-3.4.0?

[Johan Commelin]

elan show
installed toolchains
--------------------

stable-x86_64-unknown-linux-gnu
nightly-x86_64-unknown-linux-gnu

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

stable-x86_64-unknown-linux-gnu (default)
Lean (version 3.4.0, commit 4be96eaaaf71, Release)

[Johan Commelin]

I do not have a .toml file

[Johan Commelin]

Should I write this myself?

[Sebastian Ullrich]

leanpkg init <package name> will create it for you. You can use leanpkg +nightly init ... to set the Lean version to a nightly, but I'm not sure there is any point in encouraging users to use nightlies any more. @Mario Carneiro What do you think?

[Johan Commelin]

Ok, I see

[Johan Commelin]

Is there a concensus?

[Sebastian Ullrich]

Not yet I think. Right now, stable and nightly are functionally the same Lean version.

[Mario Carneiro]

Assuming lean is completely frozen now, I guess we can move to building against 3.4.0, but I expect some occasional bugfixes will come along, and then I will want to go back to nightlies

[Johan Commelin]

I hope that, now that 3.4 is out, there is a stable way to get everything working together

[Johan Commelin]

And then we document this, so that users know which 5 commands to run in a fresh directory to get a lean project up and running

[Mario Carneiro]

For now, though, you want to make sure that your lean version is nightly-2018-04-06 since that's what mathlib master is using

[Johan Commelin]

Ok, and how should I make sure I get that nightly, using elan

[Sebastian Ullrich]

@Mario Carneiro Yeah, I guess a tag should work. Not sure if force-updating it will work too :) .

[Johan Commelin]

(Because it seems using elan is wise)

[Mario Carneiro]

I am not the elan guru in this conversation :)

[Sebastian Ullrich]

leanpkg +nightly-2018-04-06 init mypackage

[Johan Commelin]

@Mario Carneiro When do you expect mathlib to use 3.4? (No pressure...)

[Mario Carneiro]

Probably tomorrow or the day after, when I get a chance to sit down and look at the changes

[Johan Commelin]

@Sebastian Ullrich But to have a leanpkg command, I already need to first run an elan command, right?

[Johan Commelin]

Because elan provides me with a leanpkg

[Sebastian Ullrich]

No, you just need to have elan installed

[Sebastian Ullrich]

It's the same as elan run nightly-2018-04-06 leanpkg init mypackage, if you like that better :)

[Johan Commelin]

Ok, so I empty my leantest directory

[Johan Commelin]

And I get

[Johan Commelin]

$ elan run nightly-2018-04-06 leanpkg init leantest
error: toolchain 'nightly-2018-04-06-x86_64-unknown-linux-gnu' is not installed

[Sebastian Ullrich]

Oops, I was hoping this worked... then you need to run elan toolchain install nightly-2018-04-06 first

[Johan Commelin]

Ok, I'll try that

[Johan Commelin]

My first goal now, is to write a 10-line readme, that will explain how to start a fresh project.

[Johan Commelin]

Including VScode integration, I hope

[Johan Commelin]

@Sebastian Ullrich That worked. And now I also ran elan run nightly-2018-04-06 leanpkg init leantest

[Johan Commelin]

Should the next step be leanpkg add https://github.com/leanprover/mathlib ?

[Sebastian Ullrich]

Yes

[Mario Carneiro]

is there a way to get the version number from mathlib?

[Sebastian Ullrich]

You mean the lean_version?

[Mario Carneiro]

yes

[Johan Commelin]

Ok, that worked. I assume now I should run leanpkg build. Right?

[Mario Carneiro]

The mathlib elan setup doesn't say anything about lean versions

[Mario Carneiro]

@Johan Commelin If you get that 10 line startup script working, pr it to the mathlib readme

[Sebastian Ullrich]

@Johan Commelin That should work, but not do much. Lean only builds the part of the dependencies you actually import in your src directory

[Johan Commelin]

Ok, so there is no need to run leanpkg build right now?

[Johan Commelin]

Then I won't do it

[Johan Commelin]

@Mario Carneiro Ok, I'll do that. Once I've got it working (^;

[Sebastian Ullrich]

I was surprised you were able to run leanpkg add before initializing the package. I guess you got a "failed to open file 'leanpkg.toml'" only at the very end? Pretty much a bug in leanpkg, oh well.

[Johan Commelin]

@Sebastian Ullrich I love breaking things. Hehe

[Johan Commelin]

Right, so I did not run leanpkg build. Only fired up VScode

[Johan Commelin]

It says No Lean file active in the Lean messages, after I opened a .lean file

[Moses Schönfinkel]

Clicking anywhere in the file usually fixes this for me.

[Johan Commelin]

Ok, that works. Never had to do that...

[Sebastian Ullrich]

@Mario Carneiro Not sure what you're trying to achieve. The Travis build will select the correct version from lean_version automatically.

[Mario Carneiro]

well, I'm mildly surprised that the default setup gave the wrong version of lean for mathlib

[Mario Carneiro]

I want a short command or script to give to a newbie that wants the latest version of mathlib and a compatible version of lean

[Mario Carneiro]

I'd prefer that the script not contain the literal string nightly-2018-04-06 since that ages

[Johan Commelin]

@Sebastian Ullrich But I need to tell VScode to use the correct version of lean, right? So I edit the settings, to point it to ~/.elan/toolchains/nightly-2018-04-06-x86_64-unknown-linux-gnu/bin/lean, is that correct?

[Sebastian Ullrich]

@Johan Commelin I've only tested emacs so far, but specifying ~/.elan/bin/lean should work

[Johan Commelin]

Lean: Unable to start the Lean server process: Error: spawn ~/.elan/bin/lean ENOENT The lean.executablePath may be incorrect, make sure it is a valid Lean executable

[Johan Commelin]

Alas, it is still complaining

[Mario Carneiro]

put .exe at the end?

[Sebastian Ullrich]

On Linux?

[Sebastian Ullrich]

Maybe it doesn't like the ~

[Johan Commelin]

Yes, I'm on linux

[Johan Commelin]

Ok, that seems to have done it. I expanded the ~ to my homedir

[Sebastian Ullrich]

Nice, good to know

[Johan Commelin]

Ok, I'm now try to compile Kevin's result that Spec(R) is quasi-compact

[Johan Commelin]

If that works, then I'll write the little readme

[Johan Commelin]

Also, is there a way to tell lean not to use all my CPU threads?

[Johan Commelin]

mkdir leantest/
cd leantest/
elan run nightly-2018-04-06 leanpkg init leantest
elan toolchain install nightly-2018-04-06
elan run nightly-2018-04-06 leanpkg init leantest
ls
ls -a
leanpkg add https://github.com/leanprover/mathlib
leanpkg add https://github.com/kbuzzard/lean-stacks-project
ls
elan show

# Change VScode settings to point to "/home/<user>/.elan/bin/lean"

[Johan Commelin]

That is my current bash history

[Johan Commelin]

So, I'll clean it up, and write a bit of details. But I thought I would log it here as well

[Sebastian Ullrich]

@Mario Carneiro So, this looks like a chicken and egg problem - when selecting the Lean version for creating the package, we don't know what dependencies the user will install yet. Well, it doesn't really matter what version to use for creating the package, so we could suggest to the user to change their Lean version after the fact when adding mathlib. I'm planning to do the same on leanpkg upgrade; we can also discuss this at https://github.com/Kha/elan/issues/5

[Johan Commelin]

O.o.....

Lean: Server has stopped due to signal SIGSEGV

That doesn't sound good...

[Kevin Buzzard]

Johan -- one possibility is that you just get everything working in the old way, and just wait until mathlib is running with 3.4.

[Kevin Buzzard]

The reason this might be useful is that what we will ultimately really need

[Kevin Buzzard]

is a clear and concise set of instructions

[Kevin Buzzard]

on how to get Lean 3.4 and mathlib running.

[Kevin Buzzard]

And at the minute mathlib doesn't work with Lean 3.4, and elan still has teething troubles

[Kevin Buzzard]

in other words, I guess what I'm saying is that I am waiting until mathlib works with Lean 3.4 before I start thinking about writing down some succinct explanation of how to use elan

[Kevin Buzzard]

and for me there is no hurry because I have a set-up that works without elan

[Kevin Buzzard]

OTOH I'm sure Sebastian is appreciating your comments on elan.

[Kevin Buzzard]

As for the segv

[Kevin Buzzard]

you do occasionally get these, although they are quite rare

[Kevin Buzzard]

a good way of getting them is to compile a project, thus getting a bunch of .olean files, and then changing the version of Lean you're using

[Kevin Buzzard]

so the first thing you need to do is to rule this out

[Kevin Buzzard]

and the second big question is whether you can reliably reproduce the segfault

[Kevin Buzzard]

and if you can, then you get an achievement

[Kevin Buzzard]

and you're allowed to post an issue to the lean repo

[Kevin Buzzard]

I've had a couple recently but I couldn't reproduce them, annoyingly

[Kevin Buzzard]

(the moment I get one, I hit ctrl-Z to go back a bit, ctrl-shift-P Lean:restart to restart Lean, and then try typing exactly the same keys again)

[Kevin Buzzard]

I am really really looking forwards to the stability of 3.4 + mathlib, but until then I have plenty to do :-)

[Sebastian Ullrich]

Just to be clear, any issues happening _after_ Lean was started successfully should not be elan's fault :)

[Johan Commelin]

So find . -name *.olean finds nothing. Which means the first option is ruled out. I guess. Now I will start the backtracking.

[Sebastian Ullrich]

The .olean version mismatch problem has been fixed for quite some time

[Johan Commelin]

Can Lean segfault if it runs out of memory? I opened a file from Kevin's lean-stacks-project and I had not compiled anything before. I only have 4GB in my rusty Thinkpad (no swap). So I think that Lean maybe ran out of memory.

[Sebastian Ullrich]

There have been many ways for Lean to segfault so far, but that one would be new :)

[Johan Commelin]

So, should I run leanpkg build or something similar? Ought that work?

[Sebastian Ullrich]

Worth a try, at least then you know it's easily reproducible

[Johan Commelin]

$ leanpkg build
configuring leantest 0.1
mathlib: trying to update _target/deps/mathlib to revision 7d1ab388bb097db5d631d11892e8f110e1f2e9cd
> git checkout --detach 7d1ab388bb097db5d631d11892e8f110e1f2e9cd    # in directory _target/deps/mathlib
HEAD is now at 7d1ab38 feat(list/basic,...): minor modifications & additions
lean-stacks-project: trying to update _target/deps/lean-stacks-project to revision a2204862a0c20c4ea4f98d5685c1a51a3b0279d3
> git checkout --detach a2204862a0c20c4ea4f98d5685c1a51a3b0279d3    # in directory _target/deps/lean-stacks-project
HEAD is now at a220486 Merge branch 'master' of github.com:kbuzzard/lean-stacks-project
> lean --make src

[Johan Commelin]

This completed immediately...

[Johan Commelin]

Doesn't do any compiling at all

[Sebastian Ullrich]

Is your segfaulting file saved in the src directory?

[Johan Commelin]

No, the src/ dir is empty

[Sebastian Ullrich]

You should save your Lean files in src, as described in https://leanprover.github.io/reference/using_lean.html#directory-layout

[Johan Commelin]

Sorry, I'm completely confused. As you can see from my log above, I only ran leanpkg add to add mathlib and lean-stacks-project. Both are added to _target/deps/. The leave src/ empty. What am I doing wrong?

[Kevin Buzzard]

Here's how you're supposed to run the stacks project.

[Kevin Buzzard]

First, clone the stacks project.

[Kevin Buzzard]

Then make it into a lean package with some leanpkg command which I forgot

[Kevin Buzzard]

then build it

[Kevin Buzzard]

Here's how you're supposed to make a new project with the stacks project as a dependency

[Kevin Buzzard]

First make a directory for your new project

[Johan Commelin]

Ok, I see. I thought you had to leanpkg add it

[Kevin Buzzard]

then use leanpkg add to add the stacks project

[Kevin Buzzard]

I think I've got it straight.

[Johan Commelin]

Aha, I hope this helps...

[Kevin Buzzard]

On behalf of the community I apologise for the lack of docs and the general difficulty of finding the docs you need

[Kevin Buzzard]

we are working on this problem

[Kevin Buzzard]

What happens in practice is that Sebastian does a really good job of writing all these package managers

[Kevin Buzzard]

and then he explains how things work here

[Kevin Buzzard]

and everyone learns

[Kevin Buzzard]

and then either stuff doesn't get written, or stuff gets written but in some place you might not expect, or stuff doesn't get written and then the older stuff is written but out of date and wrong.

[Johan Commelin]

Right, I'll try to figure out the command to turn the clone into a lean package

[Patrick Massot]

Yes we are working on it. I really for big improvements in the next few weeks

[Kevin Buzzard]

To make matters worse, and by "worse" I mean "better", we now have elan, which is something else

[Johan Commelin]

@Kevin Buzzard Could it be that you mean leanpkg configure to download the dependencies?

[Patrick Massot]

Mathlib goes 3.4, elan matures, TPIL and refman get updated and everything will become much easier

[Kevin Buzzard]

and the most comprehensive docs on elan are obtained by searching for elan here :-)

[Kevin Buzzard]

"Mathlib goes 3.4" -- here's hoping!

[Kevin Buzzard]

Presumably you noticed the rather terrifying-looking stumbling block

[Kevin Buzzard]

One thing I love about Lean is that we are free to add various type annotations everywhere if we get confused

[Kevin Buzzard]

and I get confused a lot

[Kevin Buzzard]

@Johan Commelin line 16 of an old commit

[Kevin Buzzard]

https://github.com/leanprover/lean/commit/37bde20d07dc28b7fd3e84a1c768b9ce547bd5a8#diff-93c4834f2a585510be668daf86b8e81fR16

[Kevin Buzzard]

That was when mathlib was called library_dev

[Kevin Buzzard]

When the docs moved into the reference manual, some of those old docs got lost

[Johan Commelin]

Ok, thanks!

[Kevin Buzzard]

You seem to be right -- the "creating new packages" docs survived but the "working on existing packages" para got lost.

[Johan Commelin]

Whoohoo, now leanpkg build is actually doing something!

[Kevin Buzzard]

I would go and have a cup of tea

[Kevin Buzzard]

I would also recommend maximising your console window and using ctrl-(minus key) to minimise your font size

[Kevin Buzzard]

that way successful compilation of a file whose full path is more than 80 characters doesn't result in your terminal being filled with garbage

[Johan Commelin]

I see... I'm already running fullscreen. I'm about to get a computer account at the department, and I'm going to ask for a second screen on my desk.

[Kevin Buzzard]

[and note the message I sent you yesterday about certain files which have errors in as they are WIPs; I know it's a bit unprofessional but I develop on more than one machine and github is just a convenient way to store my half-written files]

[Johan Commelin]

Running VScode on a 12" Thinkpad is horrible

[Kevin Buzzard]

I am absolutely serious when I say

[Kevin Buzzard]

that I run VS Code on a laptop with a medium size screen

[Kevin Buzzard]

and the fact that it was horrible

[Johan Commelin]

@Kevin Buzzard Yes, I saw that message. No problem. I think branches could help you there. You can push WIP branches to github as well.

[Kevin Buzzard]

actually made me bite the bullet and start wearing glasses

[Kevin Buzzard]

and now I have glasses (for reading)

[Kevin Buzzard]

I can just minimise the font to quite small :-)

[Kevin Buzzard]

I am not good at branches yet.

[Kevin Buzzard]

but I am getting there.

[Kevin Buzzard]

I never needed them before because Kenny and Chris work on localised code and don't care if other stuff doesn't compile

[Kevin Buzzard]

and nobody else has ever paid any attention to the project :-)

[Kevin Buzzard]

We are nearly done though.

[Johan Commelin]

and nobody else has ever paid any attention to the project :-)

I'm sorry for being curious

[Johan Commelin]

I should just wait a couple of days (-;

[Kevin Buzzard]

I just this morning pushed a version of tah01HR which contains a concrete endgame

[Kevin Buzzard]

i.e. "we need to prove this lemma and that lemma and then just glue everything together"

[Kevin Buzzard]

I think I am right when I say that mathlib compiles with the nightly of 6th April

[Kevin Buzzard]

and the project should work with that

[Johan Commelin]

So far the compile is doing its job perfectly (-;

[Patrick Massot]

You don't have to guess here, it's right there: https://github.com/leanprover/mathlib/blob/master/leanpkg.toml#L4

[Kevin Buzzard]

aah, another undocumented gem ;-)

[Johan Commelin]

@Patrick Massot Yes, now I only need to convince my laptop of that (-;

[Patrick Massot]

Did you put that same line in your own project leanpkg.toml?

[Kevin Buzzard]

if he cloned my project then it should be there

[Johan Commelin]

Atm I just cloned the lean-stacks-project repo, which has its own toml

[Kevin Buzzard]

So the system does actually work

[Patrick Massot]

what does which leanpkg tells you?

[Kevin Buzzard]

it's just that we need to document it better

[Johan Commelin]

And elan parsed it, and made me use the right version of leanpkg and lean :tada:

[Johan Commelin]

$ which leanpkg
/home/jmc/.elan/bin/leanpkg

[Patrick Massot]

ok, it's all fine

[Patrick Massot]

also, make sure you never ever define a leanpath variable in VScode

[Patrick Massot]

this only leads to confusion

[Johan Commelin]

I set it to /home/jmc/.elan/bin/lean

[Patrick Massot]

You shouldn't

[Johan Commelin]

So what should I do?

[Patrick Massot]

You should simply launch VScode from a terminal where the shell path variable is set correctly (ie which lean points to .elan/bin/lean)

[Patrick Massot]

which will happen if you have source $HOME/.elan/env in your initialization file (.profile or .bashrc or...)

[Johan Commelin]

Ok, that makes sense

[Johan Commelin]

I'll do that from now on

[Kevin Buzzard]

ha ha, I use leanpath all the time; it points to a symlink :-)

[Kevin Buzzard]

Johan -- I haven't used elan at all yet but I just changed the README in lean-stacks-project to explain what I think you just did.

[Kevin Buzzard]

Feel free to submit a PR explaining elan. I have not even attempted to find out whether elan has docs; I have other things to worry about currently :-)

[Johan Commelin]

If my compile succeeds, then the first thing I will do is write some small docs and PR them.

[Patrick Massot]

Let me try something (we'll see if we can PR later). Instruction for a first time user of Lean under linux:

• make sure VScode is installed
• launch VScode and install the Lean extension by clicking the extension icon in the view bar at left and searching for lean. quit VScode for ow
• make sure git and curl are installed, using your distrib package manager
• curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh and type enter when a question is asked. Then add source .elan/env to your shell initialization script, say ~/.bashrc, and source it in the current terminal (or relaunch a new terminal).
• The previous step downloaded the latest stable release, that may be too recent or too old for mathlib, and you really want mathlib. Have a look at https://github.com/leanprover/mathlib/blob/master/leanpkg.toml#L4 to see what is the nightly mathlib currently wants. Say you see nightly-2018-04-06. Then run elan toolchain install nightly-2018-04-06.
• Now we want some playground to experiment. Use elan run nightly-2018-04-06 leanpkg new my_playground. This will create a my_playground directory with a lean project layout.
• Go to that directory and type leanpkg add leanprover/mathlib this will download mathlib and put it inside my_playground/_target/deps,
• At this point you can already create some lean file in my_playground/src, launch VScode, go to and play with Lean by opening the file, typing Ctrl-shift-enter to open Lean message windows, and type, say #check 1 to see the result
• You cant also use import group_theory.subgroup and then #check is_subgroup. But this will use uncompiled version of mathlib, which is very inefficient. If you run leanpkg build from inside my_playground then it will compile only files which are dependencies of mathlib group_theory/subgroup.lean.
• If you want to play more, it's better to compile all mathlib once and for all. You can do this by going into my_playground/_target/deps/mathlib, type lean --makeand go get some coffee.

[Patrick Massot]

That being said, we really need mathlib nightlies (ie. precompiled mathlib)

[Patrick Massot]

It makes no sense that curious potential users have to wait for mathlib to compile

[Johan Commelin]

@Patrick Massot I think that is a very good start

[Johan Commelin]

I would also like a small section on how to work on an existing project, like lean-stacks-project

[Kevin Buzzard]

You can copy that from my README

[Kevin Buzzard]

except that it should be updated to use elan

[Simon Hudon]

In elan, when downloading Lean and its library, would it be possible to add a leanpkg.toml file at the root of library. That would make it easier to browse with emacs.

[Sebastian Ullrich]

What parts of browsing would that change?

[Simon Hudon]

When I open init/meta/tactic.lean in emacs, it tries to start a lean server and fails and M-. won't help
me go to a definition

[Sebastian Ullrich]

Oh, it looks like we forgot to include library/leanpkg.path in the releases. I'll fix it for the future.

[Simon Hudon]

Can leanpkg.path specify the version of lean to launch when editing the files?

[Sebastian Ullrich]

Ah, you are right. I guess injecting a leanpkg.toml file could indeed be the best solution.