Zulip Chat Archive

Stream: new members

Topic: CoCalc functionality


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 23:38):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 23:51):

sure

view this post on Zulip Alex Mathers (Apr 15 2020 at 23:51):

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

view this post on Zulip Alex Mathers (Apr 15 2020 at 23:51):

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

view this post on Zulip Alex Mathers (Apr 15 2020 at 23:51):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 23:51):

or whatever you want to call that directory

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 23:52):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 23:57):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 23:58):

What is the current contents of leanpkg.path?

view this post on Zulip Alex Mathers (Apr 15 2020 at 23:58):

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

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 23:59):

Delete the first line

view this post on Zulip Kevin Buzzard (Apr 15 2020 at 23:59):

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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:00):

Does your project depend on mathlib?

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:00):

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

view this post on Zulip 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.

view this post on Zulip Alex Mathers (Apr 16 2020 at 00:01):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:03):

Does it work?

view this post on Zulip Alex Mathers (Apr 16 2020 at 00:03):

No :/

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:03):

What's the error?

view this post on Zulip Alex Mathers (Apr 16 2020 at 00:04):

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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:04):

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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:04):

I mean, what does the file say?

view this post on Zulip Alex Mathers (Apr 16 2020 at 00:04):

import rtg.basics

view this post on Zulip Alex Mathers (Apr 16 2020 at 00:04):

Is all there is in the file

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:06):

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

view this post on Zulip Alex Mathers (Apr 16 2020 at 00:06):

Yeah there is

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:06):

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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:06):

there is a button with two going-round arrows

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:09):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:11):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Alex Mathers (Apr 16 2020 at 00:12):

Yeah I'd believe that for sure

view this post on Zulip Alex Mathers (Apr 16 2020 at 00:14):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:14):

(I just checked on one of my cocalc projects)

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Alex Mathers (Apr 16 2020 at 00:56):

Gotcha

view this post on Zulip Alex Mathers (Apr 16 2020 at 00:57):

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

view this post on Zulip 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