What files were ported in #641?

Stream: mathlib4

[Arien Malec]

@Jireh Loreaux -- I marked Mathlib.Int.Cast.Basic as ported in the tracking file -- not sure if that's fully correct or just "in progress"? Would you mind going through and seeing if there are other files you ported in mathlib4#641 that aren't tracked as such?

[Scott Morrison]

I think that was incorrect, and Mathlib.Int.Cast.Basic is still an "ad-hoc" port.

[Scott Morrison]

I've switched it back to 'No' in #port-status.

[Scott Morrison]

It looks like there's not much of a diff at this point, but there are many missing lemmas that need either porting or porting notes if they shouldn't be ported!

[Ruben Van de Velde]

Diff with mathport: https://gist.github.com/Ruben-VandeVelde/f4771dbb0d4f048add1a5f848d3b9a84

[Arien Malec]

We should do a comparison between the files in Mathlib.lean and #port-status -- I've found more examples of untracked files...

[Arien Malec]

Rather than note it as "No" should we note it as WIP or partial?

[Scott Morrison]

No, there's currently no good way to record than an "ad-hoc" port already exists.

[Scott Morrison]

We're going to run out of these ad-hoc ported files pretty soon anyway.

[Scott Morrison]

But when we switch to a more verbose yaml format maybe we can track them.

[Arien Malec]

cc @Yakov Pechersky

[Yakov Pechersky]

How should the file list in port-status be updated -- based on what files exist in mathlib3? What if there are files that are still being ported, that no longer have a mathlib3 counterpart, at some instance in time? There are various race conditions at play here.

[Jireh Loreaux]

I never changed the port status of that file, I'm not sure who did. I didn't port it in mathlib4#641. I only moved those lemmas there because they already existed in mathlib4 and that's where they ultimately belong.

[Jireh Loreaux]

That particular race condition doesn't seem all that likely, unless the contents just get moved, and then this should show up easily in the list of files that have changed since they were verified against a given SHA.

[Scott Morrison]

@Jireh Loreaux, it's okay, I think it was just a mistake by Arien. No harm.

[Arien Malec]

mistake on my part -- that's why I was explicit in posting here, to check.

[Jireh Loreaux]

Sorry, I misread your post anyway (I just reread it). For some reason I thought you said that I had marked it as ported.

[Jireh Loreaux]

My apologies.

[Arien Malec]

@Yakov Pechersky might have a mini-state machine for status: No (no file or PR exists), Claimed (no PR exists), WIP (PR exists, not merged), Stub (merge of limited defs only), Ported (fully ported)?

[Yakov Pechersky]

Sure! Although I don't really see the need for claimed, no branch. I don't know how much the tooling needs to enforce states through controlling state-transitions.

[Arien Malec]

I generally mark the status when I push the initial PR anyway -- I prefer to get the WIP out there...

[Jireh Loreaux]

FYI: I have ported Data.Int.Cast.Basic as mathlib4#670