CoCalc functionality

Stream: new members

[Alex Mathers]

Hi, anybody have experience with using Lean in CoCalc? I'm trying to figure out how to have multiple Lean files in a single project and import one into another

[Kevin Buzzard]

You need to put your leanpkg.path in the root directory of your cocalc project and adjust it accordingly.

[Kevin Buzzard]

e.g. if in your cocalc project you have a directory my_lean_project containing as usual a leanpkg.path and a leanpkg.toml, and a subdirectory src where all your Lean files are, then you need to move that leanpkg.path one directory up to the root of the cocalc project

[Kevin Buzzard]

and then you'll have to add my_lean_project in the appropriate places, e.g. it might look like this if your project imports mathlib:

builtin_path
path my_lean_project/_target/deps/mathlib/src
path my_lean_project/src

[Kevin Buzzard]

An alternative is just to dump the lean project in the root cocalc directory, then you can put files in src and have a line path src in your leanpkg.path file.

[Alex Mathers]

@Kevin Buzzard I don't seem to be allowed to make changes to the root directory, even just adding a folder, I get an "access denied" error. Do you know a way past this?

[Kevin Buzzard]

By the root directory of your cocalc project I just mean ~. If you can't access the root directory of your own cocalc project then where are you putting your files?

[Alex Mathers]

Oh, I saw a path called .smc/root and I thought you meant there. So you just mean the "home page" of the project

[Kevin Buzzard]

I mean the directory where all your files are. Sorry if I called it something wrong.

[Alex Mathers]

No problem. I'm still having issues, would you be willing to look at some screenshots to see if what I'm doing matches what you're saying?

[Kevin Buzzard]

sure

[Alex Mathers]

Screen-Shot-2020-04-15-at-4.46.24-PM.png

[Alex Mathers]

Screen-Shot-2020-04-15-at-4.46.39-PM.png

[Alex Mathers]

Screen-Shot-2020-04-15-at-4.46.52-PM.png

[Kevin Buzzard]

OK so the problem is that you have not put leanpkg.path in the root directory of your cocalc project.

[Kevin Buzzard]

or whatever you want to call that directory

[Kevin Buzzard]

currently leanpkg.path is in a subdirectory of the root directory called my_lean_project.

[Kevin Buzzard]

It's in the root directory of your lean project as opposed to the root directory of your cocalc project

[Kevin Buzzard]

also your leanpkg.path contains invalid paths, such as leanpkg.path. The paths are relative to the directory that leanpkg.path is in, so once you've put leanpkg.path into the root directory of your cocalc project, the path src and ./src will also be invalid because you have no src in the root directory of your cocalc project.

[Kevin Buzzard]

Finally, Lean will not be able to import subgrp.lean and basics.lean because they are not in directories which are in your path. They should probably be in your Lean project as opposed to floating around outside it.

[Kevin Buzzard]

Unless they're not part of the project at all.

[Alex Mathers]

Okay so now things look like this: Screen-Shot-2020-04-15-at-4.55.43-PM.png

[Alex Mathers]

I have copies of basics.lean and subgrp.lean in src/rtg/, I just have copies also in the home directory for convenience of testing these things

[Kevin Buzzard]

What is the current contents of leanpkg.path?

[Alex Mathers]

Screen-Shot-2020-04-15-at-4.58.33-PM.png

[Kevin Buzzard]

Delete the first line

[Kevin Buzzard]

and ideally the last one too because it's a duplicate of the one before

[Kevin Buzzard]

Does your project depend on mathlib?

[Kevin Buzzard]

because no mathlib imports will work with this set-up either

[Kevin Buzzard]

leanpkg.path just just be builtin_path and then a list of all the paths, relative to the root directory of the cocalc project, of where all the lean files are which you want to import.

[Alex Mathers]

I'd like to use some mathlib things, yeah. I deleted the first and last line

[Alex Mathers]

I took src from some hidden files and just moved it to the front so it has all of mathlib in it

[Kevin Buzzard]

Does it work?

[Alex Mathers]

No :/

[Kevin Buzzard]

What's the error?

[Alex Mathers]

1:0 error
file 'rtg/basics' not found in the LEAN_PATH
1:0 error
invalid import: rtg.basics
could not resolve import: rtg.basics

[Kevin Buzzard]

and what is the line of the file which gives you the error?

[Kevin Buzzard]

I mean, what does the file say?

[Alex Mathers]

import rtg.basics

[Alex Mathers]

Is all there is in the file

[Kevin Buzzard]

And do you have a file called SOMETHING/rtg/basics.lean where SOMETHING is one of the lines in your leanpkg.path file?

[Alex Mathers]

also here is what /src looks like in case that matters: Screen-Shot-2020-04-15-at-5.04.33-PM.png

[Kevin Buzzard]

what matters is whether there is a file called basics.lean in the directory rtg

[Alex Mathers]

Yeah there is

[Kevin Buzzard]

Oh -- did you restart Lean after you edited your path file?

[Kevin Buzzard]

there is a button with two going-round arrows

[Kevin Buzzard]

By the way, where did you get your mathlib olean files from? You will have to be careful to make sure that they are compiled using the same version of Lean as the one in CoCalc, or they will all be recompiled and there will be green squares there for 15 minutes

[Alex Mathers]

That's hilarious, that did something. Now the error message is imported file '/home/user/src/rtg/basics.lean' uses sorry which feels less aggressive

[Alex Mathers]

And I think that's just coming up because some things in basics use sorry at the moment, actually

[Kevin Buzzard]

Sorting out the leanpkg.path file is not the hard part.

[Kevin Buzzard]

The hard part, if you're using your own mathlib, is to make sure it's compatible with cocalc's Lean which is something like 3.5.1

[Alex Mathers]

when I "unhid" hidden files on the home page I was able to follow the directory .smc/root/ext/lean/lean/mathlib/src and there was where I found all the mathlib files. The /src is the file I just copied to the home folder

[Kevin Buzzard]

oh that's great. Did you also move the olean files?

[Kevin Buzzard]

I suspect that you didn't even need to copy them, and that the builtin_path will actually point to the mathlib files

[Alex Mathers]

I don't think so. I moved /src and leanpkg.toml and leanpkg.path and that's it

[Alex Mathers]

Yeah I'd believe that for sure

[Alex Mathers]

Navigating this type of stuff is so unnatural for me right now. Hopefully will adapt

[Kevin Buzzard]

Alex Mathers said:

I don't think so. I moved /src and leanpkg.toml and leanpkg.path and that's it

src is full of olean files

[Kevin Buzzard]

(I just checked on one of my cocalc projects)

[Alex Mathers]

I see. Then I guess I did. I'm not even sure what an olean file is tbh so I just guessed

[Kevin Buzzard]

It's the difference between "your project works" and "I am going to spend 15 minutes compiling because you imported data.real.basic"

[Alex Mathers]

Sounds important. Looking through files now I'm seeing that we have one corresponding to every .lean file it looks like. When I try to open one up it's not clear at all what's going on in there

[Kevin Buzzard]

you definitely don't want to open them, and if you press just one key when one of them is open then you probably screwed everything up

[Kevin Buzzard]

Any edit to an olean file will mean that your project will have to recompile it and all files which import it, I suspect, because this issue was fixed but I think it hadn't been fixed by 3.5.1

[Alex Mathers]

Gotcha

[Alex Mathers]

Thanks a ton for helping out, sorry it took a while

[Patrick Massot]

I don't have time to read this thread, so I'll post a blind answer just in case:

How to use Lean on CoCalc

• If you have a collection of autonomous Lean files, each of them relying only on mathlib (and not needing a cutting edge mathlib): put them anywhere in you CoCalc project, open them, enjoy

• If you have a collection of files relying on each other and on mathlib (and not needing a cutting edge mathlib):

  • Put them in some folder my_stuff in the project home folder

  • In the project home folder, before opening any Lean file, create a file named leanpkg.path containing:
    builtin_path path /ext/lean/lean/mathlib/src path ./my_stuff
    If you opened a Lean file before creating this file you'll need to restart the Lean server by clicking the restart icon on top of the file.

  • If something in your stuff requires heavy compiling (say you actually have a library of stuff and then exercises files) then open a terminal in CoCalc and lean --make my_stuff (or lean --make my_stuff/my_heavy_file.lean).

Note also that getting a cutting edge mathlib is currently not possible, because this requires a cutting edge Lean, that CoCalc doesn't have.