Kevin Buzzard (Apr 02 2020 at 22:58):
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]
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
.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
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 (Apr 02 2020 at 22:59):
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 (Apr 02 2020 at 23:08):
[just remembered I can test it myself with a private browser window, and it doesn't, so these instructions still need work]
Gabriel Ebner (Apr 03 2020 at 10:08):
Kevin Buzzard (Apr 03 2020 at 10:09):
Yeah I need to share the entire project I think, which I don't know how to do.
Gabriel Ebner (Apr 03 2020 at 10:09):
Sorry, missed the "it doesn't" comment.
Kevin Buzzard (Apr 03 2020 at 10:19):
Kevin Buzzard (Apr 03 2020 at 10:20):
Kevin Buzzard (Apr 03 2020 at 10:21):
no I am still not sharing my Lean path it seems
Kevin Buzzard (Apr 03 2020 at 10:23):
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 (Apr 03 2020 at 10:34):
I think everything is broken right now. I'll let people know when I've fixed stuff up.
Kevin Buzzard (Apr 03 2020 at 11:03):
I've opened a ticket at CoCalc. It's beyond me.
Patrick Massot (Apr 03 2020 at 13:48):
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 (Apr 03 2020 at 13:49):
All I want to do is to share a link. I don't want to host anything, I don't think.
Patrick Massot (Apr 03 2020 at 13:50):
I mean: could that be a link to your Webpage?
Kevin Buzzard (Apr 03 2020 at 14:39):
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 (Apr 03 2020 at 14:39):
I'm saying this is an option.
Patrick Massot (Apr 03 2020 at 14:40):
In my course I'm offering all three options: local Lean+VScode, CoCalc, LeanWeb.
Patrick Massot (Apr 03 2020 at 14:43):
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.
Last updated: May 14 2021 at 06:16 UTC