Zulip Chat Archive

Stream: general

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


view this post on Zulip 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.

view this post on Zulip Rob Lewis (Oct 13 2020 at 13:24):

Jasmin Blanchette said:

optimized for tablets and ebook readers (A5).

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

view this post on Zulip Jasmin Blanchette (Oct 13 2020 at 16:11):

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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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. ;)

view this post on Zulip Jasmin Blanchette (Oct 13 2020 at 18:02):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Oct 13 2020 at 18:11):

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

view this post on Zulip 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

view this post on Zulip Jasmin Blanchette (Oct 13 2020 at 18:41):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 ;-)

view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip Kevin Lacker (Oct 14 2020 at 06:25):

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

view this post on Zulip Jasmin Blanchette (Oct 14 2020 at 07:09):

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

view this post on Zulip Jasmin Blanchette (Oct 14 2020 at 07:28):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 14 2020 at 17:15):

(deleted)


Last updated: May 14 2021 at 02:15 UTC