Updating Mathlib

Stream: general

[Morenikeji Neri]

I typed leanpkg upgrade on msys2 but my mathlib doesn't update. Help!

[Kevin Buzzard]

If you're trying it with the xena-UROP project, it's probably because I set it to track Mathlib 3.4.1, which is fixed. I thought it might make life easier if we were all singing from the same hymn-sheet, as it were.

[Chris Hughes]

Keji wants to use signatures of permutations, which has just been merged.

[Kevin Buzzard]

To be honest I'm not sure of a slick way of sorting this out. I am guessing Keji is using Lean 3.4.1. If he were to download the latest nightly, and then switch his msys2 so that when he typed leanpkg it used the latest nightly, then maybe this would fix it. I don't know if he can just edit leanpkg.toml to fix it.

[Kevin Buzzard]

I'm currently in an airport which is not really the most ideal place to be experimenting with this sort of thing.

[Mario Carneiro]

I think you can just specify your mathlib dependency to point to "master"

[Mario Carneiro]

in leanpkg.toml

[Kevin Buzzard]

Keji I just edited leanpkg.toml following Mario's suggestion; try pulling the latest version of the repo (with git pull perhaps, if you have git working in msys2) and then try leanpkg upgrade again.

I must be honest -- I hadn't expected this to happen. I was envisaging people on the Xena summer project just playing around with basic stuff and nothing we needed getting PR'ed to mathlib. Really I just wanted to avoid having to spend hours showing people how to upgrade mathlib :-) We now run the risk that some of us will write code which will not run for others, but I guess in the long run most people have got Lean running on their laptops and it's in their interest to learn how to upgrade mathlib.

One could envisage a one-click solution to all of this for Windows users. An "upgrade mathlib" button which just requires someone to type in their github credentials (or perhaps not even that). For mac users it's often easier because they have a terminal pre-installed, and when they install git it might well end up in a directory which is already in their path.

[Mario Carneiro]

you can't stop progress

[Kevin Buzzard]

You said this back when I was pleading for mathlib 3.4.1, and as is usually the case I am now coming round to your way of thinking. It's not going to be so easy with CoCalc I suspect, but with my course running on CoCalc I really do think I want a frozen mathlib [famous last words]

[Chris Hughes]

Keji tried updating it with leanpkg upgrade, but it just unupdated instead, and reverted to some old version.

[Kevin Buzzard]

Did you pull or otherwise edit leanpkg.toml?

[Sebastian Ullrich]

I don't think there is a way to tell leanpkg to track a different branch for a dependency yet

[Mario Carneiro]

isn't the dependency item a git repo and a branch or commit hash?

[Sebastian Ullrich]

Yes, but leanpkg upgrade will still track the branch associated with the executed Lean version

[Sebastian Ullrich]

I.e. if you're running 3.4.1, leanpkg upgrade will always update to the head of lean-3.4.1

[Mario Carneiro]

so what does that branch info do?

[Sebastian Ullrich]

It points to the currently used commit, so it doesn't really make sense to store anything other than a commit hash or tag in that field. leanpkg upgrade ignores the field.

[Scott Morrison]

Is it reasonable to be able to change this? I would really like to be able to track arbitrary branches of dependencies.

[Scott Morrison]

I'm having trouble with the UROP repo.

[Scott Morrison]

> leanpkg upgrade
error: override toolchain 'master' is not installed
info: caused by: the toolchain file at '/Users/scott/scratch/xena-UROP-2018/leanpkg.toml' specifies an uninstalled toolchain

[Scott Morrison]

> elan toolchain list
stable (default)
nightly-2018-04-06
nightly-2018-04-20
nightly-2018-06-21
khoek-klean-3.4.2
khoek-klean-3.4.3
3.4.0
3.4.1

[Scott Morrison]

@Kevin Buzzard, do you know what's going on?

[Kevin Buzzard]

I wouldn't trust our leanpkg.toml :-)

[Kevin Buzzard]

The last time I pulled the project, it had at least one <<<<< .. ==== .. >>>>>in it :-)

[Kevin Buzzard]

leanpkg upgrade just worked for me

[Kevin Buzzard]

WARNING: Lean version mismatch: installed version is nightly-2018-06-21, but package requires master

[Scott Morrison]

I really wouldn't put leanpkg upgrade as part of your install instructions: https://github.com/ImperialCollegeLondon/xena-UROP-2018

[Scott Morrison]

leanpkg configure is what you want

[Scott Morrison]

(that doesn't touch your leanpkg.toml file, making it more likely it will survive multiple users)

[Kevin Buzzard]

Oh thanks. This was an attempt to get users to install mathlib in _target

[Scott Morrison]

btw --- we need to make sure you update/replace your blog post on installing on Windows, to tell people to use elan.

[Scott Morrison]

At Dagstuhl, Neil Strickland made a valiant effort to have someone show him how to install and prove the infinitude of primes in as many theorem provers as he could.

[Kevin Buzzard]

Neil just asked me to give a colloquium in Sheffield

[Scott Morrison]

I really struggled helping him install Lean on his (windows) laptop.

[Kevin Buzzard]

You need a terminal and git, and you need to understand how your chosen terminal's path can be configured to globally remember where git and lean are installed

[Keeley Hoek]

I don't think 'master' could ever work with the latest version of elan
it has to be 'stable', 'nightly-xxx', or something on this list https://github.com/leanprover/lean/releases with the prefix "v" removed

[Kevin Buzzard]

Aah there's the problem then. I don't use elan

[Kevin Buzzard]

Thanks.

[Scott Morrison]

Yeah --- we were definitely having problems with paths, and it wasn't helping that Neil had already tried and failed, so had left things affecting the paths.

[Scott Morrison]

It also didn't help that his system had 3 different notions of "path", between windows, cygwin, and msys2.

[Scott Morrison]

(He wanted to use cygwin, because that was the windows shell he was familiar with)

[Scott Morrison]

elan has a really big advantage here: it tries to take care of the paths for you, and I trust @Sebastian Ullrich to play with paths better than I trust users. :-)

[Johan Commelin]

Would Docker be an option for such showcasing purposes?

[Johan Commelin]

I hear that Docker also runs on Windows.

[Kevin Buzzard]

Here's a proposal for Windows users only: we make a "one size fits all" download. One zip file, that you put in C:/Users/Neil and then unpack, giving you a directory C:/Users/Neil/leanstuff/.

[Kevin Buzzard]

You then tell users to install VS Code, and then "open folder" the folder C:/Users/Neil/leanstuff/sample_project/, and to tell VS Code where the Lean binary is, which is C:/Users/Neil/leanstuff/lean-3.4.2/bin/lean.exe

[Kevin Buzzard]

and then everything just works.

[Kevin Buzzard]

No git, no command line, no nothing

[Johan Commelin]

Couldn't you even package VS code, with the right path setting, into that zipfile?

[Kevin Buzzard]

and that's because the sample project directory has got a correct leanpkg.toml, and _target/deps/mathlib exists and has all the .olean files and everything

[Kevin Buzzard]

I have no idea about how Windows works and whether you can package a complicated thing like VS Code in a zip file

[Reid Barton]

I also don't know how Windows works or how Docker on Windows works but it sounds like something worth looking into.
The examples I've managed to find involve VS Code running inside Docker on a Linux virtual system, and connecting to an X window server running under Windows. That sounds ... workable, but a little awkward (you still have at least two pieces to download).

[Reid Barton]

Some links:
https://hub.docker.com/r/joengenduvel/docker-vscode/
http://blog.ctaggart.com/2016/05/visual-studio-code-served-from-docker.html
https://www.aaron-powell.com/posts/2017-09-21-vscode-linux-docker-windows/

[Reid Barton]

There's probably no advantage to putting VS Code in the Docker container, and requiring the end user to download an X server and the Lean/mathlib/VS Code container, over just using the native VS Code, and requiring the end user to download VS Code and the Lean/mathlib container. And there are almost certainly advantages to native VS Code over one running over X11.

[Reid Barton]

I do sort of like the idea of Windows users having Lean/mathlib/git/etc. running inside a Docker container, though, since it reduces the support surface area

[Reid Barton]

It might become a very large download though, not sure.