class on itp

Stream: general

[Jeremy Avigad]

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]

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

[Patrick Massot]

the proof is also cut actually

[Bryan Gin-ge Chen]

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]

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

[Patrick Massot]

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

[Bryan Gin-ge Chen]

Oh I guess the right hand side is cut off

[Jeremy Avigad]

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]

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

[Patrick Massot]

I would either make it clearly unreadable or actually readable

[Patrick Massot]

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

[Jeremy Avigad]

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]

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]

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]

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]

I like it!

[Scott Morrison]

Are there going to be any recordings? :-)

[Jeremy Avigad]

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

[Scott Morrison]

(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]

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

[Kevin Buzzard]

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

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.