Moving Filter

Stream: mathlib4

[Yaël Dillies]

Mind moving all the filter under the Topology folder btw?

[Yury G. Kudryashov]

Yaël Dillies said:

Mind moving all the filter under the Topology folder btw?

I don't want to move files around without prior feedback from @Mario Carneiro on how it affects Mathport and his future leanup tool.

[Yury G. Kudryashov]

We had Filter under Order for a long time, we can wait a few more months until we have some tools/decisions about backward compatibility and renames.

[Mario Carneiro]

Yury G. Kudryashov said:

Yaël Dillies said:

Mind moving all the filter under the Topology folder btw?

I don't want to move files around without prior feedback from Mario Carneiro on how it affects Mathport and his future leanup tool.

The usual advice is still in effect here: if you want to split a file, clone the #align_import line into all the fragments, and if you want to join a file put two #align_import lines in the file. As for leanup, I wouldn't worry too much about it until we have a working system, because all of this will be considered "historical data" from leanup's perspective and we'll do the best we can with whatever is available. (leanup will probably make use of #align and #align_import to track renames and splits in historical data, because it's been around for a while and is relatively accurate.)

[Yury G. Kudryashov]

It's about moving Order/Filter to Topology/Filter, not splitting (I know what to do with splitting).

[Kim Morrison]

I think you can just leave the #align's as is, then, and everything will be fine re: mathport.

[Yury G. Kudryashov]

@Yaël Dillies If you want this to happen, then please open a new topic. I don't care where docs#Filter is located but other maintainers can have reasons not to move it.

[Mario Carneiro]

It's not obviously a better place for it to me

[Mario Carneiro]

a filter is kind of like a topology but they are sister concepts more than parent/child. PFilter is even more order theoretic

[Yury G. Kudryashov]

Let's postpone this discussion (offtopic for this thread) until Yael opens a new topic.

[Yaël Dillies]

Sorry it's annoying to move messages from phone (/impossible?) so I'll reply here: I want Filter to become Topology.Filter and Order.PFillter to become Order.Filter. Eventually, Topology.Filter will just be notation around Order.Filter and will be deletable or replaceable by notation.

[Mario Carneiro]

that seems... confusing

[Yaël Dillies]

Why so?

[Notification Bot]

A message was moved here from #mathlib4 > Linter for large files? by Yaël Dillies.

[Mario Carneiro]

you are giving two different definitions the same name

[Yaël Dillies]

That's why there are namespaces involved. Note that they have the same name in the literature already.

[Mario Carneiro]

Still annoying, since either you have a really long name for one of them or you open both and have name conflicts

[Mario Carneiro]

and more problematically, you have to look at an open halfway up the file when reading code to know which is being talked about

[Mario Carneiro]

Generally, I think the unqualified names of things in the same or adjacent domains should be distinct

[Mario Carneiro]

namespacing things with the same unqualified name is most useful when the same word is used for unrelated things in unrelated domains