Porting status for lean3 core

Stream: mathlib4

[Heather Macbeth]

We have the port status page
https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status
for files from mathlib3, but is there a place to check the status of files from lean3 core? Just now I wanted to use
docs#int.linear_order
which in lean3 is in core, init.data.int.order. (Not to be confused with the more advanced file data.int.order in mathlib3.). It doesn't seem to be in mathlib4's Mathlib.Init.Data.Int.*, but other than looking in that folder I wasn't sure how to determine the status.

[Heather Macbeth]

In this case I tracked down Int.LinearOrder to Mathlib.Init.Data.Int.Basic, but still curious about the general principle.

[Scott Morrison]

No, at the moment there is no equivalent of #port-status for Lean 3 core. I had been hoping that it was a (small) finite amount of work to finish porting that, and the overhead expense of tracking wouldn't be worth it, because we'd be done so soon.

[Scott Morrison]

However it's looking like this was incorrect.

[Scott Morrison]

mathlib4#512 ran into a similar problem, when I realised that Mathlib.Init.Logic is only a partial / ad-hoc port.

[Scott Morrison]

Actually, I retract that, Mathlib.Init.Logic is complete.

[Mario Carneiro]

Yeah I did Init.Logic in mathlib4#490

[Mario Carneiro]

I think we do need to track these

[Mario Carneiro]

I think it will certainly be smaller scale but from another POV that means we can use it to test our porting infrastructure

[Heather Macbeth]

Currently Mathlib.Init.Data.Int.Basic contains one instance from init.data.int.order and two lemmas from data.int.basic. Would it make sense to be very strict about filenames, thus moving these to Mathlib.Init.Data.Int.Order and Mathlib.Data.Int.Basic respectively? This would ensure that people know where to look, even without having a full tracking system.

[Mario Carneiro]

Yes, we should be strict about positioning lemmas, although there are some places where I think we can untangle dependencies from mathlib that are currently causing pain which will be hindered by strictly following the mathlib order. One way to fix this is to say that mathlib4 is allowed to have new files, and old (original mathlib) files may import new files, so if you move a definition to a new file and import it from the old file then that gives the flexibility to change things.

[Kevin Buzzard]

I've ported init.data.bool.basic and init.data.bool.lemmas, I hope to open the PR today