Zulip Chat Archive

Stream: new members

Topic: coercions in TPL3

Mike Shulman (Oct 12 2022 at 18:27):

The section on coercions in Theorem Proving in Lean (3) says that the output sort and function type are fields of the typeclasses has_coe_to_sort and has_coe_to_fun. However, it seems that (now?) they are actually parameters:

structure has_coe_to_sort : Sort u  out_param (Sort v)  Sort (max (max 1 u) v)
has_coe_to_sort.coe : Π {a : Sort u} {S : Sort v} [self : has_coe_to_sort a S], a  S

structure has_coe_to_fun : Π (a : Sort u), out_param (a  Sort v)  Sort (max (max 1 u) v)
has_coe_to_fun.coe : Π {a : Sort u} {F : a  Sort v} [self : has_coe_to_fun a F] (x : a), F x

In particular, the "try it!" boxes in this section do not work, unless I edit them to move the fields to parameters, e.g.

instance Semigroup_to_sort : has_coe_to_sort Semigroup (Type u) :=
{coe := λ S, S.carrier}

instance morphism_to_fun (S1 S2 : Semigroup) :
  has_coe_to_fun (morphism S1 S2) (λ _, S1  S2) :=
{ coe := λ m, m.mor }

Is this something that can be fixed in TPL3, for those of us still using and teaching with Lean 3?

Johan Commelin (Oct 12 2022 at 18:51):

Hmm, the easy fix would be to pin TPL to an older version of Lean. Would that be acceptible?

Mike Shulman (Oct 12 2022 at 19:00):

That would make the "try it!" boxes work, but it would reduce the usefulness of TPL for people who want to learn Lean 3. Shouldn't they want to learn the most recent version?

Johan Commelin (Oct 12 2022 at 19:03):

Well, the hope is that ~ 6 months from now they should want to learn Lean 4.

Johan Commelin (Oct 12 2022 at 19:04):

So it's not clear whether it's worth it to try to bump TPL to recent Lean.

Patrick Massot (Oct 12 2022 at 19:04):

I think @Jeremy Avigad is still willing to maintain TPIL 3.

Jeremy Avigad (Oct 12 2022 at 21:32):

Yes, hopefully it won't be hard to fix. I'll take a look tomorrow.

Mike Shulman (Oct 12 2022 at 22:29):


Mike Shulman (Oct 13 2022 at 02:33):

Also: exercise 7.10.1 says

you should work within a namespace named hide, or something like that, in order to avoid name clashes.

but it appears that namespaces are not allowed to be named hide:

invalid namespace declaration, identifier expected
invalid 'hide' command, identifier expected

Mike Shulman (Oct 13 2022 at 04:08):

And it might be more helpful for section 1.2 to link to https://leanprover-community.github.io/ instead of https://github.com/leanprover/lean/.

Jeremy Avigad (Oct 13 2022 at 14:31):

Thanks! Will do.

Jeremy Avigad (Oct 14 2022 at 00:56):

I can't seem to build TPIL any more with Sphinx. TPIL uses a Python extension, lean_sphinx, by Gabriel. It handles the lean code blocks. I am getting the following error:

Could not import extension lean_sphinx (exception: cannot import name 'CodeBlock' from 'sphinx.directives' (/home/avigad/projects/theorem_proving_in_lean/.venv/lib/python3.10/site-packages/sphinx/directives/__init__.py))
make: *** [Makefile:27: leantest] Error 2

Does anyone have any ideas what to do? Maybe something has changed in recent versions of Sphinx? I also have Python 3.9 lying around, but that doesn't seem to work either.

Jeremy Avigad (Oct 14 2022 at 01:19):

O.k., the good news is that form this page,
I discovered that I should change from sphinx.directives import CodeBlock to from sphinx.directives.code import CodeBlock.

The bad news is updating mathlib and testing showed that dozens of things have broken. It will be a while before I'll have time to do this, and I am not sure it is worth it. @Mike Shulman , if you have the time and energy, you could give it a try. The README file is pretty self explanatory, and if you can get a version to build, I can deploy it. It will mostly be a matter of fixing imports for filenames that have changed, fixing theorem names that have changed, etc.

Mike Shulman (Oct 14 2022 at 01:22):

Ah, all right; maybe it isn't worth it then. I certainly don't have the time and energy. What about pinning it to an earlier version of Lean, as Johan suggested, but adding comments noting that some things have changed since it was written?

Jeremy Avigad (Oct 14 2022 at 01:37):

@Bryan Gin-ge Chen Is there a way to access a web version of an earlier version of Lean?

Bryan Gin-ge Chen (Oct 14 2022 at 01:40):

Unfortunately not at the moment, we don't have different versions of the web editor. The community web editor is also frozen at the moment since the ZIP file containing mathlib oleans has gotten too big for GitHub pages.

Jeremy Avigad (Oct 14 2022 at 01:42):

O.k., thanks. Anyhow, it would be nice to update TPIL. I'll put it on my todo list and wait for a lazy Sunday afternoon to spend a couple of hours making all the little fixes.

Last updated: Dec 20 2023 at 11:08 UTC