cleaning up the to-be-ported list

Stream: mathlib4

[Scott Morrison]

@Mario Carneiro, what is the plan for:

data.rbmap.basic
data.rbtree.basic
data.rbtree.default
data.rbtree.default_lt
data.rbtree.find
data.rbtree.init
data.rbtree.insert
data.rbtree.main
data.rbtree.min_max

They are all marked as WIP @digama0, and not otherwise needed for other files. Shall we just mark these all as should_port: false?

[Mario Carneiro]

I think so, they will not be ported in mathlib

[Mario Carneiro]

they are about 90% ported in std

[Scott Morrison]

In mathlib3 file#logic/equiv/array has doc-comment

We keep this separate from the file containing `list`-like equivalences as those have no future
in mathlib4.

does this mean I can mark the file as not-for-porting?

[Mario Carneiro]

This file is not likely to move to std unless Equiv does

[Mario Carneiro]

but also, array is basically dead in lean 4 right now, Array is a different type

[Scott Morrison]

That's what I was thinking -- the only place we use this is in file#data/fintype/array, which itself is a leaf file. Thus I'd suggest we mark both files as not for porting.

[Eric Wieser]

Note that should_port: false is not actually read by anything

[Eric Wieser]

Didn't we port port-status#data/array/lemmas? Edit: seems not

[Scott Morrison]

Eric Wieser said:

Note that should_port: false is not actually read by anything

Is there a way to make a file disappear from the dashboard?

[Eric Wieser]

There's an open PR to add support for that flag

[Eric Wieser]

I never bothered to merge it because it became moot when you deleted all the default files in mathlib3