init files not being included

Stream: general

[Daniel Selsam]

Is there a reason some files (e.g. init.data.sum.instances) are not being included in init (e.g. are not included in init.data.sum.default)? The result is that lean/all and mathlib/all both have different declarations for sum.decidable_eq. Atleast on the Lean4 side after mathporting, the Lean3 and Mathlibpackages cannot be imported together. It is not a problem, only a minor annoyance.

[Mario Carneiro]

What? I would guess that such a file has been forgotten then, because I have never seen a file from init.* being imported in a non-prelude file

[Mario Carneiro]

Yep, init.data.sum.instances is imported nowhere

[Mario Carneiro]

Do you know any other files in init.* which are not reachable from init.default?

[Daniel Selsam]

Not off the top of my head.

[Mario Carneiro]

How did you make lean/all? Can you send it to me?

[Mario Carneiro]

leanproject mk-all doesn't seem to work in lean/library

[Mario Carneiro]

Ah, I got it. Looks like there is one other orphan file: init.meta.decl_cmds

[Mario Carneiro]

I recognize this file, it was used for the original version of to_additive before it got fancy