Zulip Chat Archive

Stream: general

Topic: CoCalc


view this post on Zulip Patrick Massot (May 03 2018 at 19:42):

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

view this post on Zulip Johan Commelin (May 03 2018 at 19:51):

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

view this post on Zulip Johan Commelin (May 03 2018 at 19:51):

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

view this post on Zulip Johan Commelin (May 03 2018 at 19:51):

I am really excited about this!

view this post on Zulip Kevin Buzzard (May 03 2018 at 22:02):

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.

view this post on Zulip Kevin Buzzard (May 03 2018 at 22:03):

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...

view this post on Zulip Kevin Buzzard (May 03 2018 at 22:04):

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

view this post on Zulip William Stein (May 03 2018 at 22:28):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 22:35):

Hiya.

view this post on Zulip Kevin Buzzard (May 03 2018 at 22:36):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 22:36):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 22:37):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 22:38):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 22:38):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 22:38):

and I'm going to go and do some schemes

view this post on Zulip Andrew Ashworth (May 04 2018 at 00:53):

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

view this post on Zulip Patrick Massot (Aug 31 2018 at 11:31):

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

view this post on Zulip Kevin Buzzard (Aug 31 2018 at 12:32):

I can use Lean in CoCalc :-)

view this post on Zulip Kevin Buzzard (Aug 31 2018 at 12:32):

As of today

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:29):

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

view this post on Zulip Kevin Buzzard (Aug 31 2018 at 14:32):

Yes

view this post on Zulip Kevin Buzzard (Aug 31 2018 at 14:32):

Shall I live stream on twitch?

view this post on Zulip Johan Commelin (Aug 31 2018 at 14:36):

You shall!

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:36):

Yeah!

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 14:38):

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.

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:39):

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

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 14:40):

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

view this post on Zulip Patrick Massot (Aug 31 2018 at 14:54):

synchronisation is completely random :(

view this post on Zulip Johan Commelin (Aug 31 2018 at 14:55):

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

view this post on Zulip Johan Commelin (Aug 31 2018 at 14:56):

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

view this post on Zulip Patrick Massot (Aug 31 2018 at 15:01):

what is the email address associates to your account?

view this post on Zulip Johan Commelin (Aug 31 2018 at 15:50):

johan@commelin.net I think

view this post on Zulip Patrick Massot (Aug 31 2018 at 15:52):

You should receive an email

view this post on Zulip Patrick Massot (Aug 31 2018 at 15:53):

But it's hopelessly slow

view this post on Zulip Johan Commelin (Aug 31 2018 at 15:54):

Ok, you are also on an unpaid account?

view this post on Zulip Patrick Massot (Aug 31 2018 at 15:54):

Using Lean on CoCalc without paying doesn't seem possible

view this post on Zulip Patrick Massot (Aug 31 2018 at 15:54):

Yes

view this post on Zulip Johan Commelin (Aug 31 2018 at 15:54):

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

view this post on Zulip Johan Commelin (Aug 31 2018 at 15:56):

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

view this post on Zulip William Stein (Aug 31 2018 at 17:45):

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

view this post on Zulip William Stein (Aug 31 2018 at 17:45):

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

view this post on Zulip William Stein (Aug 31 2018 at 17:45):

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

view this post on Zulip Patrick Massot (Aug 31 2018 at 18:05):

Thanks!

view this post on Zulip William Stein (Aug 31 2018 at 18:15):

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

view this post on Zulip Patrick Massot (Aug 31 2018 at 18:16):

eheh, that's the lemma I just wrote

view this post on Zulip William Stein (Aug 31 2018 at 18:16):

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

view this post on Zulip Patrick Massot (Aug 31 2018 at 18:18):

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

view this post on Zulip Gabriel Ebner (Aug 31 2018 at 18:20):

@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

view this post on Zulip William Stein (Aug 31 2018 at 18:21):

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

view this post on Zulip William Stein (Aug 31 2018 at 18:26):

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...

view this post on Zulip Patrick Massot (Aug 31 2018 at 18:31):

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

view this post on Zulip Patrick Massot (Aug 31 2018 at 18:31):

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

view this post on Zulip Kevin Buzzard (Aug 31 2018 at 19:09):

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

view this post on Zulip Johan Commelin (Aug 31 2018 at 20:01):

This is awesome! Thank you very much!

view this post on Zulip Johan Commelin (Aug 31 2018 at 20:02):

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

view this post on Zulip Johan Commelin (Aug 31 2018 at 20:02):

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

view this post on Zulip Scott Morrison (Sep 01 2018 at 01:05):

Could someone add me as a collaborator on that project?

view this post on Zulip Patrick Massot (Sep 01 2018 at 08:14):

I hope I just did that

view this post on Zulip Patrick Massot (Sep 01 2018 at 08:15):

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

view this post on Zulip Kevin Buzzard (Sep 01 2018 at 08:55):

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.

view this post on Zulip William Stein (Sep 05 2018 at 04:34):

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

view this post on Zulip Johan Commelin (Sep 05 2018 at 04:37):

Hooray! That's really nice.

view this post on Zulip Scott Morrison (Sep 05 2018 at 04:43):

This looks really promising!

view this post on Zulip Scott Morrison (Sep 05 2018 at 04:44):

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.

view this post on Zulip Johan Commelin (Sep 05 2018 at 04:45):

It is on the todo list.

view this post on Zulip Kevin Buzzard (Sep 05 2018 at 07:38):

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").

view this post on Zulip Kevin Buzzard (Sep 06 2018 at 17:36):

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

view this post on Zulip Kevin Buzzard (Sep 06 2018 at 17:39):

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.

view this post on Zulip Harald Schilly (Sep 06 2018 at 18:25):

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.

view this post on Zulip Mario Carneiro (Sep 06 2018 at 18:26):

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

view this post on Zulip Mario Carneiro (Sep 06 2018 at 18:26):

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

view this post on Zulip Mario Carneiro (Sep 06 2018 at 18:28):

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

view this post on Zulip Mario Carneiro (Sep 06 2018 at 18:29):

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

view this post on Zulip Mario Carneiro (Sep 06 2018 at 18:30):

This is the way most users do it, I think

view this post on Zulip Sebastian Ullrich (Sep 06 2018 at 21:02):

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

view this post on Zulip Kenny Lau (Sep 11 2018 at 15:02):

how does this work?

view this post on Zulip Kevin Buzzard (Sep 11 2018 at 16:22):

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.

view this post on Zulip Kenny Lau (Sep 11 2018 at 16:26):

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

view this post on Zulip Kevin Buzzard (Sep 11 2018 at 16:27):

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

view this post on Zulip Kenny Lau (Sep 11 2018 at 16:33):

apparently only a few people have access

view this post on Zulip Johan Commelin (Sep 11 2018 at 16:38):

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

view this post on Zulip Johan Commelin (Sep 11 2018 at 16:38):

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

view this post on Zulip Harald Schilly (Sep 11 2018 at 19:36):

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:

view this post on Zulip Kevin Buzzard (Sep 11 2018 at 19:45):

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.

view this post on Zulip Kevin Buzzard (Sep 11 2018 at 19:46):

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).

view this post on Zulip Kevin Buzzard (Sep 11 2018 at 19:47):

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.

view this post on Zulip Chris Hughes (Sep 11 2018 at 20:07):

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.

view this post on Zulip Kevin Buzzard (Sep 11 2018 at 20:15):

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? ;-)

view this post on Zulip Johan Commelin (Sep 12 2018 at 03:02):

@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...

view this post on Zulip William Stein (Sep 12 2018 at 19:22):

@Harald Schilly is in Vienna, Austria.

view this post on Zulip William Stein (Sep 12 2018 at 19:22):

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

view this post on Zulip William Stein (Sep 12 2018 at 19:23):

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.

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:24):

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

view this post on Zulip William Stein (Sep 12 2018 at 19:24):

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

view this post on Zulip Kenny Lau (Sep 12 2018 at 19:24):

lol how do you know who I am

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:24):

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

view this post on Zulip William Stein (Sep 12 2018 at 19:25):

@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.

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:25):

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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:25):

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

view this post on Zulip Harald Schilly (Sep 12 2018 at 19:25):

@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.

view this post on Zulip William Stein (Sep 12 2018 at 19:26):

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

view this post on Zulip Kenny Lau (Sep 12 2018 at 19:26):

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

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

view this post on Zulip Kenny Lau (Sep 12 2018 at 19:26):

somehow WS managed to find my account

view this post on Zulip William Stein (Sep 12 2018 at 19:26):

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

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:26):

Isn't @Gabriel Ebner in Vienna?

view this post on Zulip William Stein (Sep 12 2018 at 19:26):

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

view this post on Zulip Harald Schilly (Sep 12 2018 at 19:27):

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

view this post on Zulip Kenny Lau (Sep 12 2018 at 19:27):

fair enough

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:27):

https://gebner.org/

view this post on Zulip Harald Schilly (Sep 12 2018 at 19:28):

nice

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:28):

I think he is currently on vacations

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:30):

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

view this post on Zulip William Stein (Sep 12 2018 at 19:30):

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

view this post on Zulip William Stein (Sep 12 2018 at 19:32):

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.

view this post on Zulip William Stein (Sep 12 2018 at 19:33):

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

view this post on Zulip William Stein (Sep 12 2018 at 19:39):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 19:40):

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

view this post on Zulip Sebastian Ullrich (Sep 12 2018 at 19:42):

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

view this post on Zulip Sebastian Ullrich (Sep 12 2018 at 19:44):

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

view this post on Zulip William Stein (Sep 12 2018 at 19:45):

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...

view this post on Zulip William Stein (Sep 12 2018 at 19:47):

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

view this post on Zulip William Stein (Sep 12 2018 at 19:47):

But what is lean's library folder?

view this post on Zulip William Stein (Sep 12 2018 at 19:47):

How do I determine that?

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:49):

it is lean/library

view this post on Zulip William Stein (Sep 12 2018 at 19:50):

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

view this post on Zulip William Stein (Sep 12 2018 at 19:52):

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

view this post on Zulip William Stein (Sep 12 2018 at 19:52):

Here's what I'm currently doing:

view this post on Zulip William Stein (Sep 12 2018 at 19:52):


view this post on Zulip William Stein (Sep 12 2018 at 19:52):

    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", ".", [])
    );

view this post on Zulip Chris Hughes (Sep 12 2018 at 19:54):

import data.finset is probably a reasonable test.

view this post on Zulip William Stein (Sep 12 2018 at 19:55):

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

file 'init' not found in the LEAN_PATH

view this post on Zulip Sebastian Ullrich (Sep 12 2018 at 19:56):

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

view this post on Zulip Sebastian Ullrich (Sep 12 2018 at 19:57):

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

view this post on Zulip William Stein (Sep 12 2018 at 19:57):

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

view this post on Zulip Sebastian Ullrich (Sep 12 2018 at 19:58):

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

view this post on Zulip William Stein (Sep 12 2018 at 20:00):

ok, that works perfectly.

view this post on Zulip William Stein (Sep 12 2018 at 20:19):

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/./."
  ]
}

view this post on Zulip William Stein (Sep 12 2018 at 20:30):

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?

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 20:31):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 20:31):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 20:32):

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

view this post on Zulip William Stein (Sep 12 2018 at 20:33):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 20:34):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 20:34):

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

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 20:35):

I'm afraid I'm afk right now though

view this post on Zulip Patrick Massot (Sep 12 2018 at 20:42):

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

view this post on Zulip William Stein (Sep 12 2018 at 20:44):

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.

view this post on Zulip Sebastian Ullrich (Sep 12 2018 at 21:16):

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

view this post on Zulip William Stein (Sep 12 2018 at 21:20):

@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.

view this post on Zulip Sebastian Ullrich (Sep 12 2018 at 21:26):

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

view this post on Zulip William Stein (Sep 12 2018 at 21:58):

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.

view this post on Zulip William Stein (Sep 12 2018 at 21:59):

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?

view this post on Zulip Sebastian Ullrich (Sep 12 2018 at 22:03):

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.

view this post on Zulip William Stein (Sep 12 2018 at 22:11):

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.

view this post on Zulip Gabriel Ebner (Sep 12 2018 at 23:55):

@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.

view this post on Zulip William Stein (Sep 13 2018 at 04:18):

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

view this post on Zulip William Stein (Sep 13 2018 at 04:22):

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.

view this post on Zulip Mario Carneiro (Sep 13 2018 at 04:32):

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

view this post on Zulip Harald Schilly (Sep 13 2018 at 12:57):

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...

view this post on Zulip Kenny Lau (Sep 13 2018 at 15:25):

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 15:25):

maybe we should all join a discord group

view this post on Zulip Kenny Lau (Sep 13 2018 at 15:25):

is that a good idea?

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 15:26):

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.

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 15:59):

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:

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 16:00):

vscode.png

cocalc1.png

cocalc2.png

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 16:04):

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!

view this post on Zulip Patrick Massot (Sep 13 2018 at 16:04):

Yes, the progress looks impressive

view this post on Zulip William Stein (Sep 13 2018 at 16:14):

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 ?

view this post on Zulip William Stein (Sep 13 2018 at 16:15):

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.

view this post on Zulip Mario Carneiro (Sep 13 2018 at 16:16):

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

view this post on Zulip Mario Carneiro (Sep 13 2018 at 16:17):

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

view this post on Zulip William Stein (Sep 13 2018 at 16:18):

@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.

view this post on Zulip Mario Carneiro (Sep 13 2018 at 16:19):

I think this is default vscode behavior

view this post on Zulip William Stein (Sep 13 2018 at 16:20):

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

view this post on Zulip Reid Barton (Sep 13 2018 at 16:21):

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

view this post on Zulip William Stein (Sep 13 2018 at 16:22):

@Reid Barton -- done.

view this post on Zulip William Stein (Sep 13 2018 at 16:22):

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".

view this post on Zulip William Stein (Sep 13 2018 at 16:25):

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

view this post on Zulip William Stein (Sep 13 2018 at 16:29):

@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!)

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 16:35):

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.

view this post on Zulip Patrick Massot (Sep 13 2018 at 16:37):

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

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 16:37):

game over

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 16:37):

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

view this post on Zulip William Stein (Sep 13 2018 at 16:38):

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.

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 16:38):

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

view this post on Zulip William Stein (Sep 13 2018 at 16:38):

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

view this post on Zulip William Stein (Sep 13 2018 at 16:39):

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.

view this post on Zulip William Stein (Sep 13 2018 at 16:39):

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

view this post on Zulip Patrick Massot (Sep 13 2018 at 16:39):

Thanks, I managed to get back my frames

view this post on Zulip Patrick Massot (Sep 13 2018 at 16:40):

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

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 16:40):

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.

view this post on Zulip Patrick Massot (Sep 13 2018 at 16:42):

This Lean in CoCalc is amazing

view this post on Zulip Reid Barton (Sep 13 2018 at 16:43):

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

view this post on Zulip Patrick Massot (Sep 13 2018 at 16:44):

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

view this post on Zulip Reid Barton (Sep 13 2018 at 16:45):

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.

view this post on Zulip Patrick Massot (Sep 13 2018 at 16:45):

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

view this post on Zulip William Stein (Sep 13 2018 at 16:46):

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.

view this post on Zulip Reid Barton (Sep 13 2018 at 16:47):

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

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 16:47):

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).

view this post on Zulip William Stein (Sep 13 2018 at 16:48):

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

view this post on Zulip Kevin Buzzard (Sep 13 2018 at 16:49):

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.

view this post on Zulip William Stein (Sep 13 2018 at 16:51):

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.

view this post on Zulip Reid Barton (Sep 13 2018 at 16:53):

out.png is an autocompletion menu

view this post on Zulip William Stein (Sep 13 2018 at 16:54):

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.

view this post on Zulip Reid Barton (Sep 13 2018 at 16:55):

@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)

view this post on Zulip Reid Barton (Sep 13 2018 at 17:25):

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

view this post on Zulip Reid Barton (Sep 13 2018 at 17:27):

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

view this post on Zulip William Stein (Sep 13 2018 at 18:59):

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

view this post on Zulip William Stein (Sep 13 2018 at 21:41):

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

view this post on Zulip Johan Commelin (Sep 14 2018 at 06:49):

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

view this post on Zulip Johan Commelin (Sep 14 2018 at 13:22):

@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/>?

view this post on Zulip Johan Commelin (Sep 14 2018 at 13:33):

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:

view this post on Zulip Patrick Massot (Sep 14 2018 at 13:40):

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

view this post on Zulip William Stein (Sep 14 2018 at 16:07):

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

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:18):

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!

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 16:19):

There's multiplayer voice chat??

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:20):

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

view this post on Zulip Kevin Buzzard (Sep 14 2018 at 16:20):

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...

view this post on Zulip William Stein (Sep 14 2018 at 16:24):

@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).

view this post on Zulip William Stein (Sep 14 2018 at 16:27):

Does tfae mean "the following are equivalent"

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:29):

Yes it does.

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:29):

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

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:30):

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.

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:31):

@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.

view this post on Zulip William Stein (Sep 14 2018 at 16:33):

@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.

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:34):

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

view this post on Zulip William Stein (Sep 14 2018 at 16:36):

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

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:39):

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

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:39):

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

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:40):

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

view this post on Zulip Harald Schilly (Sep 14 2018 at 16:44):

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.

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:45):

Right... sorry for the confusion.

view this post on Zulip Harald Schilly (Sep 14 2018 at 16:46):

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

view this post on Zulip William Stein (Sep 14 2018 at 17:15):

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.

view this post on Zulip Johan Commelin (Sep 15 2018 at 15:16):

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.

view this post on Zulip William Stein (Sep 15 2018 at 16:01):

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

view this post on Zulip William Stein (Sep 15 2018 at 16:02):

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

view this post on Zulip William Stein (Sep 15 2018 at 16:05):

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

view this post on Zulip William Stein (Sep 15 2018 at 16:05):

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

view this post on Zulip William Stein (Sep 15 2018 at 16:06):

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!

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:06):

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

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:08):

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

view this post on Zulip William Stein (Sep 15 2018 at 16:08):

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

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:08):

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

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:08):

How do I go about getting that system into CoCalc?

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:08):

I am making a database of problems.

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:10):

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

view this post on Zulip William Stein (Sep 15 2018 at 16:11):

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.

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:12):

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.

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:14):

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."

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:14):

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

view this post on Zulip William Stein (Sep 15 2018 at 16:14):

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.

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:15):

Oh crazy. What are my options for Lean?

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:16):

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.

view this post on Zulip William Stein (Sep 15 2018 at 16:16):

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).

view this post on Zulip Kevin Buzzard (Sep 15 2018 at 16:16):

But they might be super-powerful these days.

view this post on Zulip William Stein (Sep 15 2018 at 16:18):

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.

view this post on Zulip William Stein (Sep 15 2018 at 16:20):

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

view this post on Zulip William Stein (Sep 15 2018 at 16:21):

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

view this post on Zulip Jeremy Avigad (Sep 16 2018 at 01:05):

@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.

view this post on Zulip Scott Morrison (Sep 16 2018 at 01:06):

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

view this post on Zulip Jeremy Avigad (Sep 16 2018 at 01:09):

I'm in! Thanks very much.

view this post on Zulip William Stein (Oct 02 2018 at 14:25):

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.

view this post on Zulip Johan Commelin (Oct 02 2018 at 14:26):

Thanks for the update!

view this post on Zulip Gihan Marasingha (Sep 16 2020 at 23:45):

@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!

view this post on Zulip Bryan Gin-ge Chen (Sep 16 2020 at 23:50):

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.

view this post on Zulip William Stein (Sep 17 2020 at 04:30):

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.

view this post on Zulip Jennifer Balakrishnan (Nov 20 2020 at 20:44):

@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?

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 20:48):

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

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 20:52):

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

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 20:56):

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.

view this post on Zulip Gihan Marasingha (Nov 20 2020 at 20:58):

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.

view this post on Zulip Ruben Van de Velde (Nov 20 2020 at 21:00):

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:

view this post on Zulip William Stein (Nov 20 2020 at 21:14):

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.

view this post on Zulip Alex J. Best (Nov 21 2020 at 01:06):

@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!

view this post on Zulip Jennifer Balakrishnan (Nov 21 2020 at 02:54):

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).

view this post on Zulip William Stein (Nov 22 2020 at 04:48):

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

view this post on Zulip William Stein (Nov 22 2020 at 04:48):

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

view this post on Zulip Alex J. Best (Nov 22 2020 at 15:07):

Great, thank you @William Stein !

view this post on Zulip Jennifer Balakrishnan (Nov 22 2020 at 16:11):

Awesome! Thank you @William Stein !!

view this post on Zulip Floris van Doorn (Mar 05 2021 at 20:29):

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?

view this post on Zulip Kevin Buzzard (Mar 05 2021 at 23:14):

@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.

view this post on Zulip Kevin Buzzard (Mar 05 2021 at 23:15):

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

view this post on Zulip Rob Lewis (Mar 05 2021 at 23:16):

@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.

view this post on Zulip Floris van Doorn (Mar 06 2021 at 07:06):

Ok, thanks!

view this post on Zulip Vijay Sharma (Mar 30 2021 at 20:04):

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?

view this post on Zulip Kevin Buzzard (Mar 30 2021 at 21:02):

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.

view this post on Zulip Gihan Marasingha (Apr 16 2021 at 12:21):

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.

view this post on Zulip Vijay Sharma (Apr 29 2021 at 13:51):

@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?

view this post on Zulip Gihan Marasingha (Apr 29 2021 at 16:46):

@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?

view this post on Zulip Vijay Sharma (May 03 2021 at 08:27):

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

view this post on Zulip Johan Commelin (May 03 2021 at 08:50):

@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).

view this post on Zulip Johan Commelin (May 03 2021 at 08:51):

Example: prints as Mon, May 3 2021, 10:50 for me.

view this post on Zulip Gihan Marasingha (May 03 2021 at 10:42):

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

view this post on Zulip Vijay Sharma (May 03 2021 at 10:59):

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


Last updated: May 16 2021 at 05:21 UTC