Passing the Theorem Proving in Lean unit tests?

Stream: general

[Sam Estep]

Hi all! I'm still fairly new to Lean and am working through the Theorem Proving in Lean book (currently on Chapter 5), but occasionally I've been running into things that don't work for me locally. As a sanity check, I went to try running the test suite for the book, but that also failed on my machine, so it seemed like just an issue with my local Lean setup. But when I tried running the tests in a Docker image built using the Lean Community Ubuntu instructions, I got exactly the same errors (pasted here):

$ curl https://raw.githubusercontent.com/samestep/lean-docker/8846c6c/Dockerfile | docker build -t lean -
$ docker run -it lean
# git clone https://github.com/leanprover/theorem_proving_in_lean.git
# cd theorem_proving_in_lean
# make install-deps
# make leantest

Is there something wrong with my Lean setup (both locally and in the linked Dockerfile), or are these tests simply out of date? If the latter, would it be worthwhile if I submit a PR fixing the tests, and possibly adding some sort of CI setup to the repo for the book?

[Patrick Massot]

You are probably using a lean version which is too recent for this book.

[Sam Estep]

Patrick Massot said:

You are probably using a lean version which is too recent for this book.

Ah that would make sense; what's a version that works with the book?

[Chris Wong]

The "leanprover" organization (as opposed to "leanprover-community") is for the original Microsoft version of Lean 3.x, which is no longer developed

[Chris Wong]

So that repo probably uses the last Microsoft release, Lean 3.4

[Scott Morrison]

This is not quite accurate.

[Scott Morrison]

Lean is still being very actively developed, by Leonardo de Moura at Microsoft, but they are working on Lean 4.

[Scott Morrison]

It is true that Lean 3 is no longer being developed in the leanprover organisation.

[Utensil Song]

I would suggest rewriting the examples/tests/exercises in #tpil to work under the community Lean to learn the evolution since 3.4 instead of sticking to 3.4 and learn some outdated muscle memory.

[Patrick Massot]

Sure, but @Jeremy Avigad only has 24 hours per day...

[Utensil Song]

Oh I meant for beginners reading #tpil and doing exercises in it. This task is a good first task, easy enough for any beginner.

[Sam Estep]

Utensil Song said:

I would suggest rewriting the examples/tests/exercises in #tpil to work under the community Lean to learn the evolution since 3.4 instead of sticking to 3.4 and learn some outdated muscle memory.

That sounds like a good idea! I've forked the repo to my personal GitHub to start working on that. Is there a more recent (Lean 3 community) reference that I can refer to while doing this? I notice that The Lean Reference Manual is also outdated as you describe

[Utensil Song]

There’s no such an updated reference AFAIK. I just picked things up by reading changelog or reading/searching/asking on Zulip. Hopefully there would be an updated one for Lean 4.

[Utensil Song]

（deleted）

[Sam Estep]

Also, looking at the topics in the "new members" stream vs this one, it seems like I may have started this topic in the wrong stream; apologies for that! I'll ask further questions about this in the "new members" stream to avoid spamming this one with off-topic messages

[Jeremy Avigad]

It might not be too hard to update TPiL to the latest version of Lean. Patrick is right that I am juggling a number of things, but it is on my to-do list...