ad hoc files

Stream: mathlib4

[Johan Commelin]

Can we generate an easy overview of which files are ad hoc ports? Is it just all the .lean files that don't have a porting header at the top?

[Johan Commelin]

Gives me this list:

Mathlib/Control/Random.lean
Mathlib/Control/SimpSet.lean
Mathlib/Control/Writer.lean
Mathlib/Data/Array/Basic.lean
Mathlib/Data/Array/Defs.lean
Mathlib/Data/BinaryHeap.lean
Mathlib/Data/ByteArray.lean
Mathlib/Data/Equiv/Functor.lean
Mathlib/Data/Finset/Basic.lean
Mathlib/Data/Fintype/Basic.lean
Mathlib/Data/HashMap.lean
Mathlib/Data/KVMap.lean
Mathlib/Data/List/Card.lean
Mathlib/Data/List/Chain.lean
Mathlib/Data/List/Nodup.lean
Mathlib/Data/List/Pairwise.lean
Mathlib/Data/List/Perm.lean
Mathlib/Data/List/Range.lean
Mathlib/Data/Multiset/Basic.lean
Mathlib/Data/Multiset/Nodup.lean
Mathlib/Data/Nat/ForSqrt.lean
Mathlib/Data/String/Defs.lean
Mathlib/Data/String/Lemmas.lean
Mathlib/Data/UInt.lean
Mathlib/Data/UnionFind.lean
Mathlib/Init/Algebra/Classes.lean
Mathlib/Init/Algebra/Functions.lean
Mathlib/Init/Algebra/Order.lean
Mathlib/Init/Align.lean
Mathlib/Init/CcLemmas.lean
Mathlib/Init/Classical.lean
Mathlib/Init/Control/Combinators.lean
Mathlib/Init/Core.lean
Mathlib/Init/Data/Bool/Basic.lean

[Eric Wieser]

!4#4000 knocks one off this list

[Eric Wieser]

Many of these ad-hoc files seem to be missing #align statements; did we put the aligns in another file, or are we just relying on the names not having changed?

[Ruben Van de Velde]

Did we have #align when those were added? :)

[Eric Wieser]

It seems we did, but perhaps added manually

[Yakov Pechersky]

Having #align after every decl was a choice made later -- in fact, earlier, the idea was that #align were to be added only in instances when one really needed it. But for some files, almost every decl needed it. I had asked Mario, can we, instead of "whitelisting" and writing in #align, get a file that had #align for everything, and delete the ones that were tautological? And I think that then moved to "don't delete tautological #align at all".