Should we mark Mathlib.Data.RBTree.* as ported?

Stream: mathlib4

[Arien Malec]

These shouldn't block anything (e.g., porting data.list.defs) because they are "don't port"

[Scott Morrison]

I propose we make the file over on the mathlib4 side. It can be empty, besides a module-doc explaining that none of the content needed porting, as Std4's RBMap is meant to be a complete replacement, and all tactic development will use that. This stub file is helpful documentation, and means we won't need to special case any CI that attempts to track progress.

[Arien Malec]

Mario just closed the PR that got there. :grinning:

[Arien Malec]

I can do another PR with totally empty content except for the comments…

[Scott Morrison]

@Mario Carneiro, would that be okay? I like the idea of porting as doc-string-only files, just so these files (and others like them) stop showing up on the list of things that need porting. Alternatively we can just warn people off them until the YAML update and there's a way of annotating "no port required".

[Mario Carneiro]

I'm going to handle data.rbtree myself. Please mark them as WIP mario

[Scott Morrison]

Done. Marked as WIP on #port-status, for data.rbtree.* and data.rbmap.*