mathlib4-port-status-new

Stream: mathlib4

[Johan Commelin]

I just discovered https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status-new
Is this actually used somewhere?

[Eric Wieser]

@Yakov Pechersky created it as an example of what the updated mathlibtool code could parse

[Eric Wieser]

No attempt was made to switch to that format

[Eric Wieser]

But it would be very easy to switch, since I think think port-status generates the yaml in that format

[Johan Commelin]

Ok, thanks for the info. So it's orthogonal to the changes that Reid and I are working on.

[Eric Wieser]

Yes; but it preserves free-form comments, which your approach might not

[Eric Wieser]

(there is a comment field)

[Johan Commelin]

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20status
We are proposing a new file for recording free-form comments.

[Yakov Pechersky]

My hope with the yaml format was to decouple stiff data, like porting, hash, PR number, from free-form data

[Yakov Pechersky]

But also keep it in the same place

[Yakov Pechersky]

In a way that would be amenable to automation

[Scott Morrison]

I'm going to delete this now.