Zulip Chat Archive

Stream: general

Topic: Passing the Theorem Proving in Lean unit tests?


Sam Estep (Jul 25 2020 at 16:54):

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 (Jul 25 2020 at 17:00):

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

Sam Estep (Jul 25 2020 at 17:01):

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 (Jul 26 2020 at 01:34):

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 (Jul 26 2020 at 01:34):

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

Scott Morrison (Jul 26 2020 at 01:34):

This is not quite accurate.

Scott Morrison (Jul 26 2020 at 01:35):

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

Scott Morrison (Jul 26 2020 at 01:35):

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

Utensil Song (Jul 26 2020 at 13:15):

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

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

Utensil Song (Jul 26 2020 at 13:29):

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 (Jul 26 2020 at 16:05):

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 (Jul 26 2020 at 16:15):

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 (Jul 26 2020 at 16:16):

(deleted)

Sam Estep (Jul 26 2020 at 16:32):

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 (Jul 27 2020 at 14:28):

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...


Last updated: Dec 20 2023 at 11:08 UTC