CoCalc: How to share a Lean project

Stream: general

[Kevin Buzzard]

I want to let users interact with a Lean file without installing Lean. Unfortunately the Lean file I want to let them interact with is part of a lean project and involves imports of other files in the project. My understanding is that this means that the community web editor can't do it without just cutting and pasting all imports on the top, which is sometimes unfeasible.

CoCalc can solve this problem now because it now has the functionality to share CoCalc project files, and it supports Lean. I believe that free projects don't have internet access so the below would not work without extensive modification. But for a project with internet access, here's a step-by-step guide to enabling users to interact with one of the project files without having to install Lean. Note that CoCalc currently only supports Lean 3.5.1 so be sure your project runs with this version of Lean.

Step 0) Write the Lean project you want to share on CoCalc and put it on github. Maybe some files in your project import some other files in your project -- that's OK.

Step 1) Go to Cocalc.com and make a new Cocalc project. Make sure it has internet access.

Step 2) Create a new linux terminal in the project with New -> Linux terminal.

Step 3) At the terminal, type

git clone https://github.com/leanprover-community/mathlib-tools.git
cd mathlib-tools
pip3 install .
cd ..
rm -rf mathlib-tools

I suspect that at some point in the future this will just become pip3 install mathlibtools (Patrick made some changes to the github repo earlier today when we were debugging all this).

Step 4) Clone your Lean project on CoCalc with leanproject get <name of your Lean project on github> e.g.

leanproject get ImperialCollegeLondon/natural_number_game

Now there are two reasons why things won't work yet: first, CoCalc's current policy is to have the leanpkg.path file in the root directory rather than in the project folder, and secondly CoCalc doesn't use elan, it just runs a fixed version of Lean, which at the time of writing is 3.5.1, and hence if your project doesn't run on 3.5.1 you're in trouble.

Step 5) If you had set up your Lean project to use Lean 3.5.1 then that's great. If you didn't then you'll have to fix this now. To get your project running on 3.5.1: go back to Files in CoCalc and find the leanpkg.toml file in your Lean project. Change the line that says

lean_version = [whatever it says]

to

lean_version = "leanprover-community/lean:3.5.1"

and then within your lean project type

leanproject --no-lean-upgrade upgrade-mathlib

This should get you to the last version of mathlib which was supported in 3.5.1 (commit message "Lie algebra should not extend lie ring")

Step 6) Finally, to get your lean project to work with CoCalc you need to ensure that the leanpkg.path for the project is in the root directory of your CoCalc project. You can do this either by moving all the contents of the Lean project folder into the root directory of the CoCalc folder (don't forget .git and .gitignore), or you can just move leanpkg.path and then hack it, e.g. if the path file which leanproject generated looks like this

builtin_path
path _target/deps/mathlib/src
path ./src

and it's in a directory called natural_number_game then your hacked one should be in the root folder of the CoCalc project and should looks like this:

builtin_path
path natural_number_game/_target/deps/mathlib/src
path natural_number_game/src

Step 7) leanproject build from within the Lean project should now build it.

Step 8) When the build is finished, use the CoCalc file manager to find the Lean file or files you want to share with the world, click on the box on the left and then click on "Share" amongst the options at the top.

[Kevin Buzzard]

If anyone fancies beta testing, does this link work? Hopefully you should be able to get to the "lost levels" of the natural number game, the API for < which I never managed to find the time to translate into about 20 more web pages but they're all there in one single Lean file which you should be able to play just as if it were the natural number game. Does it work?

[Kevin Buzzard]

[just remembered I can test it myself with a private browser window, and it doesn't, so these instructions still need work]

[Gabriel Ebner]

cocalc_error.png

[Kevin Buzzard]

Yeah I need to share the entire project I think, which I don't know how to do.

[Gabriel Ebner]

Sorry, missed the "it doesn't" comment.

[Kevin Buzzard]

https://cocalc.com/share/fd285f5a46ee9b6180a0719438cc82490ff98187/natural_number_game/?viewer=share

[Kevin Buzzard]

Maybe this is the best link

[Kevin Buzzard]

no I am still not sharing my Lean path it seems

[Kevin Buzzard]

I thought I had this working before with the Lean maths challenges but now I am just wondering whether CoCalc just over-rode my local mathlib imports with their inbuilt mathlib ones.

[Kevin Buzzard]

I think everything is broken right now. I'll let people know when I've fixed stuff up.

[Kevin Buzzard]

I've opened a ticket at CoCalc. It's beyond me.

[Patrick Massot]

Kevin Buzzard said:

I want to let users interact with a Lean file without installing Lean. Unfortunately the Lean file I want to let them interact with is part of a lean project and involves imports of other files in the project. My understanding is that this means that the community web editor can't do it without just cutting and pasting all imports on the top, which is sometimes unfeasible.

CoCalc is great, but that preliminary comment is wrong. You can use your own library in the Lean web editor, but you need to host it somewhere.

[Kevin Buzzard]

All I want to do is to share a link. I don't want to host anything, I don't think.

[Patrick Massot]

I mean: could that be a link to your Webpage?

[Kevin Buzzard]

Ok let's say that it could be. Then you are telling me to put a whole bunch of stuff in http://wwwf.imperial.ac.uk/~buzzard/xena/ ?

[Patrick Massot]

I'm saying this is an option.

[Patrick Massot]

In my course I'm offering all three options: local Lean+VScode, CoCalc, LeanWeb.

[Patrick Massot]

Instructions can be found at https://github.com/bryangingechen/lean-web-editor. This yet another thing that should be integrated to leanproject (something like leanproject web and then copy everything to you web server), but days last only 24 hours.