CoCalc

Stream: general

[Patrick Massot]

Someone sent me this link: https://twitter.com/cocalc_com/status/990971941308727296

This is how calculating a Fibonacci number in #leanprover looks like on #CoCalc! http://leanprover.github.io/ https://twitter.com/cocalc_com/status/990971941308727296/photo/1

- CoCalc (@cocalc_com)

[Johan Commelin]

William told me he is finishing up his new collaborative editor for CoCalc

[Johan Commelin]

After that, a collaborative IDE for lean is somewhere on his todo list...

[Johan Commelin]

I am really excited about this!

[Kevin Buzzard]

We're going to use it over the summer. They like stable versions of software by default, and when mathlib 3.4.1 comes out I'm going to ask them to install it too. They didn't seem keen to stay up to date with mathlib HEAD but mathlib current is just fine as far as I am concerned.

[Kevin Buzzard]

It solves the massive headache of getting Lean installed on a random undergraduate's laptop, which can take forever especially if the errors are all in Italian and hence harder to google...

[Kevin Buzzard]

The big question is how much faster will it be than the lean web editor.

[William Stein]

I'm here in case anybody has any questions/comments/suggestions/mock ups for a LEAN ide mode that makes sense in cocalc/etc.

[Kevin Buzzard]

Hiya.

[Kevin Buzzard]

William, I've been trying to figure out what a canonical isomorphism is in Lean.

[Kevin Buzzard]

I was supposed to be finishing my schemes work but I got sucked down a real rabbithole

[Kevin Buzzard]

Lean is going to know what an affine scheme is as soon as I pull my finger out.

[Kevin Buzzard]

https://leanprover.github.io/live/latest/

[Kevin Buzzard]

That's what you're up against @William Stein

[Kevin Buzzard]

and I'm going to go and do some schemes

[Andrew Ashworth]

I think Lean 4 will allow a bit more flexibility when it comes to making interesting IDE assists, particularly with the parser upgrades and further development of the {! !} "hole" functionality

[Patrick Massot]

Lean in CoCalc seem to make a lot of progress:
https://github.com/sagemathinc/cocalc/search?q=lean&unscoped_q=lean

[Kevin Buzzard]

I can use Lean in CoCalc :-)

[Kevin Buzzard]

As of today

[Patrick Massot]

Do you mean you have access to a private beta-test?

[Kevin Buzzard]

Yes

[Kevin Buzzard]

Shall I live stream on twitch?

[Johan Commelin]

You shall!

[Patrick Massot]

Yeah!

[Gabriel Ebner]

I tried lean on cocalc earlier today and it worked out of the box. There is no autocompletion, no syntax highlighting, and no mathlib, but it shows error messages just like in vscode.

[Patrick Massot]

Do you mean public CoCalc or do you have special access?

[Gabriel Ebner]

Public cocalc. Just create a file with the .lean extension and it works.

[Patrick Massot]

synchronisation is completely random :(

[Johan Commelin]

I'm on an unpaid account, and the server is overloaded. I can't even create a file.

[Johan Commelin]

If someone wants to add me to their Lean test project, so that I can multiplayer on their files, I'dd appreciate that.

[Patrick Massot]

what is the email address associates to your account?

[Johan Commelin]

johan@commelin.net I think

[Patrick Massot]

You should receive an email

[Patrick Massot]

But it's hopelessly slow

[Johan Commelin]

Ok, you are also on an unpaid account?

[Patrick Massot]

Using Lean on CoCalc without paying doesn't seem possible

[Patrick Massot]

Yes

[Johan Commelin]

I should really get my uni to pay for an account.

[Johan Commelin]

At the moment it is completely unusable in general, I can't even create a terminal or such.

[William Stein]

Hi -- I created a non-free upgraded project on CoCalc just now. Here's a link:

[William Stein]

https://cocalc.com/projects/32a71772-8761-49d1-9134-6eb7f3fca4f5/files/?session=default

[William Stein]

I added everybody who commented above as collaborators to the project.

[Patrick Massot]

Thanks!

[William Stein]

Here's what it looks like:Screenshot-2018-08-31-at-11.14.49-AM.png

[Patrick Massot]

eheh, that's the lemma I just wrote

[William Stein]

Yep. By the way, anybody who is a collaborator on that project can add anybody else (in project settings).

[Patrick Massot]

The message window displays only info and errors, but not the current tactic state, this is similar to one of the Lean message display mode in VScode but I can't find the other one

[Gabriel Ebner]

@William Stein You need to request the goal state separately. It is not sent as part of the error messages. https://github.com/leanprover/lean-client-js/blob/83f190d044502d1cd39f320ef15da5357547d539/lean-client-js-core/src/commands.ts#L87-L114

[William Stein]

Gabriel -- thanks. I didn't realize that. I'll add that to the todo list.

[William Stein]

Is there something like prettier or yapf (inspired by Gofmt) for lean code? We are pushing out "sort of" canonical format support like that as much as possible all over in cocalc...

[Patrick Massot]

That's great, I can prove random stuff that we already have

[Patrick Massot]

Now it's time for dinner, but many thanks!

[Kevin Buzzard]

Thanks so much for the work you've done on this William!

[Johan Commelin]

This is awesome! Thank you very much!

[Johan Commelin]

@William Stein The prettier will likely be added in the next version of Lean (Lean 4).

[Johan Commelin]

See also: https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/VScode.20extension/near/133129165

[Scott Morrison]

Could someone add me as a collaborator on that project?

[Patrick Massot]

I hope I just did that

[Patrick Massot]

And I'm happy to see that everybody seems to haved managed to travel back from Orsay!

[Kevin Buzzard]

I wrote a few lines of code in a test document and then sent William some comments (in the project chat) about which points of the workflow were currently harder in CoCalc than in VS Code. It seemed much quicker than the Lean Web Editor -- it was slower than local VS Code of course, but certainly fast enough to be usable (especially by beginners). The main things we're missing are: (1) mathlib (2) view of goal in tactic mode and (3) tab completion. Also syntax highlighting but for me that wasn't really a deal breaker.

[William Stein]

I just improved the syntax highlighting a bit, so it's maybe usable now (it wasn't before). I haven't done anything else yet. Screenshot-2018-09-04-at-9.32.57-PM.png

[Johan Commelin]

Hooray! That's really nice.

[Scott Morrison]

This looks really promising!

[Scott Morrison]

Is it right that there isn't a "goal display" mode yet? Or am I just missing it. I know for people who work in term mode all the time it's not critical, but for beginners and mathematicians who use tactic mode all the time it is very helpful.

[Johan Commelin]

It is on the todo list.

[Kevin Buzzard]

The big jobs which remain, I guess, are: (1) access to mathlib [e.g. reading LEAN_PATH or leanpkg.path I guess] (2) displaying goals in tactic mode (3) tab completion (4) hover over function name -> mini window with definition / docstring; I guess that of these, (1) and (2) are the ones which I really need for my teaching (I'd also need an extension of (1), which is "read my library too").

[Kevin Buzzard]

@Harald Schilly I downloaded and I believe compiled mathlib about two days ago on a cocalc project if this helps.

[Kevin Buzzard]

There's a project called LEAN that I have access to on CoCalc (as do several of us) and in _target/deps/mathlib is a only-a-few-days-old mathlib, compiled using CoCalc's servers.

[Harald Schilly]

yes, I'm in that project. so, the goal I think is to compile a recent version of mathlib globally (currently a path like /ext/lean/.../lean/mathlib) and make it picked up by default by lean. I don't know that part about picking it up automatically. That's all.

[Mario Carneiro]

The lean path is specified in leanpkg.path in the current project folder

[Mario Carneiro]

You can put things like ../lean/mathlib in it

[Mario Carneiro]

That will bypass leanpkg somewhat, though - commands like leanpkg configure will clobber the file

[Mario Carneiro]

To make it stick you could install mathlib in ~/.leanpkg (I believe this is where leanpkg install puts stuff), and then add a dependency to mathlib in the leanpkg.toml file

[Mario Carneiro]

This is the way most users do it, I think

[Sebastian Ullrich]

@Mario Carneiro packages in ~/.leanpkg are only used by stand-alone files not contained in packages

[Kenny Lau]

how does this work?

[Kevin Buzzard]

What do you mean?

William wrote some code and now you can use Lean at CoCalc, but there are still some things missing (like displaying goal in tactic mode, and autocompletion, last time I looked). My plan is to offer it to the 1st years.

[Kenny Lau]

well I just went to it and I can't use anything

[Kevin Buzzard]

can you be more precise? I go to it and I can use Lean

[Kenny Lau]

apparently only a few people have access

[Johan Commelin]

@Kenny Lau You have to create a .lean file. And supposedly if you click on it, the Lean editor should open.

[Johan Commelin]

But it might not be usable at all on a free account.

[Harald Schilly]

This is the way most users do it, I think

Hi again. Just to clarify what my goal in this "CoCalc" stream (is this the term?) is: the situation is a course, where many who are now to lean want to follow examples and experiment around. The underlying infrastructure is a linux-based multi-user environment. This means, there is a common read-only directory where we (administrators of the online service) can install lean and everyone accesses it from there. Additionally, it would be good to have mathlib and maybe another library available globally. The goal is to give everyone a good "out of the box" experience, such that these libraries work without much overhead. In Python, there are global "site" directories, but with lean this seems to be different -- or well -- I haven't understood it yet. So, my understanding here is, every student should setup their own lean-specific directory and inside of it is a leanpkg.path file. What's exactly the content? Or should it rather be a leanpkg.toml file? Sorry, I'm a complete lean novice :rolling_eyes:

[Kevin Buzzard]

leanpkg.toml is for the leanpkg package manager. If the package installed correctly initially, it won't need to be managed. leanpkg.path is the file which, conventionally (on a single user install) the IDE reads so it knows where the paths are which will be looked in when the IDE runs into a line of the form import data.equiv.basic -- it will look through the entries in leanpkg.path until it finds a line corresponding to a directory containing data/equiv/basic.lean. So neither of them are actually essential for the set-up to work.

[Kevin Buzzard]

An example of how I use leanpkg.toml is that if I have a project which has mathlib as a dependency, and if mathlib upgrades, I can upgrade my local version of mathlib using the leanpkg upgrade command. The students will not need to be upgrading any particular packages (and indeed they'd need internet access for this to work).

[Kevin Buzzard]

I upgrade mathlib because it changes a lot right now (many commits per week) and some of them are new functions or theorems which I need. But my students won't need anything so bleeding-edge.

[Chris Hughes]

It's not just advanced mathematics that's getting PRed, some of it is things like int.cast_pow, which I think they might need. Over the summer I added quite a few trivial little lemmas like this when people needed them.

[Kevin Buzzard]

yes but one of the points of the summer project was to make sure we'd have everything we need in mathlib by October. What's the situation with cos by the way? ;-)

[Johan Commelin]

@Harald Schilly You seem to be in a European timezone. Is that right? Where exactly are you based? Because it might be feasible to meet up with one of the people who really know how this stuff works...

[William Stein]

@Harald Schilly is in Vienna, Austria.

[William Stein]

Screenshot-2018-09-12-at-12.20.10-PM.png

[William Stein]

I implemented "tab completion". You have to actually press the tab key to get completions. It first shows once that can be determined in the browser (so standard keywords, functions, etc.,), then it shows the results that come back from the lean server.

[Mario Carneiro]

Can the keywords show with a different icon or color than the constants?

[William Stein]

@Kenny Lau I invited you to the lean cocalc project, in case you want to try it.

[Kenny Lau]

lol how do you know who I am

[Mario Carneiro]

also, hopefully once results come back from lean you can put the types of the constants in that list as well, that's pretty important

[William Stein]

@Mario Carneiro I'll add that to the todo list, along with showing type information, for later. I'm only going to do stuff now that is absolutely critical for Kevin's course. I think some sort of lean path configuration should be next on my list.

[Patrick Massot]

Kenny you complained in this thread you didn't have access

[Mario Carneiro]

that's fine, I just wanted you to know what would be helpful

[Harald Schilly]

@Harald Schilly You seem to be in a European timezone.

yes, vienna as william said. do you know if there is someone active with lean at the university of vienna? that could be quite interesting.

[William Stein]

@Mario Carneiro I just added you to the project too.

[Kenny Lau]

Kenny you complained in this thread you didn't have access

yes I did, but I didn't say what my account is

[Kenny Lau]

somehow WS managed to find my account

[William Stein]

@Mario Carneiro -- yes, I've been comparing with VS code...

[Patrick Massot]

Isn't @Gabriel Ebner in Vienna?

[William Stein]

@Kenny Lau -- I just typed your name into the collaborator search and it was the only result.

[Harald Schilly]

@Patrick Massot sounds like a name that could be from over here!

[Kenny Lau]

fair enough

[Patrick Massot]

https://gebner.org/

[Harald Schilly]

nice

[Patrick Massot]

I think he is currently on vacations

[Patrick Massot]

And, very conveniently, he is the maintainer of the VScode Lean extension

[William Stein]

I'm going to work on displaying "the current tactic state" next.

[William Stein]

Kevin, for your course, as long as I make it possible to easily set LEAN_PATH, or even just make it set to some default (e.g., /home/user/lean), then you could just rsync out /home/user/lean to all student projects. You would just update it in your project whenever you want, test it, then click a button to push it out to students whenever you want.

[William Stein]

I'll set LEAN_PATH to ~/lean right now, since it's a fairly easy change to make, anyways.

[William Stein]

Or is that not nearly enough, because it'll have to be customizable with lots of colons to detect many directories?

[Kevin Buzzard]

I guess we either need several directories, or we do the horrible thing of putting them all in the same directory giving a huge mess of core lean and mathlib and my stuff all mixed together

[Sebastian Ullrich]

Yes, it is expected that there is a separate entry for each package in LEAN_PATH. I suppose for Kevin's students it should be sufficient to include ., the global mathlib path, and Lean's library folder in there

[Sebastian Ullrich]

Note that this effectively disables leanpkg (i.e. importing custom dependencies, as well as importing files relative to the package root)

[William Stein]

I could have it just read ~/leanpkg.path if it exists. My only worry is that students would mess it up; also there is no easy way to push out a top level file to students right now...

[William Stein]

OK, for now how about: LEAN_PATH=.:/ext/lean/mathlib:[whatever lean's library folder is??]

[William Stein]

But what is lean's library folder?

[William Stein]

How do I determine that?

[Mario Carneiro]

it is lean/library

[William Stein]

It's OK that lean/library is not an absolute path?

[William Stein]

Also, what is a very simple "hello word" style test of LEAN_PATH?

[William Stein]

Here's what I'm currently doing:

[William Stein]

[William Stein]

    process.env.LEAN_PATH = `${process.env.HOME}:${process.env.HOME}/lean:/ext/lean/mathlib:lean/library`;
    this._server = new lean_client.Server(
      new lean_client.ProcessTransport("lean", ".", [])
    );

[Chris Hughes]

import data.finset is probably a reasonable test.

[William Stein]

With the above LEAN_PATH, I get this error from #print "hello":

file 'init' not found in the LEAN_PATH

[Sebastian Ullrich]

lean/library should be an absolute path; no magic there

[Sebastian Ullrich]

I.e. append /library to where you store Lean

[William Stein]

I don't know where we store lean. Also, it can very based on if the user is using cocalc.com or cocalc-docker.

[Sebastian Ullrich]

I see. You can ask Lean: lean --path

[William Stein]

ok, that works perfectly.

[William Stein]

What does this mean exactly - this is just the default already with me changing nothing?

~/cocalc/src$ lean --path
{
  "is_user_leanpkg_path": true,
  "leanpkg_path_file": "/home/user/.lean/leanpkg.path",
  "path": [
    "/ext/lean/lean-3.4.1-linux/bin/../library",
    "/ext/lean/lean-3.4.1-linux/bin/../lib/lean/library",
    "/home/user/.lean/_target/deps/mathlib/.",
    "/home/user/.lean/./."
  ]
}

[William Stein]

E.g., does it mean users can already customize their path by editing the file /home/user/.lean/leanpkg.path, so that's already done?

[Kevin Buzzard]

I think they're not supposed to touch that file, which is auto-generated by the package manager

[Kevin Buzzard]

The package manager looks at leanpkg.toml and sees the dependencies of the project.

[Kevin Buzzard]

It looks to me like mathlib is a dependency for that project because dependency projects are downloaded to _target/deps

[William Stein]

How can I try importing something from mathlib to see what happens?

[Kevin Buzzard]

Make a file blah.lean with the line import data int.basic and then compile it

[Kevin Buzzard]

If that mathlib directory actually exists and has a mathlib in then it might work

[Kevin Buzzard]

I'm afraid I'm afk right now though

[Patrick Massot]

He means import data.int.basic he missed a point

[William Stein]

Cool -- it looks like it just works once somebody has installed mathlib already in the standard way and restarted the project in project settings. Cool.

[Sebastian Ullrich]

I thought the goal was to not have mathlib installed in the standard (user-specific) way but precompiled in a global path?

[William Stein]

@Sebastian Ullrich -- maybe. I'm still confused. It just happens to be the case that mathlib is installed for the user for this test project, and it's important to also support that case too, I guess. For example, Kevin's class could just push out a custom ~/.lean to the students and it might just work... then he can update it every day if he wants.

[Sebastian Ullrich]

Yes, if Kevin can just push his ~/.lean with prebuilt mathlib to all students, it should just work for them. At least as long as they use stand-alone .lean files; if they create their own Lean packages, the ~/.lean packages will not be visible anymore until they add them back as dependencies to the new package

[William Stein]

Oh my gosh this path stuff is driving me crazy. I'm deleting all the code I've written related to it and just going to ensure lean starts in $HOME.

[William Stein]

Look -- if all users on a system are supposed to have access to an extra package, namely mathlib, which is installed systemwide, what is the admin supposed to do in order to install that package?

The answer in python is to become root, set umask properly, then do pip install packagename. What is the answer for LEAN?

[Sebastian Ullrich]

You have to include that directory in either LEAN_PATH or ~/.lean/leanpkg.path (or tell users to create a new package and add it as a dependency there). leanpkg is directly inspired by Rust's package manager, which like all modern package managers is focused on reproducible build environments and does not really have a notation of global packages.

[William Stein]

does not really have a notation of global packages.

OK, thanks for the clarification. I'll take as an axiom then that "lean does not have global packages", and won't do anything further for now in that direction. I'll let Kevin have his students install mathlib themselves into their projects, or have him push out an install to all student projects. I'm moving on to showing tactic state.

[Gabriel Ebner]

@Harald Schilly My office is at the Freihaus of the TU Wien. Feel free to stop by (but make sure I'm there first). I'll be back from vacation in the second week of October.

[William Stein]

LEAN in CoCalc now has a new "Info at Cursor" panel, which shows the tactic at the cursor, and also other info about what's at the cursor.

Screenshot-2018-09-12-at-8.31.00-PM.png

[William Stein]

I also made numerous small changes so the UI does not get slowed down by trying to render too much. I might have introduced too much "debouncing" here though.

So, Kevin, I think this is the absolute bare minimum of functionality needed for your course. You'll have to build all the library stuff, then push it out to the student projects, since LEAN has no notion of global packages, as discussed above. I think if you install packages, etc., etc., then restart a project in cocalc (project settings --> restart project), then LEAN will run as if it is being run from $HOME, so it'll pick up those packages.

The other problem is that sometimes one has to close and open a file if it isn't syncing. This is on my immediate todo list.

[Mario Carneiro]

I think there is a bug in the printing of the tactic info - it says expr when it should say exact expr

[Harald Schilly]

It's OK that lean/library is not an absolute path?

my understanding is that this is in the lib subdirectory, i.e. /ext/lean/lean/lib/lean/library/

ok ... but I see this is already somewhat resolved. looks like it is possible to have mathlib globally, but there is no common way to make it available by default. it's sort of opt-in...

[Kenny Lau]

@Reid Barton maybe you can use cocalc now instead of twitch

[Kenny Lau]

maybe we should all join a discord group

[Kenny Lau]

is that a good idea?

[Kevin Buzzard]

So for those who haven't experimented recently, I've just been playing with a lean file at CoCalc with Kenny -- true multiplayer Lean! There are now two windows you can have for messages corresponding to the two VS Code windows -- one which reports all output and one which prints the goal when you're in a tactic proof. Underscores work! Tactic proofs are now fine.

[Kevin Buzzard]

The most obvious thing for me, when writing code, that is better in VS Code than in CoCalc, is that VS Code does cleverer auto-completion -- it chooses more wisely, and for the highlighted choice it displays the type of the term and also the docstring if any. Here are some examples:

[Kevin Buzzard]

vscode.png

cocalc1.png

cocalc2.png

[Kevin Buzzard]

For VS Code we see filter.map + type + docstring. For cocalc the guessing is less good (VS Code correctly guesses I want filter.ma<something>) and I don't see the types of the possibilities, which is really important for when you're using functions which are unfamiliar to you.

But this is a very mild thing. In the last week there has been huge progress!

[Patrick Massot]

Yes, the progress looks impressive

[William Stein]

But this is a very mild thing.

CoCalc has the exact same completion info available, but all I did with it was sort in alphabetical order and display the names. I don't know what order I should sort in (or should I just NOT sort and leave things in whatever order the LEAN server outputs)? Displaying the type, etc., info is probably easy now that the hard part is done (which is getting completions to display at all). The CodeMirror show-hint plugin API is very rich regarding showing more than just a string in a completions box. It sounds like you're pretty happy with what vscode shows, so I should just look in the code to see what it does with what comes back from the LEAN server. @Gabriel Ebner ?

[William Stein]

I think there is a bug in the printing of the tactic info - it says expr when it should say exact expr

That's weird since I'm just printing what the lean server returns with no processing.

[Mario Carneiro]

Do you know what word you are completing when you ask for completions?

[Mario Carneiro]

I think VSCode prioritizes maximum subsequences, and initial segments relative to the query

[William Stein]

@Mario Carneiro yes, you know precisely what the "CodeMirror token" is, where the cursor is, etc.
Can somebody point me at the relevant code in the vscode mode? -- maybe I can just copy it over and use it with minimal change.

[Mario Carneiro]

I think this is default vscode behavior

[William Stein]

OK, so I guess the same question, but for vscode's source code... of course, I can try to hunt it down.

[Reid Barton]

Could someone (@William Stein?) add me to the Lean test project? Same email address on CoCalc as here

[William Stein]

@Reid Barton -- done.

[William Stein]

And as always, anybody on the project can add anybody else by clicking "Settings" in the project, then typing a name or email address at "Add New Collaborators".

[William Stein]

@Reid Barton once in, click on Log to see which files people opened when.

[William Stein]

@Kevin Buzzard I'll work on adding the extra type, etc., info to completions right now -- it seems like it's really useful for people (remember, I'm still sort of clueless about LEAN itself!)

[Kevin Buzzard]

Yes -- sorry. Here's how it works. As I'm sure you're aware, in "raw" mode, Lean wants to know proofs of every single little thing you do, so e.g. if you have a=b+c and you want to deduce c=a-b (and you are not intending on using Lean's automation to try and prove this automatically) then you are going to have to find the name of this theorem, or a related theorem which will get you half way there or whatever. Now there's an elaborate naming convention, so you tend to start guessing that this lemma is called something like "sub_of_add...something" or "sub_iff_add..." or maybe if these things are integers you might try "int.add_of_..." and you start playing around with auto-completion, trying to find the exact lemma you want. And in fact the moment I type sub_of Lean starts suggesting possible lemmas (here the type will be the statement of the lemma) and you can use up and down arrow to look through them to find the exact one you want (or one which is near enough, e.g. you have to turn a=b into b=a and you remember that this is called eq.symm etc).

vscode2.png

There's a screenshot of this in action.

[Patrick Massot]

Oh oh, I made a mistake. I close the CoCalc subwindow showing all messages. Now I have no idea how to reopen it.

[Kevin Buzzard]

game over

[Kevin Buzzard]

You can make more windows with the [|] and [-] boxes

[William Stein]

Patrick -- options: (1) just close all the frames and it goes back to the default, or (2) split any frame, then select the new frame (or old) and change it from what it is to what you want.

[Kevin Buzzard]

and then change what they display with a drop down menu just by it

[William Stein]

And (3), suggest a new button for me to add to make creating frames clearer!

[William Stein]

Yep, @Kevin Buzzard just did (2). (1) is also useful -- there is a default layout, and you get that by click the x in the upper right until there are no windows.

[William Stein]

Note that your frame layout is stored in localStorage on your browser; it's not sync'd across users or other browsers.

[Patrick Massot]

Thanks, I managed to get back my frames

[Patrick Massot]

I think I may have revealed that I never used CoCalc before... But I swear I use standalone Sage!

[Kevin Buzzard]

so the screenshot is displaying a bunch of random terms which have been defined, and the algorithm appears to be that the characters in sub_of appear, in that order, in the name of the term.

[Patrick Massot]

This Lean in CoCalc is amazing

[Reid Barton]

In emacs, each item in that completion list includes the type (in the format name : type), so all the types are visible at once

[Patrick Massot]

Now I need to find how to get my university to pay enough money so that my 40 students that will be using Lean during spring can use that instead of trying to install Lean at home

[Reid Barton]

If I were to clone another lean package in a subdirectory and leanpkg build it and then edit its files, would the editor pick up the correct lean path? I know for now the priority has been getting things set up properly for Kevin's students but I wonder whether it is also ready for more general use.

[Patrick Massot]

What is the meaning of the number in the title of CoCalc webpage? My tab in Firefox displays "(5) LEAN - CoCalc"

[William Stein]

Patrick: thanks! The number is files with unseen chats. It should also be the number on the bell in the upper right. It's basically like the number here in zulip, but just the number of "threads" .

Reid: thanks -- I will definitely add that -- the info is also sent to the frontend.

[Reid Barton]

I guess I will just try it unless you tell me it's a bad idea/definitely won't work

[Kevin Buzzard]

Reid can you send a screenshot of how it looks in emacs? I would be interested in comparing IDEs for Lean. I know you and Sebastian use emacs, and I was going to start when I was under the impression that it was going to be the only way I could possibly use Lean with cocalc, but when William decided to write his own interface for Lean I stopped again. I am really used to VS Code even though I've used emacs for 25 years and part of me would love to be doing Lean in emacs (it still annoys me that I can't do (or maybe just don't know how to) fancy editing in VS Code like "cut from here to the end of the line and then paste it half way into the line above", things which I can do easily in emacs).

[William Stein]

Patrix: about $600. We also have a (now popular at some places) option where students just directly pay us a 1-time $14 fee.

[Kevin Buzzard]

Now I need to find how to get my university to pay enough money so that my 40 students that will be using Lean during spring can use that instead of trying to install Lean at home

Patrick, my experience is that anything which looks remotely like it is an innovative new teaching method is something which my university is prepared to throw three-digit sums at no problem (indeed they threw a 5-digit sum at me). Hopefully it will work the same at your end.

[William Stein]

If I were to clone another lean package in a subdirectory and leanpkg build it and then edit its files, would the editor pick up the correct lean path? [...] I wonder whether it is also ready for more general use.

At present I do absolutely nothing to touch any paths and LEAN_PATH is not set. There is a lean server process and yesterday I made sure it gets started in $HOME, so ~/.lean gets picked up and can impact the lean search path.

If you just kill the lean server (with kill in a terminal), then things are currently in a broken state, and your only recourse is to restart the project (which takes 5-20 seconds), by clicking "Restart Project" in project settings. I'll add automatically starting the lean server if it is killed to my todo list.

[Reid Barton]

out.png is an autocompletion menu

[William Stein]

I guess I will just try it unless you tell me it's a bad idea/definitely won't work

I have no idea -- just go for it, possibly restart the project, and report back. If you want to make another new project to play with, send me a link and I'll upgrade it with network access.

[Reid Barton]

@Kevin Buzzard if you want a more representative sample then you could seek randomly through https://www.twitch.tv/videos/308713302 (there might be some dead time at the start while I get things all set up)

[Reid Barton]

I started a build of lean-category-theory but from your description I expect that while the build will succeed, if I try opening a file in lean-category-theory, it will use the same global lean server process which won't know about the lean-category-theory source paths or its dependencies.
I looked into how the emacs mode knows how to invoke the lean server.
It maintains a list of running lean server sessions each of which is associated to a leanpkg.path file.
For each buffer, it runs lean -p (with working directory the directory containing the buffer's file, I guess) and extracts the "leanpkg_path_file" field from the JSON output. (It also offers to run leanpkg configure if appropriate, which is nice but hardly critical.)
Then if it doesn't already have a session with the correct leanpkg.path file, it starts a new server.
All of this happens from https://github.com/leanprover/lean-mode/blob/master/lean-server.el#L360

[Reid Barton]

@William Stein :up: in case you want to support multiple Lean projects per CoCalc project.

[William Stein]

Thanks -- I've copied this to another todo item at lean.tasks

[William Stein]

I redid tab completion so now:
- there's an indicator about whether the completion is from the lean kernel or the frontend syntax mode
- the syntax ones come first, then the lean kernel ones
- I do NOT sort the lean kernel ones at all - the order is precisely what lean produces.
- the type information is now displayed to the right.

Screenshot-2018-09-13-at-2.40.01-PM.png

[Johan Commelin]

This is so cool! Once again, thanks for the effort you're putting into this.

[Johan Commelin]

@William Stein Here another small feature request: when there are multiple goals, I think they are separated by a blank line. Could you separate them with something like an <hr/>?

[Johan Commelin]

Hmmm, I just realised this isn't even done in VScode. However VScode highlights the turnstile (|-) symbols. Apparently my eyes thought that was really helpful :smiley:

[Patrick Massot]

Oh yes, colorized tactic state and messages is great, and very easy to port from the vscode extension. Have a look at https://github.com/leanprover/vscode-lean/blob/master/src/infoview.ts#L326 Note especially how it calls https://github.com/leanprover/vscode-lean/blob/master/src/infoview.ts#L355 which is very naive yet very useful

[William Stein]

Yes, @Patrick Massot, I've added colorized tactic state to the todo list.

[Johan Commelin]

I just had a multiplayer Lean/CoCalc session with @Reid Barton. Voice chat enabled. Really cool. We made quite some progress on the tfae tactic!

[Kevin Buzzard]

There's multiplayer voice chat??

[Johan Commelin]

There is a little :video_recorder: icon in the top-right.

[Kevin Buzzard]

I thought cocalc was basically for profs to distribute homework for students to do in sage. Looks like it has moved on a lot since I last looked seriously...

[William Stein]

@Johan Commelin -- AWESOME! @Kevin Buzzard it's a bit more than just "sagemath cloud" now. The video chat is hosted by appear.in -- it basically creates an ephemeral video chat room associated to any file (with the room name a big hash of the project_id and filename and a shared secret).

[William Stein]

Does tfae mean "the following are equivalent"

[Johan Commelin]

Yes it does.

[Johan Commelin]

The idea is that you feed it a list of propositions, and then a graph of implications.

[Johan Commelin]

What you get out of this is a function that you feed to natural numbers, and it will spit out the equivalence between those two propositions.

[Johan Commelin]

@William Stein I did get some banner on top of the appear.in chatroom, saying that the free chatrooms would no longer be available after the 24th of this month.

[William Stein]

@Johan Commelin -- crap, that's really unfortunate. We will have to remove this functionality, or try to find another provider (e.g., google?) that still makes random video chat available. Their pricing last I checked for non free was ridiculously high, much higher than we charge for cocalc, so paying them wasn't an option.

[Johan Commelin]

Yeah, I'm sorry. But I thought you'dd like to know this before it suddenly happened.

[William Stein]

OK, I've made an issue for this: https://github.com/sagemathinc/cocalc/issues/3185

[Johan Commelin]

Hmm, maybe it wasn't that bad: https://blog.appear.in/2018-product-updates/claiming

[Johan Commelin]

@William Stein I didn't check it carefully, only made a mental note to tell you that there was some warning.

[Johan Commelin]

So it's not actually about free vs money, but somehow the room needs to have an owner.

[Harald Schilly]

So it's not actually about free vs money, but somehow the room needs to have an owner.

I think it's about "registered user" (even with a pseudonym) vs. completely anonymous. The dialog to claim a room clearly states that it is free.

[Johan Commelin]

Right... sorry for the confusion.

[Harald Schilly]

no problem, this is still something introducing friction and good to be aware of that

[William Stein]

Another change I didn't mention: if you kill the lean server process in a terminal, it will now automatically start again. This could be relevant for packages (I don't know), and certainly means things should be a little more robust.

[Johan Commelin]

Here is a way to grind CoCalc to a halt: choose your favorite 1000-line file (e.g. data/polynomial.lean) from mathlib and upload it to CoCalc. Once you open it in the Lean IDE the website turns into a unit test for the halting problem.

[William Stein]

Do you have any idea why? Is it the browser frontend that gets slow or the lean server running on the backend?

[William Stein]

Oh booth are at 100% -- it might just be the overhead of rendering all the gutter markers to show progress.

[William Stein]

Incidentally if you see this and try to refresh the page and have the file opened again... change ?session=default to ?session=default2 and load cocalc to get a new session. For what it is worth, I opened data/polynomial.lean and the lean server ran at 100% for a while and my browser frontend was slow... but after about 30s everything was fine with lots of errors on the side (as expected due to missing imports). So this doesn't seem to be a "halting problem" sort of problem? (At least if you meant "infinite loop" or something like that.) Screenshot-2018-09-15-at-9.04.46-AM.png

[William Stein]

In any case, right now my goal is that this is just good enough for @Kevin Buzzard 's class...

[William Stein]

In any case, I think the root cause is inefficiency in constructing the hover tips on the left; I'll make a note to optimize that!

[Kevin Buzzard]

I should work on this more -- I would like to get "example sheet 0" up and running.

[Kevin Buzzard]

William -- I have say 20 .lean files each of which is very short, and is just the statement of a theorem in Lean.

[William Stein]

Yep - if your class examples/homework are way too slow, I want to know about it!

[Kevin Buzzard]

The students' job is to take each of these files and to add a proof of the theorem to it

[Kevin Buzzard]

How do I go about getting that system into CoCalc?

[Kevin Buzzard]

I am making a database of problems.

[Kevin Buzzard]

It's currently quite simple -- each entry is an identification number (say 0008), a lean file Q0008.lean with the theorem, a lean file S0008.lean with the proof, and TeX files of the theorem and the proof in maths, plus an additional "more information" file containing comments such as how difficult the question is to do in maths and in Lean

[William Stein]

1. Some ways to get the files into cocalc:
- make a tarball or whatever, and drag and drop them to the files listing
- click the "Upload" button in the upper right in the files listing
- click +New, then click on the big Upload box near the bottom
- setup ssh access to your project in Project Settings, then use scp or rsync.
- put the .lean files on github, then git clone them into cocalc.
2. Make sure to look at https://tutorial.cocalc.com/ in case you want to use any of our course management functionality to simplify distribution to/from students.

[Kevin Buzzard]

Some of the maths questions are not appropriate for Lean, for various technical reasons which I won't bore you with. Of those questions, the vast majority are well suited for Sage -- perhaps because the question is actually just a computation. For those database entries I could maybe add a sage file.

[Kevin Buzzard]

Ideally I'd like to set homework to the students of the form "For homework, do the following questions in the database : 0027, 0038, 0039, 0040."

[Kevin Buzzard]

I think it would be a much better way of managing my course in general.

[William Stein]

For sage code your options include:
- a .sage file; we do fully supported editing .sage files and running sage (in a terminal, say) in cocalc.
- a .sagews file -- that's a "sage worksheet", which is much like the old "sage notebooks".
- a Jupyter notebook -- i.e., a .ipynb file with a specific choice of Sage kernel. These are extremely popular also outside of math these days and are well supported both in CoCalc and in many other places.

[Kevin Buzzard]

Oh crazy. What are my options for Lean?

[Kevin Buzzard]

I have heard lots of talk about Jupyter notebooks but because I'm so used to the command line and emacs I've always steered clear of notebooks. I could never quite work out what they had to offer me.

[William Stein]

For lean, right now it is only -- "make a .lean file".

I can definitely see how it would make sense to have something like a LEAN Jupyter notebook, where each notebook cell is pretty much exactly like a .lean file is now in cocalc... But I have no implemented that (yet).

[Kevin Buzzard]

But they might be super-powerful these days.

[William Stein]

They're not really so much super powerful. I would describe them more as very beginner friendly... in certain ways (and less in others). In CoCalc they are especially nice because of the TimeTravel button, which means you can see all past states of the notebook.

[William Stein]

They are like a command line repl, but you can go back and change something from before, and confuse yourself even more :-). But overall, if you're careful, it is really useful for certain types of tasks. For example, my Ph.D. student and I were computeing J_0(42)(QQ)_tor exactly in this Jupyter notebook recently: Screenshot-2018-09-15-at-9.19.13-AM.png

[William Stein]

It's like a command line terminal session, but where you can clean it up and keep it around, and easily run it again.
tutorial

[Jeremy Avigad]

@William Stein could you add me as a collaborator? I'll be teaching a (probably small) Lean-based course at Carnegie Mellon next semester, and it would be great to do it with CoCalc.

[Scott Morrison]

@Jeremy Avigad, I just sent you an invite to the LEAN project on CoCalc.

[Jeremy Avigad]

I'm in! Thanks very much.

[William Stein]

Video chat: After some investigation and back and forth with appear.in support, I have switched from appear.in to https://jitsi.org/ for our CoCalc video chat. jitsi.org is completely free and open source, and works very well.

[Johan Commelin]

Thanks for the update!

[Gihan Marasingha]

@William Stein It's taken a while with the finance dept., but I've now got my CoCalc subscription going for my introductory pure maths course, which begins on Monday. I'd like to do something like the Mathematics in Lean book, which does some clever things to present HTML lecture notes within VS Code. They are interactive in the sense that clicking on the Lean snippets in the lecture notes brings up a Lean editor.

Is the same thing possible in CoCalc? @Bryan Gin-ge Chen @Jeremy Avigad - do you know how / if this might work?

Thanks!

[Bryan Gin-ge Chen]

Is there a special URL that can be used to open a snippet in the Lean editor in CoCalc? If so, then you could clone the Mathematics in Lean repo, replace the chapters with your lecture notes, and then replace the URL here with something appropriate for CoCalc.

[William Stein]

there a special URL that can be used to open a snippet in the Lean editor in CoCalc?

Unfortunately there isn't, though there was a very similar feature request a few days ago (https://github.com/sagemathinc/cocalc/issues/4851).

They are interactive in the sense that clicking on the Lean snippets in the lecture notes brings up a Lean editor.

You could use HTML (or Markdown) for your notes, and also pre-create a bunch of files with the corresponding lean code. The student would get a copy of all of this content and have it in their cocalc project (this is easy to accomplish with the Library, or a handout). Next to each block of code, put a relative link to the corresponding .lean file. When the student clicks the link, the corresponding lean file will open in a tab next to the book. Maybe that is sufficient for your needs?

If the above is unclear, let me know.

[Jennifer Balakrishnan]

@William Stein We were experimenting with Lean on CoCalc for my graduate topics class last week (and will be continuing over the next two weeks). We applied upgrades, but @Alex J. Best noticed that we were capped at 1 GB RAM by Lean. Is there a way to modify this on CoCalc?

[Kevin Buzzard]

@Gihan Marasingha you've been using CoCalc with your students at Exeter, right? Did you run into this issue?

[Gihan Marasingha]

I haven't run into a memory issue or maybe I have and I haven't realised it.

[Gihan Marasingha]

Oh and I didn't see the comments (in September!) about doing something like Maths in Lean in CoCalc. That's good to know and I might try that for next term.

[Gihan Marasingha]

The main issue I had was that most of my (~270) first-year students really didn't want to have anything to do with Lean. However, now they're 9 weeks in to the term, some of them are beginning to realise how useful Lean is and that (perhaps) their aversion to Lean was really a disguised aversion to proof.

[Ruben Van de Velde]

To be fair, proving things instead of just thinking you've proved things (but leaving holes you could drive a truck through) is really annoying when you start out :smiley:

[William Stein]

Jennifer Balakrishnan said:

William Stein We were experimenting with Lean on CoCalc for my graduate topics class last week (and will be continuing over the next two weeks). We applied upgrades, but Alex J. Best noticed that we were capped at 1 GB RAM by Lean. Is there a way to modify this on CoCalc?

1. How do you know you're capped at 1GB RAM in each LEAN process?

2. Maybe setting this environment variable would help: NODE_OPTIONS=--max-old-space-size=8192 ? The code that spawns the lean process is here; it's completely undocumented, but there is hope that maybe setting that environment variable would change how node runs... The way to set an environment variable for a cocalc project is to set a JSON object in the "Custom environment variables" section of Project settings, then restart the project. Probably the JSON is {"NODE_OPTIONS":"--max-old-space-size=8192"} in this case. I didn't try this, since I don't know 1.

[Alex J. Best]

@William Stein

1. It was just an empirical observation that we were getting out of memory errors but the lean process in the info panel always showed at most 1gb. I have now checked and 1gb is the limit set by lean internally at build time https://github.com/leanprover-community/lean/blob/d9997024f55dc756d47e2cacd12e8091ae37c9bf/src/shell/lean.cpp#L168 in the Lean VScode extension this is overridden by default to 4gb when starting the server.
2. It looks like https://github.com/sagemathinc/cocalc/blob/e341ad577db9486b834b10d745ad52d743e2cf3c/src/smc-project/lean/lean.ts#L73 is whats spawning the server, so changing this line to ['-M 4096'] would replicate the default vscode behavior, seeing as the default cocalc memory is only 1gb it might make more sense to set this up instead as an option in cocalc somewhere projectwise? Either a memory setting or a lean extra command line arguments setting? Sorry I don't know enough about typescript/cocalc to make a PR myself!

[Jennifer Balakrishnan]

Thanks @William Stein. I tried setting the environment variable as you suggested, but unfortunately it looks like we're still locked in at 1 GB (eyeballing one lean file, it seems to get through about 70 lines, after which it reports "excessive memory consumption" and halts).

[William Stein]

If you restart your project it will now have the -M 4096 option that @Alex J. Best suggests above.

[William Stein]

I've decided to just make it the default, since vscode does.

[Alex J. Best]

Great, thank you @William Stein !

[Jennifer Balakrishnan]

Awesome! Thank you @William Stein !!

[Floris van Doorn]

I'm helping someone to set up Lean in CoCalc. Is there a way to get a new version of mathlib in CoCalc as a user (the default seems to be 3.11.0)? After trying leanproject new ... and creating a new file in that project it seems that CoCalc is reading the wrong leanpkg.toml. Can you move the toml file to get the latest version of Lean as a user?

[Kevin Buzzard]

@Gihan Marasingha might be a good person to ask. My memory is that if you want to use all the infrastructure which cocalc has, which you do, then you're stuck with Lean 3.11.0. The only leanpkg.toml ever read is the one in the root directory.

[Kevin Buzzard]

The CoCalc people say that they simply cannot keep up with the constant changing of core Lean using their infrastructure.

[Rob Lewis]

@Floris van Doorn AFAIK CoCalc has a fixed Lean executable, it doesn't use elan. I think you should be able to point it to a different mathlib version with leanpkg.toml, but it will have to be compatible with that Lean version.

[Floris van Doorn]

Ok, thanks!

[Vijay Sharma]

Hello, I was trying to run lean on Cacalc and I followed the steps here: https://github.com/kbuzzard/xena/blob/master/CoCalc/CoCalc_notes.md but whenever I open the .lean file in Cocalc it throws the error that: LEAN_PATH is not found. Any ideas how can I fix it?

[Kevin Buzzard]

Those notes are really old. The version of lean on cocalc is old and he t won't handle modern mathlib. Because of this i have kind of got frustrated with lean in cocalc, but I know @Gihan Marasingha uses it and maybe he knows some more recent instructions. If you just want to use it yourself then you just put lean files in the root directory of your project and it works fine. I think that at that time I was trying to figure out how to get a different mathlib to the default cocalc one, but now there is no point doing this because the default cocalc mathlib is the most recent version of mathlib which works with the version of lean on cocalc. When I wrote those instructions this issue was not there.

[Gihan Marasingha]

Only just saw this @Vijay Sharma . What Kevin says is correct AFAIK. Cocalc isn't designed for use with LEAN projects per se. If you have any more questions, please give me a shout.

[Vijay Sharma]

@Gihan Marasingha I too just saw your message now. Indeed I am super keen to setup lean on CoCalc. If you are available sometime would be possible to have a short call?

[Gihan Marasingha]

@Vijay Sharma Absolutely. I'm in the GMT + 1 time zone at the moment (in England). Currently, I'm free all day on 3 May. What time is good for you?

[Vijay Sharma]

@Gihan Marasingha Thank you so much. Today is also possible. Say your time 1630hrs?

[Johan Commelin]

@Vijay Sharma A cool thing about Zulip: if you type <time and hit [Enter] then you'll get a dialog to select a time in your timezone. But it will be printed in a timezone aware format, so everyone sees it in the local time (of their computer).

[Johan Commelin]

Example: 2021-05-03T10:50:00+02:00 prints as Mon, May 3 2021, 10:50 for me.

[Gihan Marasingha]

@Vijay Sharma That works for me. I'll send you a message to set up a meeting.

[Vijay Sharma]

Hey Gihan, my email address is vijay@riyaaz.org