Lean installation in CoCalc

Stream: general

[Rob Lewis]

The CoCalc talk in another thread reminded me that I should start getting things ready for my course next year. This led to a chat with @Harald Schilly about how CoCalc installs Lean/mathlib. Irrelevant for my course, but probably relevant to others, so I'm bringing it here.

It would probably be good to install Lean through the version manager elan, with a reasonable default version (3.5.1?) and a handful of options pre-installed. Right now it's a plain install of a 3.4.2 binary.

What about pre-installing versions of mathlib? leanpkg has a notion of a global install of a package. But I'm not sure it's the best move here. @Gabriel Ebner doesn't think it will play well with elan. And it probably interacts badly with non-global mathlib dependencies, which people might use if they want a newer version than whatever CoCalc gives.

CoCalc could provide directories containing (compiled) mathlibs for each Lean version it pre-installs. Users would have to set up projects with leanpkg.toml files pointing to the right spot. Fine for courses that can distribute this project, trickier for someone who just wants to open a .lean file in CoCalc and start using real numbers.

As I understand it, free CoCalc doesn't allow accessing external websites. So adding packages from GitHub won't work, nor will elan on new versions of Lean, nor will cache-olean/update-mathlib. This is why I'm suggesting pre-installing things, although of course this a reason to pay for CoCalc :)

Thoughts? ( cc @William Stein )

[William Stein]

I can tell you that by default it is very confusing for people to get access to mathlib on CoCalc if they aren't experts. We CoCalc admins definitely do NOT know what to do in order to make mathlib (or other libraries?) available by default, though we've tried and failed repeatedly. If you want to see precisely what our lean install is on cocalc now, just open a Terminal in any cocalc project (+New --> Terminal), then type cd /ext/lean and ls:

[William Stein]

[William Stein]

/ext/lean$ ls
lean  lean-3.4.1-linux  lean-3.4.2-linux
/ext/lean$ which lean
/ext/bin/lean
/ext/lean$ ls -l lean
lrwxrwxrwx 1 salvus salvus 16 Feb 12  2019 lean -> lean-3.4.2-linux
/ext/lean$ cd lean-3.4.2-linux/
/ext/lean/lean-3.4.2-linux$ ls
bin  include  lib  mathlib  mathlib-lean-3.4.2
/ext/lean/lean-3.4.2-linux$ lean --path
{
  "is_user_leanpkg_path": true,
  "leanpkg_path_file": "/home/user/.lean/leanpkg.path",
  "path": [
    "/ext/lean/lean-3.4.2-linux/bin/../library",
    "/ext/lean/lean-3.4.2-linux/bin/../lib/lean/library"
  ]
}

Note that we have a copy of mathlib but it's not in either of the directories of the default lean search path, which might be why it doesn't work. Should we move it into a subdirectory called "library"?

[Rob Lewis]

The library subdirectory is for the core Lean library. I'm guessing you'd have trouble moving mathlib there. With your current setup, you can do the following:

~$ leanpkg install /ext/lean/lean-3.4.2-linux/mathlib-lean-3.4.2/

(don't do it inside /ext/lean/lean-3.4.2-linux/, apparently). This is a global install of mathlib so it should be available whenever you open a Lean file -- you might need to restart the Lean server if it was running already.

[Rob Lewis]

This is fine if your users are okay with a fixed version of Lean and mathlib.

[Patrick Massot]

One can think that users of CoCalc don't need many versions of mathlib (they would use Lean locally if they were that serious about it). But I'm worried for teachers: what if I start a course using mathlib and suddenly CoCalc updates mathlib? What I did last year was to distribute a compiled mathlib using CoCalc distribution mechanism. Let's dream a bit here. Let's say some script downloads a mathlib nightly on the first of every month and call it mathlib_january etc. Then users could add a leanpkg dependency to mathlib_february or something. Then every year automatically erases ancient mathlibs.

[Patrick Massot]

This shouldn't be a Lean specific issue however. What happens to existing projects when Sage is updated? I guess Sage has some breaking changes from times to times.

[William Stein]

This shouldn't be a Lean specific issue however. What happens to existing projects when Sage is updated? I guess Sage has some breaking changes from times to times.

1. We keep all past versions of Sage, and have a sage_select command so users can choose a default. Right now things are extra complicated because the last Sage update was python2 --> python3! With Jupyter the situation is very good since there is no default sage version for Jupyter notebooks -- you have to explicitly choose a version the first time, and then it defaults to that afterwards and is encoded in the ipynb file, so you get that version henceforth when using that notebook. If an instructor prepares course materials with Sage-8.9, then all students will be using sage-8.9 when they open that notebook, even if we installed sage-9.1... unless sage-8.9 isn't available and then they get a message and select from the closes related kernel. This is one thing Jupyter really got right.

2. We do have several point in time snapshots of the entire (several hundred GB) install stack for a project, which can be selected in project settings. Then no matter what upgrades happen for a default cocalc project, they don't happen for that project. People asked for this, but in practice don't use it much -- for most software, people tend to prefer the newest version with whatever bugfixes are in it (plus documentation parity with the web) to a static version. We also have many completely custom images (using the mybinder spec) and some classes use this for the whole class. We could do more to make this more straightforward to use though.

[William Stein]

We'll try leanpkg install /ext/lean/lean-3.4.2-linux/mathlib-lean-3.4.2/since this will at least be a good start. Would this break people being able to install their own mathlib locally that overrides the global one?

[Harald Schilly]

Rob Lewis said:

```
~$ leanpkg install /ext/lean/lean-3.4.2-linux/mathlib-lean-3.4.2/
```
(don't do it inside `/ext/lean/lean-3.4.2-linux/`, apparently).

Sorry, I'm not 100% sure about that. Does it matter in which directory I run that leanpkg install ? Not inside the one you mention?

[Rob Lewis]

William Stein said:

We'll try leanpkg install /ext/lean/lean-3.4.2-linux/mathlib-lean-3.4.2/since this will at least be a good start. Would this break people being able to install their own mathlib locally that overrides the global one?

I'm not sure -- will try to test locally. Maybe someone else here knows off the top of their head? :)

[Rob Lewis]

Harald Schilly said:

Sorry, I'm not 100% sure about that. Does it matter in which directory I run that leanpkg install ? Not inside the one you mention?

Running leanpkg install /ext/lean/lean-3.4.2-linux/mathlib-lean-3.4.2/ anywhere outside of /ext/lean should be fine, is my guess. I got weird errors when I did it there, but then I switched to ~ and it worked.

[Rob Lewis]

Oh, I think it has to be done somewhere you have write access.

[Rob Lewis]

That's why it didn't work in /ext/lean.

[Harald Schilly]

ok, I tried that leanpkg install ...and all that happened was it changed files in my $HOME/.lean directory.

So, just to clarify: what we here at cocalc aim for is to have lean + mathlib + other libs (if there is a need) at a global location, which is read-only. That directory is accessible from each and every project on cocalc. Then, when lean starts, it should pick up that global mathlib. With Linux or Python, it is possible to tweak a PATH or PYTHONPATH variable, containing a list of directories where it should search for binaries or a library. I suppose with LEAN there is nothing like that and you have to configure this in your local directory? If that's the case, this might only work if we install mathlib + other libs in that builtin_path directory (I saw that in a leanpkg.path file)

[Harald Schilly]

ok, hmm, I think I should read up in detail what the install command is doing.

[Kevin Buzzard]

Note: Rob points out that some of this post is incorrect

I think install is how a user installs dependencies for their project. For example many mathematics projects have a dependency on mathlib. The install command, for me, would edit leanpkg.toml to indicate that my project relies on mathlib (or more precisely on a certain commit of mathlib). Then leanpkg configure would download that particular commit and put it into _target, and then, if you have all the user tools installed, update-mathlib would download compiled binaries for the version of mathlib you chose.

Having a stable version of Lean is eminently sensible. 3.5.1 is just a bugfix for 3.4.2 really, I think, so you should probably use that. But I have always downloaded my own mathlibs when using lean on cocalc, because different project rely on different things and mathlib changes can be non-backwards-compatible.

[William Stein]

I just tried typing leanpkg install /ext/lean/lean-3.4.2-linux/mathlib-lean-3.4.2/ in a cocalc project, then creating a lean file and putting a bunch of code that uses mathlib from here in, and it works (no errors in output).

[Rob Lewis]

Kevin, leanpkg install is different than leanpkg add.

[Rob Lewis]

Hmm. When you're outside a Lean project (ie no leanpkg.toml in a directory below you), the leanpkg_path_file value shown by lean --path is different. It doesn't exist on my machine. I wonder if creating that file would act as a "default" path file, and what exactly needs to go in to direct it to a default mathlib install.

[William Stein]

I could make it so that when cocalc is about to start the lean server it first checks to see if ~/.lean is empty, and in that case runs leanpkg install /ext/lean/lean-3.4.2-linux/mathlib-lean-3.4.2/. Then mathlib would work for random users (esp without internet access on cocalc), but if anybody needs to do something custom, they can just delete and customize ~/.lean however they want and it won't get touched.

[William Stein]

Anyway, making a change to run a leanpkg install of mathlib when first running lean wouldn't be too hard... it also doesn't waste disk space.

[Rob Lewis]

William Stein said:

I could make it so that when cocalc is about to start the lean server it first checks to see if ~/.lean is empty, and in that case runs leanpkg install /ext/lean/lean-3.4.2-linux/mathlib-lean-3.4.2/. Then mathlib would work for random users (esp without internet access on cocalc), but if anybody needs to do something custom, they can just delete and customize ~/.lean however they want and it won't get touched.

That would work, except manually editing a hidden directory isn't the normal way people will try to update mathlib. More likely they'll have a local Lean project and run leanpkg add ... to get a copy from GitHub. The pre-installed one might still be available and cause conflicting imports, I'm not sure.

[William Stein]

My main motivation is new students and random people who want to solve some problems using mathlib + lean that say @Kevin Buzzard tweets about. They wouldn't have access to github if they are using cocalc for free, and anyways it would be nice to avoid the friction of opening a terminal and using leanpkg add. The question is if both of these audiences can be served without confusion.

[Rob Lewis]

Right. It seems like a reasonable default.

[William Stein]

That would work, except manually editing a hidden directory isn't the normal way people will try to update mathlib.

If one does leanpkg install /ext/lean/lean-3.4.2-linux/mathlib-lean-3.4.2/ in a clean account, then later does leanpkg add ..., what happens? Maybe the second command gives them the latest mathlib version and all is good?

[William Stein]

I've made this issue, which I'll look into later today (have to go now): https://github.com/sagemathinc/cocalc/issues/4393

[Rob Lewis]

I'm starting a VM to try it from a clean slate.

[William Stein]

@Rob Lewis thanks. You can also easily get a new anonymous throw-away cocalc project by opening the following link in a private browsing session: https://cocalc.com/app?anonymous=true

Never mind -- that wouldn't have internet access.

[Rob Lewis]

Okay, I think you're safe with this setup. Run leanpkg install /ext/... in/below ~. If someone creates a Lean project anywhere in ~, the new leanpkg.path seems to override the global install. This happens whether or not mathlib is added to the project with leanpkg add. The global install is unavailable in the project as soon as the project is created.

[William Stein]

I implemented this and it is NOW live in CoCalc. mathlib will "just work" with no manual intervention by users for any newly started (or restarted) project that doesn't already have a ~/.lean directory. In particular, @Kevin Buzzard you could post lean files on share.cocalc.com that rely on mathlib, and when people open that content (e.g, as an anonymous user), it'll work (or at least lack of mathlib won't be the issue).

Here's an example on the share server: https://share.cocalc.com/share/df81e09e5b8f16f28b3a2e818dcdd4560e7818ae/support/2020-02-19-lean-natural-numbers.lean?viewer=share

If somebody clicks the green button to open the document it should work, automatically adding support for mathlib on first use of lean and they will see this:

pasted image

I'm guessing the error involving example (p : ℕ) : prime p → p ≥ 2 := prime.two_le is due to our version of mathlib being slightly old. @Harald Schilly should update the mathlib version soon and then it'll work, presumably (I don't know).

[Johan Commelin]

@William Stein @Harald Schilly Wow! Thanks a lot for all your effort.

[Kevin Buzzard]

Thanks for this William. I'm giving a talk in Oxford today and if I get it working before then I'll showcase it

[Rob Lewis]

Awesome!

[Rob Lewis]

A small note, if you're going to update the mathlib version you might as well update the Lean version as well. I'd recommend using 3.5.1 from here: https://github.com/leanprover-community/lean/releases

[Harald Schilly]

Rob Lewis said:

... recommend using 3.5.1 ...

thank you, I discovered that already. However, regarding mathlib, my impression is that it is fine to grab the master-tip of the repository, but there are also "snapshot" like releases in it's repo. Last one from Oct'19, though. I'm aware of that mathlib-tool, and reading the sources of that script, it looks like grabbing the nightly build is what I should do. For me, as an "outsider" to lean, this is a little bit confusing ^^

[Rob Lewis]

I think it's extra complicated because the CoCalc install isn't (and shouldn't be) following the "standard" installation model.

[Rob Lewis]

I have no idea what the snapshot releases in the mathlib repo are for. Maybe we should delete those?

[Rob Lewis]

Using the master tip of mathlib is fine, if you're building it yourself. There are supporting scripts for downloading pre-built olean files. But there's no need to install them in CoCalc. You could do it locally to create the mathlib image if you wanted.

[Rob Lewis]

(deleted)

[Rob Lewis]

The easiest way to get a fully built mathlib repo manually is through the CI. Download the build artifact here: https://github.com/leanprover-community/mathlib/runs/456786112

[Rob Lewis]

That will give you the master version of mathlib with pre-built oleans.

[Harald Schilly]

thank you @Rob Lewis … yes, it's different. So, what I ended up is writing a script to grab the latest nightly build of mathlib from the mathlib-nightly repo. Just one minor detail was off: it extracts as "src/*" without these two toml and path files. I ended up writing them on my own, without specifying the lean version. With what @William Stein came up with will point to the matlib path, which will be next to the default version of lean we at cocalc symlink to. Therefore, the mathlib package will correspond to whatever the default version is, i.e. 3.5.1 right now.

[Harald Schilly]

net result: the file william shared yesterday will process fine, see screenshot below. This isn't live on cocalc yet, but will be part of our next update (during the weekend).

2020-02-20-lean-mathlib-3.5.1-cocalc.png

[Patrick Massot]

I have no idea what the snapshot releases in the mathlib repo are for. Maybe we should delete those?

Does anyone has enough admin power to get rid of those? They are useless and confusing.

[Rob Lewis]

Nice! Sounds good to me :)

[Rob Lewis]

Yeah, let's figure out how to delete the snapshots. We're certain they aren't used for anything, right?

[Patrick Massot]

The dates clearly prove they aren't used for anything.

[Rob Lewis]

The snapshot is related to some kind of package manager @Simon Hudon was working on at some point. I'm not going to delete that one.

[Rob Lewis]

The others are gone.

[Patrick Massot]

Harald and William, how does all this conversation relate to https://github.com/sagemathinc/cocalc/issues/3589? Did you also solve that?

[Harald Schilly]

The ticke is still open, so I assume the server starts in the home directory.

One question about the logic: if running lean -p in the directory where the .lean file is says is_user_leanpkg_path is true → start the lean server in $HOME. If it is false → start it in the directory where leanpkg_path_file is. Correct?

[Harald Schilly]

We should make the logic crystal clear on the ticket, that's all. The implementation shouldn't be hard...

[Patrick Massot]

It would be nice if someone who knows more about when Lean does could have a look. Maybe Gabriel or Rob?

[Kevin Buzzard]

Maths challenges for the Lean curious on CoCalc got demoed in Oxford today and it was slow but ultimately worked fine. In particular mathlib imports work fine (I couldn't get them to work with shared projects yesterday).

[Kevin Buzzard]

@William Stein is it slow because Oxford is a long way from Seattle or something?

[Patrick Massot]

I find it distracting that CoCalc is constantly displaying help on the tactic under cursor. VScode doesn't do that.

[William Stein]

Kevin Buzzard said:

William Stein is it slow because Oxford is a long way from Seattle or something?

1. What precisely was slow? 2. the CoCalc servers are on the east coast of the US.

[William Stein]

Patrick Massot said:

I find it distracting that CoCalc is constantly displaying help on the tactic under cursor. VScode doesn't do that.

Can you clarify this? Do you mean that a panel off to the right is displaying something when it shouldn't? What's a minimal example to reproduce this? CoCalc just takes exactly the same LSP language server protocol data as VSCode and displays it, though how it does so is different.

[Patrick Massot]

Compare pasted image and pasted image

[Patrick Massot]

This is the exact same Lean code with the cursor at the same place.

[Patrick Massot]

But the CoCalc version has an extra line at the bottom right, documenting the sorry tactic.

[William Stein]

Thanks. In VSCode how does one display the help? In CoCalc it would probably be very easy to change things so that the help is always displayed in a completely separate panel, and if you don't want to see it, you just close that panel... Would that work for you?

[William Stein]

(By the way, CoCalc has dark mode editor themes, and also an overall dark mode for the whole UI -- look in Account --> Preferences.)

[Patrick Massot]

In VScode that help would show up as a tooltip if you hover over "sorry".

[Patrick Massot]

The solution you describe would work.

[Kevin Buzzard]

I have a memory that in the community web editor the behaviour is the same as in CoCalc. But I can't get the community web editor to work right now.

[William Stein]

I've created an issue: https://github.com/sagemathinc/cocalc/issues/4403

[Patrick Massot]

Thanks!

[William Stein]

@Patrick Massot this is implemented and now live at https://cocalc.com. Refresh your browser to see the change. The panel layout doesn't change for files you already have open, but a new "Help" panel appears for newly opened files. Also, help only goes to the help panel (starting now, even with existing files).

[Patrick Massot]

Kevin's stuff is not responding right now. I tried logging in my account and accessing the Lean project where we tried stuff last year but it simply hangs at Parsing at line 1.

[Patrick Massot]

Unfortunately this is my typical CoCalc experience. When it works it's great, but when it doesn't work there is nothing you can do or investigate.

[Patrick Massot]

pasted image

[Patrick Massot]

Now I have a lot of error messages:

invalid import: data.real.basic
/home/user/_target/deps/mathlib/data/real/basic.lean:275:13: error: unexpected token
 4:10 error
excessive memory consumption detected at 'is_def_eq' (potential solution: increase memory consumption threshold)
 6:0 error
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)

[Patrick Massot]

This is all in the project we share.

[Patrick Massot]

But it works in my teaching project from last year.

[Harald Schilly]

I've just released the software update, that includes the newer lean/mathlib setup. So, in CoCalc, projects have a "software environment" setting (in project settings → project control). "Default" is what I just updated and if your project is still running from before the update, you have to restart it to get the update. If you're set to "Experimental", you're one step ahead and use what will be the Default soon.

[Harald Schilly]

In any case, I just tested it with these challenges via an anonymous account. clicking the button copies all these files into a fresh project and when I open up a solution, it works.

[Harald Schilly]

I'll try to remember posting here when we're about to update anything regarding LEAN. If there are any requests, you can ping me as well.

[Patrick Massot]

Thanks!

[Patrick Massot]

Kevin, how did you setup up the challenges so that anyone can play via anonymous accounts?

[Patrick Massot]

By the way, I just tried the first challenge and it worked perfectly.

[Harald Schilly]

Patrick Massot said:

Kevin, how did you setup up the challenges so that anyone can play via anonymous accounts?

this is all via https://doc.cocalc.com/share.html .. i.e. make a directory, put files in it, go to the parent of that directory (or home dir) and select just this directory and then publish it as such a "share". all files inside of it will end up being public as well.

[Harald Schilly]

when you open it (anonymously, or a fresh project), cocalc's lean editor will start, notices that there is no config in ~/.lean and creates it (that's what william coded up one or two days ago).

[Johan Commelin]

Nice! That works really smoothly. And for my test it was really responsive. This is cool!

[Harald Schilly]

quick update from my perspective at cocalc: I tried to upgrade to lean 3.6.0 + mathlib 2020-02-27 nightly, but it doesn't work. I have no idea why. The symptoms are high (never ending) cpu usage and then it fails with "excessive memory usage error" or the whole cocalc interface is unresponsive. So, something must have changed that causes an issue. Hence there won't be 3.6.0 on cocalc for now.

[Johan Commelin]

@Gabriel Ebner @Rob Lewis :up:

[Kevin Buzzard]

One thing you could try is this: upgrade the Lean binary to 3.6, upgrade the mathlib Lean files, and then compile them yourself with lean --make src in the mathlib root directory. It will take a while but it might be the easiest way to just make everything work.

[Johan Commelin]

@Harald Schilly Currently mathlib is not compatible with lean 3.6.0

[Kevin Buzzard]

Oh!

[Johan Commelin]

Lean 3.6.0 was released yesterday, and we'll first have to fix mathlib.

[Harald Schilly]

ahh!

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/master/leanpkg.toml

[Johan Commelin]

Still says 3.5.1 :grinning:

[Harald Schilly]

ok. that explains everything. hence just updating mathlib nightly ^^

[Johan Commelin]

No worries.

[Johan Commelin]

Probably in a couple of days there will be a big change in mathlib. From then on mathlib wont work with lean 3.4.2 anymore but only with lean 3.6.*

[Johan Commelin]

3.5.1 exists as some sort of transition.

[Rob Lewis]

@Harald Schilly If you're installing versions of Lean manually (i.e. you're not using the version manager elan), you'll always need to check by hand that your lean and mathlib versions match. This is a "nonstandard" installation. For the most part we expect people to be using elan.

[Harald Schilly]

hi, I am trying to update lean + mathlib on CoCalc. When I looked into this the last time, I wrote a script to get the latest nightly mathlib build, but somehow it stopped being updated. That makes me suspicious. If I download the latest nightly of mathlib, is there a way for me to know, for which version of lean it is? (there is no toml file in it)

[Kevin Buzzard]

I think everything works completely different now.

[Kevin Buzzard]

You should use leanproject to download mathlib (and any other Lean repo)

[Kevin Buzzard]

It does all the dirty work behind the scenes

[Harald Schilly]

ok, thank you, never heard of it. I hope it support these global installations like they're on cocalc? I'll check what it is, though.

[Kevin Buzzard]

https://leanprover-community.github.io/get_started.html

[Kevin Buzzard]

https://leanprover-community.github.io/toolchain.html

[Kevin Buzzard]

https://leanprover-community.github.io/install/linux.html

[Kevin Buzzard]

These may or may not be helpful. The bottom of the first page are links. The second page is an explanation of what's going on, and the third is explicit linux install instructions, although there are also quicker installation procedures for e.g. Ubuntu

[Kevin Buzzard]

The overview is: you shouldn't install Lean, you should install elan which is a tool which works out which version of Lean you should be using, and if necessary downloads it. For CoCalc you might want to consider downloading all ten or so recent versions of Lean, or you might want to offer one by default and let users download more if they want. I had problems with sharing Lean projects on CoCalc precisely because they were written with the wrong version of Lean (and new Lean releases come at the rate of one per month right now, which is not a problem for us because of elan but which might be a problem for CoCalc if it doesn't want to adopt elan).

[Kevin Buzzard]

Mathlib in contrast updates several times per day, and to help with this we use a tool called leanproject.

[Kevin Buzzard]

leanproject downloads mathlib binaries, updates your mathlib and so on. It has only been around for a couple of months but it seems to currently be the solution to all our problems and I can't imagine it changing much any time soon.

[Kevin Buzzard]

Speaking personally, as a Lean user I want the world. I want to be able to develop using bleeding edge Lean and bleeding edge mathlib on CoCalc, and I want the leanpkg.toml file in my Lean project to tell CoCalc which version of Lean and mathlib to use. Furthermore, if I share a Lean file, perhaps one which depends on a local installation of mathlib in my Lean project in my CoCalc project, and runs on Lean 3.9.0 because I didn't update to 3.11 yet, it would be brilliant if this just worked.

[Kevin Buzzard]

You must have the same problems with Sage, there are lots of versions of Sage. But realistically I don't know how easy it would be to implement my dreams.

[Kevin Buzzard]

Here is the reason that you at CoCalc might be motivated to make the system so flexible: if I have a Lean project stored on CoCalc and I want to share one file with the world, and this file has other local files as imports as well as mathlib imports, then currently there is no easy way for me to do this unless I set up my own web editor. CoCalc will be fussy about which version of Lean I use, and which version of mathlib, and I never figured out how to get it to play well with local imports unless I zipped up the entire project and shared it as a zip file, which is very inefficient; start-up times are already bad. Your main rival is the Lean Web Editor and here I can share a file given e.g. its URL, but the only imports I am allowed are imports from mathlib. The mathlib is very up to date though. This means that a sharing of a file might break if I don't maintain it.

[Harald Schilly]

thank you for all the explanations. there are certain constraints which make some aspects impossible. so, one solution could be that there is no default lean on cocalc any more and therefore simple sharing of lean projects will not work out of the box.

[Kevin Buzzard]

How does sharing work? Here is what I could imagine. One looks for a file and sees if it is in some directory which contains a leanpkg.toml file, and if it is then it reads the version of Lean from the toml file. This is exactly what elan does if I'm not mistaken.

[Harald Schilly]

sage and all other software packages are much easier to setup, because they have consistent releases and don't require internet access when someone wants to run them.

[Kevin Buzzard]

buzzard@bob:~/lean-projects$ cd lean-perfectoid-spaces
buzzard@bob:~/lean-projects/lean-perfectoid-spaces$ lean --version
Lean (version 3.5.1, commit d3a94649bdb4, Release)
buzzard@bob:~/lean-projects/lean-perfectoid-spaces$ cd ..
buzzard@bob:~/lean-projects$ cd mathlib
buzzard@bob:~/lean-projects/mathlib$ lean --version
Lean (version 3.10.0, commit 2c578165cc85, Release)
buzzard@bob:~/lean-projects/mathlib$ cd ..
buzzard@bob:~/lean-projects$ lean --version
Lean (version 3.4.2, commit cbd2b6686ddb, Release)
buzzard@bob:~/lean-projects$

[Harald Schilly]

I don't know anything about lean or elan, so, I don't know. there is a tool that picks up configuration information for lean. I don't remember if this was elan or lean itself.

[Kevin Buzzard]

elan is that tool

[Kevin Buzzard]

You can see it in action in the shell session above. Just moving between directories changes which lean I am running

[Kevin Buzzard]

If I have a project with internet access then I can download Lean locally.

[Bryan Gin-ge Chen]

We stopped updating the mathlib-nightly releases because one of the programs used in the CI script stopped compiling and we didn't realize that anyone was still using the nightly releases. If it would help make Lean easy to use on cocalc, we could try to restart the nightly releases again. @Gabriel Ebner what do you think?

[Harald Schilly]

Kevin Buzzard said:

elan is that tool

ok, well, I thought lean --path is how to look up which lean environment you're using. we're probably both right, just or different aspects.

[Kevin Buzzard]

Yes, I think that lean isn't a binary, I don't really know how it works. What I don't understand is why I can't share a project and have it run with the version of Lean which it says in the project.

[Kevin Buzzard]

(I'm not saying "you have to do this", I'm saying "I'm ignorant", of course)

[Harald Schilly]

so, elan is not easy to install either. there is just one script (something from rust?) and I would have to audit what it is doing before I can run it. it would be better if there is somewhere a short explanation what it is supposed to do or few steps to do it manually.

[Kevin Buzzard]

because locally this is what is happening with me. I download projects with leanproject(which imports all the correct mathlib binaries) and open them in VS Code and they run with the correct version of Lean because of some elan magic.

[Kevin Buzzard]

Yes, unfortunately I am not someone who knows what is actually going on, I am just someone with an understanding of what seems to be happening from the user perspective

[Harald Schilly]

well, one of the constraints in cocalc is, that you can't in general assume that you can download anything from the web. besides that, it would mean you have to store all the files for all projects separately.

[Kevin Buzzard]

I just occasionally type things like pip install --upgrade leanproject and don't worry about anything else.

[Harald Schilly]

ok, I see, thank you for the links

[Kevin Buzzard]

What I have been doing in CoCalc is that all my projects live in different directories and each one has a different mathlib in it

[Kevin Buzzard]

My Leans I store in ~/.elan/toolchains

[Kevin Buzzard]

I currently seem to have 17 versions of Lean on this computer

[Kevin Buzzard]

buzzard@bob:~/.elan/toolchains$ ls -l
total 68
drwxr-xr-x 6 buzzard buzzard 4096 Feb  8 14:10 3.3.0
drwxrwxr-x 5 buzzard buzzard 4096 Mar 24  2019 3.4.2
drwxrwxr-x 5 buzzard buzzard 4096 May  7 18:33 leanprover-community-lean-3.10.0
drwxr-xr-x 5 buzzard buzzard 4096 May 10 13:57 leanprover-community-lean-3.11.0
drwxr-xr-x 5 buzzard buzzard 4096 Feb 12 21:38 leanprover-community-lean-3.5.1
drwxr-xr-x 5 buzzard buzzard 4096 Mar  7 21:54 leanprover-community-lean-3.6.1
drwxrwxr-x 5 buzzard buzzard 4096 Mar 18 18:54 leanprover-community-lean-3.7.0
drwxrwxr-x 5 buzzard buzzard 4096 Mar 19 20:56 leanprover-community-lean-3.7.1
drwxr-xr-x 5 buzzard buzzard 4096 Mar 21 23:21 leanprover-community-lean-3.7.2
drwxr-xr-x 5 buzzard buzzard 4096 Apr 11 15:07 leanprover-community-lean-3.8.0
drwxr-xr-x 5 buzzard buzzard 4096 Apr 22 22:18 leanprover-community-lean-3.9.0
drwxr-xr-x 5 buzzard buzzard 4096 May  8 14:30 leanprover-community-lean-9.9.9
drwxr-xr-x 5 buzzard buzzard 4096 Dec 28 18:29 nightly-2018-04-06
drwxr-xr-x 5 buzzard buzzard 4096 Apr 14  2019 nightly-2018-04-20
drwxr-xr-x 5 buzzard buzzard 4096 Apr 28  2019 nightly-2018-06-21
drwxrwxr-x 5 buzzard buzzard 4096 Oct 22  2019 nightly-2019-01-13
drwxr-xr-x 5 buzzard buzzard 4096 Mar 24  2019 stable
buzzard@bob:~/.elan/toolchains$

[Kevin Buzzard]

and more appear on the fly, because elan downloads them automatically

[Gabriel Ebner]

Bryan Gin-ge Chen said:

We stopped updating the mathlib-nightly releases because one of the programs used in the CI script stopped compiling and we didn't realize that anyone was still using the nightly releases. If it would help make Lean easy to use on cocalc, we could try to restart the nightly releases again. Gabriel Ebner what do you think?

I don't like creating an extra distribution system to make it easier to use mathlib in an unsupported way. You can get the almost the same thing as the mathlib nightlies by running leanproject get mathlib (instead of downloading a zip file from the release page).

[Gabriel Ebner]

Harald Schilly said:

so, elan is not easy to install either. there is just one script (something from rust?) and I would have to audit what it is doing before I can run it. it would be better if there is somewhere a short explanation what it is supposed to do or few steps to do it manually.

You can compile elan yourself. It builds a small rust program called elan-init. You then just need to install it to /usr/bin/elan-init and then symlink elan-init to /usr/bin/elan, /usr/bin/lean, /usr/bin/leanpkg, and /usr/bin/leanchecker if you're installing it manually.

[Harald Schilly]

ok, I'll try that. installing elan on cocalc isn't supported, because it want's to download files into the user's home directory – but it must be global. I could try moving files around, but who knows if that will help at all.

[Gabriel Ebner]

I really strongly suggest to use elan, Lean has no backward or forward compatibility.

[Harald Schilly]

ahh! so I actually don't have to run elan-init .. ok ok

[Gabriel Ebner]

By default, elan will look for toolchains in ~/.elan. I would suggest that you preinstall all Lean versions (like every single one from 3.4.2 to 3.11.0). You can either symlink ~/.elan to /opt/elan, or set the environment variable ELAN_HOME=/opt/elan.

[Gabriel Ebner]

Assuming that you have the global installation at /opt/elan, you can pick whatever directory you like.

[Harald Schilly]

yes, directories will be different. so, I also assume, that all cocalc projects then will have to set ELAN_HOME=/ext/lean/elan ?

[Gabriel Ebner]

My suggestion is to either make a symlink ~/.elan -> /ext/lean/elan or set ELAN_HOME=/ext/lean/elan in all cocalc projects.

[Harald Schilly]

I ran elan toolchain install stable → which installed 3.11 it in a global toolchain repository. good. :-)