## Stream: new members

### Topic: CoCalc functionality

#### Alex Mathers (Apr 15 2020 at 21:23):

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 (Apr 15 2020 at 21:35):

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

#### Kevin Buzzard (Apr 15 2020 at 21:36):

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 (Apr 15 2020 at 21:37):

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 (Apr 15 2020 at 21:38):

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 (Apr 15 2020 at 23:32):

@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 (Apr 15 2020 at 23:33):

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 (Apr 15 2020 at 23:38):

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 (Apr 15 2020 at 23:38):

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

#### Alex Mathers (Apr 15 2020 at 23:49):

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?

sure

#### Alex Mathers (Apr 15 2020 at 23:51):

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

#### Alex Mathers (Apr 15 2020 at 23:51):

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

#### Alex Mathers (Apr 15 2020 at 23:51):

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

#### Kevin Buzzard (Apr 15 2020 at 23:51):

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

#### Kevin Buzzard (Apr 15 2020 at 23:51):

or whatever you want to call that directory

#### Kevin Buzzard (Apr 15 2020 at 23:52):

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

#### Kevin Buzzard (Apr 15 2020 at 23:52):

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

#### Kevin Buzzard (Apr 15 2020 at 23:55):

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 (Apr 15 2020 at 23:56):

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 (Apr 15 2020 at 23:57):

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

#### Alex Mathers (Apr 15 2020 at 23:57):

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

#### Alex Mathers (Apr 15 2020 at 23:57):

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 (Apr 15 2020 at 23:58):

What is the current contents of leanpkg.path?

#### Alex Mathers (Apr 15 2020 at 23:58):

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

#### Kevin Buzzard (Apr 15 2020 at 23:59):

Delete the first line

#### Kevin Buzzard (Apr 15 2020 at 23:59):

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

#### Kevin Buzzard (Apr 16 2020 at 00:00):

Does your project depend on mathlib?

#### Kevin Buzzard (Apr 16 2020 at 00:00):

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

#### Kevin Buzzard (Apr 16 2020 at 00:00):

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 (Apr 16 2020 at 00:01):

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

#### Alex Mathers (Apr 16 2020 at 00:02):

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

Does it work?

No :/

#### Kevin Buzzard (Apr 16 2020 at 00:03):

What's the error?

#### Alex Mathers (Apr 16 2020 at 00:04):

1:0 error
1:0 error
invalid import: rtg.basics
could not resolve import: rtg.basics

#### Kevin Buzzard (Apr 16 2020 at 00:04):

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

#### Kevin Buzzard (Apr 16 2020 at 00:04):

I mean, what does the file say?

#### Alex Mathers (Apr 16 2020 at 00:04):

import rtg.basics

#### Alex Mathers (Apr 16 2020 at 00:04):

Is all there is in the file

#### Kevin Buzzard (Apr 16 2020 at 00:05):

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 (Apr 16 2020 at 00:05):

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

#### Kevin Buzzard (Apr 16 2020 at 00:06):

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

Yeah there is

#### Kevin Buzzard (Apr 16 2020 at 00:06):

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

#### Kevin Buzzard (Apr 16 2020 at 00:06):

there is a button with two going-round arrows

#### Kevin Buzzard (Apr 16 2020 at 00:07):

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 (Apr 16 2020 at 00:08):

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 (Apr 16 2020 at 00:09):

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

#### Kevin Buzzard (Apr 16 2020 at 00:09):

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

#### Kevin Buzzard (Apr 16 2020 at 00:10):

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 (Apr 16 2020 at 00:11):

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 (Apr 16 2020 at 00:11):

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

#### Kevin Buzzard (Apr 16 2020 at 00:12):

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 (Apr 16 2020 at 00:12):

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

#### Alex Mathers (Apr 16 2020 at 00:12):

Yeah I'd believe that for sure

#### Alex Mathers (Apr 16 2020 at 00:14):

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

#### Kevin Buzzard (Apr 16 2020 at 00:14):

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 (Apr 16 2020 at 00:14):

(I just checked on one of my cocalc projects)

#### Alex Mathers (Apr 16 2020 at 00:15):

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

#### Kevin Buzzard (Apr 16 2020 at 00:15):

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 (Apr 16 2020 at 00:20):

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 (Apr 16 2020 at 00:26):

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 (Apr 16 2020 at 00:27):

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

Gotcha

#### Alex Mathers (Apr 16 2020 at 00:57):

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

#### Patrick Massot (Apr 16 2020 at 08:10):

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.

Last updated: May 13 2021 at 16:25 UTC