Zulip Chat Archive

Stream: general

Topic: class on itp

Jeremy Avigad (Oct 14 2018 at 14:42):

Hey, check out the flyer I made up for an Interactive Theorem Proving class I am teaching next semester: http://www.andrew.cmu.edu/user/avigad/itp/. Comments are welcome. The course schedule goes live next week and I'll circulate it then.
@Kevin Buzzard How is your experience with CoCalc? Is there anything I should know?

Patrick Massot (Oct 14 2018 at 15:05):

The Zorn screenshot is almost readable but not quite, because the first line is cut off

Patrick Massot (Oct 14 2018 at 15:07):

the proof is also cut actually

Bryan Gin-ge Chen (Oct 14 2018 at 15:08):

What browser are you using? I see this in both firefox and chrome, which looks fine to me: Screenshot-2018-10-14-11.07.12.png

Patrick Massot (Oct 14 2018 at 15:08):

I'd love to attend the end of this course...

Patrick Massot (Oct 14 2018 at 15:08):

I see the same, and it's certainly not fine

Bryan Gin-ge Chen (Oct 14 2018 at 15:08):

Oh I guess the right hand side is cut off

Jeremy Avigad (Oct 14 2018 at 15:08):

It's not really meant to be readable. I just wanted to make an impressionistic suggestion that the course has something to do with something that looks like computer code. Is it really worth the effort to do better?

Patrick Massot (Oct 14 2018 at 15:09):

You just saw it with Bryan: the trouble is it looks like it will be readable

Patrick Massot (Oct 14 2018 at 15:09):

I would either make it clearly unreadable or actually readable

Patrick Massot (Oct 14 2018 at 15:09):

Of course I write this only because you asked for comments, it's not a big problem

Jeremy Avigad (Oct 14 2018 at 15:22):

Thanks. I just tried making a sharper, more readable version, but it is too prominent: it doesn't look good. zorn2.png
I'll try blurring the image.

Jeremy Avigad (Oct 14 2018 at 15:32):

I just spent a few minutes playing with Gimp's blurring and distortion features, but I didn't like any of the results. I'll leave it the way it is.

Reid Barton (Oct 14 2018 at 16:02):

I also had the same reaction regarding the top image. To clarify, the only issue is the top line and the line endingtrans are cut off. Otherwise the existing image is great.

Jeremy Avigad (Oct 14 2018 at 16:27):

O.k., how about this one? http://www.andrew.cmu.edu/user/avigad/itp/
The old one: http://www.andrew.cmu.edu/user/avigad/itp/index_old.html

Scott Morrison (Oct 14 2018 at 16:29):

I like it!

Scott Morrison (Oct 14 2018 at 16:29):

Are there going to be any recordings? :-)

Jeremy Avigad (Oct 14 2018 at 16:38):

Hmm... I wasn't planning on it, but I'll think about it.

Scott Morrison (Oct 14 2018 at 17:03):

(Perhaps just ask for a student volunteer; I've had great success with students recording on their phone, and just sending me the youtube links afterwards.)

Simon Hudon (Oct 14 2018 at 19:03):

I'm happy to see a reference to software / hardware verification :)

Kevin Buzzard (Oct 14 2018 at 19:59):

@Jeremy Avigad my experience with CoCalc is: first, you have to pay to get a reliable service. Second, there is one thing which in my mind might not go as smoothly as one might hope. I don't know if this situation will apply to you. The homeworks I want to give out are lean files which rely on two dependencies: firstly mathlib, and secondly a (very) small library of my own. I decided I would make a github repo for the homework (and put my library in /src). But it seems crazy to actually make the contents _target/deps/mathlib be part of the homework I set, because then everyone would get a new mathlib for every homework. This might be one way of doing it. But there's a mathlib installed on CoCalc, so one way of doing it would be to hack together an appropriate leanpkg.path which is CoCalc-specific. Unfortunately I have not had the time to think about this problem, because our ICT guys actually made Lean really easy to use on our local machines this year (the students click on VS Code and it opens a Lean project, the extension is installed, the path to Lean is correct -- it just works straight out of the box) so most people have been using Lean on our local machines. It's high priority to make all this work really smoothly on CoCalc but I have not ironed out these details yet. @William Stein I plan to work on this at some point but this is a summary of where I am now. I am not running a course -- everything is completely informal with me, and students are still learning the basics, so I have not had to think too hard about this yet. But within a week or so I will have to engage with this issue.

Jeremy Avigad (Oct 15 2018 at 01:27):

Thanks, @Simon Hudon. I know enough to point students to Chlipala's CPDT and FRAP, and Nipkow and Klein's Concrete Semantics. Porting anything from those to Lean is a reasonable project. If I have any students that are looking for something more creative, I'll send them to you.
And thanks, @Kevin Buzzard. This is helpful. I have got until January to figure it out, so I'll likely come back with more specific questions later.

Last updated: Aug 03 2023 at 10:10 UTC