Zulip Chat Archive

Stream: general

Topic: TPiL


view this post on Zulip Jeremy Avigad (Aug 07 2020 at 00:20):

Hallelujah! Theorem Proving in Lean is finally updated, running with Lean 3.18.4 and using the community online version of Lean. I also did lots of searching and replacing to favor the use of Type* everywhere over writing universe u and Type u or just Type. I wasn't completely uniform, but second chapter lists all the variations and explains that they are equivalence.

TPiL can probably use other updates, revisions, and expansions, but for now I will focus efforts in Mathematics in Lean instead, since that is more focused on mathlib and the mathlib style of writing proofs.

view this post on Zulip Sam Estep (Aug 07 2020 at 02:58):

Amazing, thanks so much Jeremy! As a newcomer this is super helpful :)

view this post on Zulip Sam Estep (Aug 07 2020 at 02:58):

Just as a sanity check to make sure my installation is correct, I'm trying to run the tests locally but I'm again running into a bit of a snag even with the updated TPiL version (for reproducibility I'm using a custom Docker image which should just be Ubuntu 20.04 with Lean 3.18.4 installed according to the community instructions):

$ docker run -it registry.gitlab.com/sestep/lean-docker:9e940742
# git clone https://github.com/leanprover/theorem_proving_in_lean.git
# cd theorem_proving_in_lean
# git checkout 24e75ef
# lean --version
Lean (version 3.18.4, commit f539be1e867c, Release)
# make install-deps
# make leantest 2>&1 >/dev/null | grep ': error: ' | wc -l
262

As shown above, I seem to still be hitting quite a few errors; could someone correct my method here? From Jeremy's message earlier this evening I'm guessing I'm missing a leanproject up command somewhere, but when I run that, it doesn't seem to create a leanpkg.toml file as I had expected.


Last updated: May 14 2021 at 13:24 UTC