New edition of the Hitchhiker's Guide based on 3.20.0c

Stream: general

[Jasmin Blanchette]

I am proud to announce a new edition of The Hitchhiker's Guide to Logical Verification based on Lean 3.20.0c and a recent mathlib. Two PDFs are available: standard (A4) and optimized for tablets and ebook readers (A5).

The version of mathlib we use is slighly nonstandard (w.r.t. to @Jannis Limperg's induction' and cases' tactics), but the PRs are underway, and it's not too hard to get used to induction and cases after having learned with the more novice-friendly primed versions.

[Rob Lewis]

Jasmin Blanchette said:

optimized for tablets and ebook readers (A5).

Nice formatting. Makes me wish I had a tablet ;)

[Jasmin Blanchette]

Or an e-reader. An earlier version looks roughly like this:
IMG_20200825_182203.jpg

[Jasmin Blanchette]

Now that we have a tablet version, @Johan Commelin is no longer going to call me a "dinosaur from the last century". :smiley:

[Johan Commelin]

@Jasmin Blanchette :rofl: touché
I'm really happy with all the energy you've been investing in this resource! I'm hoping I will be teaching a Lean course next summer, and I think this will be one of the two texts, next to MiL.

[Jasmin Blanchette]

I'm extremely pleased a text that explicitly says it's not a Lean tutorial (in the preface) and that it's aimed at computer scientist has found a place in the Lean community. This was actually very unexpected to me. ;)

[Jasmin Blanchette]

Let me know if you find anything that could be improved.

[Kevin Lacker]

Reading through it, I like the cheat sheet for Lean's special symbols ;-) Is that available anywhere else on the web?

[Marc Huisinga]

Kevin Lacker said:

Reading through it, I like the cheat sheet for Lean's special symbols ;-) Is that available anywhere else on the web?

https://github.com/leanprover/vscode-lean/blob/master/translations.json

[Bryan Gin-ge Chen]

The emacs version is here. There are a few differences still, I think.

[Kevin Lacker]

one item of feedback around learning tactics from written material like a book - I think it really helps to tell people that you must be using an environment that shows you the current goals, like vscode or emacs, in order to write tactics-based proofs

[Jasmin Blanchette]

I'm curious. Which other environment would one use?

[Kevin Lacker]

it just depends on your students, I suppose - someone who's already done other computer science might have a preferred text editor, and start using one of those

[Kevin Lacker]

for emacs specifically, lean-mode doesn't open the goal buffer by default, you have to do it explicitly

[Kevin Lacker]

https://insights.stackoverflow.com/survey/2019#technology-_-most-popular-development-environments is the best data i could find on this... about 55% of developers are using emacs or vscode which are the environments supported by lean. most people should switch to vscode for lean programming... if someone tries to just use their normal development environment they will find tactics impossible to use

[Jasmin Blanchette]

Ah I see. It never crossed my mind that these environments would work remotely well with Lean at all. Even with proof terms, you want to see the current goal (type). Anyway, the Hitchhiker's Guide does assume VS Code throughout.

[Kevin Lacker]

yeah, they don't work with Lean remotely well. my feedback is just that it would be helpful to mention that vscode is a requirement in the book, in case people start reading it independently and don't realize that yet ;-)

[Andrew Ashworth]

I'm loving the new update! Now when will we get C++ GUI Programming with Qt5? :wink:

[Reid Barton]

And what about the crossover titles, Lean GUI Programming with Qt and Interactive Theorem Proving with C++ Templates?

[Mario Carneiro]

Regarding "Interactive Theorem Proving with C++ Templates?", see also https://www.reddit.com/r/rust/comments/j9nnpv/proving_that_1_1_2_in_rust/

[Jasmin Blanchette]

Kevin Lacker said:

yeah, they don't work with Lean remotely well. my feedback is just that it would be helpful to mention that vscode is a requirement in the book, in case people start reading it independently and don't realize that yet ;-)

Indeed, I'll make sure to clarify all of this is the next edition. Thanks! I'm assuming it's OK if I thank @Kevin Lacker in the preface; if not, please let me know.

[Kevin Lacker]

feel free, but for such a minor nitpick there is no need to mention it

[Jasmin Blanchette]

I mention my boss for having noticed "the the" somewhere.

[Jasmin Blanchette]

I saw it as a great opportunity to sneak in a swearword (Fokkink).

[Jason Rute]

Reid Barton said:

And what about the crossover titles, Lean GUI Programming with Qt and Interactive Theorem Proving with C++ Templates?

@Patrick Massot started the first one here: https://github.com/leanprover-community/lean-client-python#qt-interface

[Kevin Buzzard]

(deleted)

[Jasmin Blanchette]

Johan Commelin said:

Jasmin Blanchette :rofl: touché
I'm really happy with all the energy you've been investing in this resource! I'm hoping I will be teaching a Lean course next summer, and I think this will be one of the two texts, next to MiL.

A long time ago, you wrote the above. Did you ever use the HG for any teaching? I'm trying to keep a list of who uses/used it.

[Johan Commelin]

(Un)fortunately I don't have to teach anything this year... So I haven't tried out the text yet on unexpecting students in Freiburg.