Zulip Chat Archive

Stream: general

Topic: Lean homework in CoCalc

Kevin Buzzard (Nov 29 2018 at 10:42):

Here are my notes on setting Lean homework in CoCalc:


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 (Nov 29 2018 at 10:56):

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 (Nov 29 2018 at 14:48):

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 (Nov 29 2018 at 21:13):

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 (Feb 12 2019 at 00:55):

@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 (Feb 12 2019 at 07:11):

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 (Feb 12 2019 at 07:28):

I've asked nicely.

Johan Commelin (Feb 12 2019 at 07:31):

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 (Feb 12 2019 at 07:32):

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

Kevin Buzzard (Feb 12 2019 at 08:08):

Cocalc sessions are not internet enabled by default

Kevin Buzzard (Feb 12 2019 at 08:09):

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 (Feb 12 2019 at 08:09):

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.

Last updated: Dec 20 2023 at 11:08 UTC