Stream: general

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

Jasmin Blanchette (Oct 13 2020 at 11:57):

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 (Oct 13 2020 at 13:24):

Jasmin Blanchette said:

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

Jasmin Blanchette (Oct 13 2020 at 16:11):

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

Jasmin Blanchette (Oct 13 2020 at 16:19):

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 (Oct 13 2020 at 17:49):

@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 (Oct 13 2020 at 18:02):

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 (Oct 13 2020 at 18:02):

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

Kevin Lacker (Oct 13 2020 at 18:07):

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

Marc Huisinga (Oct 13 2020 at 18:09):

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 (Oct 13 2020 at 18:11):

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

Kevin Lacker (Oct 13 2020 at 18:14):

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 (Oct 13 2020 at 18:41):

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

Kevin Lacker (Oct 13 2020 at 18:45):

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 (Oct 13 2020 at 18:45):

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

Kevin Lacker (Oct 13 2020 at 18:50):

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 (Oct 13 2020 at 18:53):

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 (Oct 13 2020 at 19:03):

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 (Oct 13 2020 at 21:02):

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

Reid Barton (Oct 13 2020 at 21:48):

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

Mario Carneiro (Oct 14 2020 at 00:08):

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 (Oct 14 2020 at 06:20):

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 (Oct 14 2020 at 06:25):

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

Jasmin Blanchette (Oct 14 2020 at 07:09):

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

Jasmin Blanchette (Oct 14 2020 at 07:28):

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

Jason Rute (Oct 14 2020 at 17:14):

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 (Oct 14 2020 at 17:15):

(deleted)

Last updated: May 14 2021 at 02:15 UTC