Lean homework in CoCalc

Stream: general

[Kevin Buzzard]

Here are my notes on setting Lean homework in CoCalc:

https://github.com/kbuzzard/xena/blob/master/CoCalc/CoCalc_notes.md

That link will be updated as people tell me better ways of getting round a kludgy hack with paths. Rather than go into details here, I will just hope that someone tells me a better way of doing it and then I'll update the link above. [The current issue is that when a student clicks on a .lean file CoCalc looks for leanpkg.path in their home directory, which my homework cannot access. @William Stein any ideas on how to make this less hacky?]

@Patrick Massot @Jeremy Avigad I've got it working, and am optimistic that it will be working even better soon. Jeremy, you might well be happy with CoCalc's installation of mathlib which is at path /ext/lean/lean-3.4.1-linux/mathlib/, but I am greedy and want both bleeding edge mathlib and also a library of my own, which is why I had to work harder.

[Rob Lewis]

Thanks for the info, Kevin. I'm going to look into using CoCalc for my course in April. Just to check -- are you using the standard or basic course plan? As an instructor, do you have write access to a subdirectory of students' home folders?

[Kevin Buzzard]

I bought 4 months of Standard Medium Course (70 people). I am running an unconventional course in an unconventional way -- I have 250 students, but Lean is just an optional extra, so I did not need 250 people.

[Kevin Buzzard]

So today I used the "shared project" functionality of CoCalc and we had multiple people working on one lean file. I thought it would be chaos but it worked fine, and was very funny. What happened was that completely coincidentally I found two groups of people independently trying to define dihedral groups in Lean, and because I'd spent several hours earlier today thinking about CoCalc I suggested that we tried to do it together. This was slightly brave on my part because I had not thought at all about how imports worked for group projects, and initially there was some confusion about which version of mathlib we needed. I hacked together a solution though, and it worked really smoothly. I guess I should add a description of how it all worked to my notes.

[Patrick Massot]

@Kevin Buzzard do you have any update to https://github.com/kbuzzard/xena/blob/master/CoCalc/CoCalc_notes.md? Do you think we could easily get CoCalc to upgrade to Lean 3.4.2? I hope I'll be able to start using Lean in CoCalc with my students this week

[Kevin Buzzard]

Oh! I'd forgotten about that. I could ask William. I know he told me that they would only consider upgrading once every 6 months or so, but it has been six months...

[Kevin Buzzard]

I've asked nicely.

[Johan Commelin]

Your CoCalc projects have got an internet connection, right? Can't you just ask William to install elan? Then you'll get the right Lean automatically?

[Johan Commelin]

Or maybe if you have elan then it doesn't yet play nicely with their own Lean web editor?

[Kevin Buzzard]

Cocalc sessions are not internet enabled by default

[Kevin Buzzard]

And I know from experience (running random old projects on the tube) that if you don't have an internet connection then elan just breaks

[Johan Commelin]

I know, so it would be nice to have both options. The updated-twice-a-year-lean and the hottest-and-newest-elan-enabled-lean. If you pay for internet, the second option works. Otherwise, fallback to the first option.