TPiL

Stream: general

[Jeremy Avigad]

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.

[Sam Estep]

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

[Sam Estep]

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.