Zulip Chat Archive

Stream: general

Topic: Updating Mathlib


view this post on Zulip Morenikeji Neri (Aug 10 2018 at 14:15):

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

view this post on Zulip Kevin Buzzard (Aug 10 2018 at 14:50):

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.

view this post on Zulip Chris Hughes (Aug 10 2018 at 14:50):

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

view this post on Zulip Kevin Buzzard (Aug 10 2018 at 14:52):

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.

view this post on Zulip Kevin Buzzard (Aug 10 2018 at 14:53):

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

view this post on Zulip Mario Carneiro (Aug 10 2018 at 14:55):

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

view this post on Zulip Mario Carneiro (Aug 10 2018 at 14:55):

in leanpkg.toml

view this post on Zulip Kevin Buzzard (Aug 10 2018 at 15:13):

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.

view this post on Zulip Mario Carneiro (Aug 10 2018 at 15:14):

you can't stop progress

view this post on Zulip Kevin Buzzard (Aug 10 2018 at 15:23):

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]

view this post on Zulip Chris Hughes (Aug 10 2018 at 15:24):

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

view this post on Zulip Kevin Buzzard (Aug 10 2018 at 16:09):

Did you pull or otherwise edit leanpkg.toml?

view this post on Zulip Sebastian Ullrich (Aug 10 2018 at 17:19):

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

view this post on Zulip Mario Carneiro (Aug 10 2018 at 17:20):

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

view this post on Zulip Sebastian Ullrich (Aug 10 2018 at 17:24):

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

view this post on Zulip Sebastian Ullrich (Aug 10 2018 at 17:25):

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

view this post on Zulip Mario Carneiro (Aug 10 2018 at 17:27):

so what does that branch info do?

view this post on Zulip Sebastian Ullrich (Aug 10 2018 at 17:35):

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.

view this post on Zulip Scott Morrison (Aug 10 2018 at 23:23):

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

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:54):

I'm having trouble with the UROP repo.

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:54):

> 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

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:54):

> 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

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:54):

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

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 15:55):

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

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 15:56):

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

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 15:57):

leanpkg upgrade just worked for me

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 15:57):

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

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:58):

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

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:58):

leanpkg configure is what you want

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:58):

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

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 15:58):

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

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:59):

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

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:59):

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.

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 15:59):

Neil just asked me to give a colloquium in Sheffield

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:59):

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

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 16:01):

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

view this post on Zulip Keeley Hoek (Aug 25 2018 at 16:01):

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

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 16:01):

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

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 16:02):

Thanks.

view this post on Zulip Scott Morrison (Aug 25 2018 at 16:05):

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.

view this post on Zulip Scott Morrison (Aug 25 2018 at 16:05):

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

view this post on Zulip Scott Morrison (Aug 25 2018 at 16:05):

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

view this post on Zulip Scott Morrison (Aug 25 2018 at 16:06):

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. :-)

view this post on Zulip Johan Commelin (Aug 25 2018 at 16:07):

Would Docker be an option for such showcasing purposes?

view this post on Zulip Johan Commelin (Aug 25 2018 at 16:08):

I hear that Docker also runs on Windows.

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 16:08):

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/.

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 16:09):

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

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 16:10):

and then everything just works.

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 16:10):

No git, no command line, no nothing

view this post on Zulip Johan Commelin (Aug 25 2018 at 16:10):

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

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 16:10):

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

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 16:11):

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

view this post on Zulip Reid Barton (Aug 25 2018 at 16:44):

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).

view this post on Zulip Reid Barton (Aug 25 2018 at 16:45):

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/

view this post on Zulip Reid Barton (Aug 25 2018 at 16:52):

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.

view this post on Zulip Reid Barton (Aug 25 2018 at 16:53):

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

view this post on Zulip Reid Barton (Aug 25 2018 at 16:54):

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


Last updated: May 17 2021 at 21:12 UTC