Zulip Chat Archive

Stream: mathlib4

Topic: mathport #print

Winston Yin (Dec 07 2022 at 06:09):

Why is mathport inserting all these #print statements and commenting much of the code out?

Winston Yin (Dec 07 2022 at 06:09):

https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Algebra/Order/Ring/Defs.lean

Mario Carneiro (Dec 07 2022 at 06:19):

That means that the declaration already exists (the #print is to remind you of that, and the commented code shows what mathport would have otherwise produced in case that is interesting to you)

Mario Carneiro (Dec 07 2022 at 06:20):

it is intended to help find new declarations in already ported files since they stand out by being the only uncommented things

Mario Carneiro (Dec 07 2022 at 06:21):

You can also change the mathport configuration to either not comment them out or to completely remove them

Winston Yin (Dec 07 2022 at 06:22):

So the content in Algebra.Order.Ring.Defs has already been ported?

Winston Yin (Dec 07 2022 at 06:23):

Right! It has all gone into Algebra.Order.Ring

Winston Yin (Dec 07 2022 at 06:29):

The port status page says algebra.order.ring.defs is a "No", but it seems it's been ported into Algebra.Order.Ring and Algebra.Order.Ring.Lemmas. Should this be reflected on the port status page somehow?

Mario Carneiro (Dec 07 2022 at 06:33):

they should be moved where they belong

Mario Carneiro (Dec 07 2022 at 06:33):

some of the ad hoc ports put stuff in the wrong place

Winston Yin (Dec 07 2022 at 06:34):

So I should move them to be in parity with mathlib3?

Scott Morrison (Dec 07 2022 at 07:06):

Yes, Algebra.Order.Ring was an adhoc port.

Scott Morrison (Dec 07 2022 at 07:07):

So you should treat it as a big pile of garbage, except:

  • if there are broken proofs in the output of mathport, it's possible you'll find a usable proof in the ad hoc ported file
  • sometimes there is something in the ad hoc ported file that a tactic needs, and you can't just throw out. In this case, find a new home for it (probably by moving it to another ad-hoc ported file, or asking here)

Scott Morrison (Dec 07 2022 at 07:08):

You need to get Algebra.Order.Ring.Defs to match the current mathlib3 version as closely as possible, and you also need to keep all the tactics working. :-)

Winston Yin (Dec 07 2022 at 22:17):

Thanks. I've started the process. Since protected_proj hasn't been ported yet, how can I manually add protected to the projections of a class? Also, how do I see a list of all projections?

Scott Morrison (Dec 07 2022 at 22:38):

You just write protected in front of the field names when you define the structure/class.

Winston Yin (Dec 07 2022 at 22:52):

In class Foobar extends Foo, how do I protect Foobar.toFoo?

Ruben Van de Velde (Dec 07 2022 at 22:54):

I don't :)

Last updated: Dec 20 2023 at 11:08 UTC