Today's insane Mathlib import dependency

Stream: general

[Kim Morrison]

Mathlib.Topology.UnitInterval depends on Mathlib.FieldTheory.Subfield

[Kim Morrison]

Is that really necessary?

(Sorry, late here, and venting about slow builds...)

[Yaël Dillies]

tbf, FieldTheory.Subfield has actually not much to do with field theory

[Yaël Dillies]

It should probably be under Algebra.Field instead

[Kim Morrison]

UnitInterval.png

Anyone think they can snip enough edges here?

[Kim Morrison]

Presumably the target is the first edge.

[Kim Morrison]

If anyone is interested in doing more of this:

% lake exe graph --from Mathlib.FieldTheory.Subfield --to Mathlib.Topology.UnitInterval UnitInterval.png

[Yaël Dillies]

Yes, it's avoidable, but I would claim it's not as insane as one would think at first

[Yaël Dillies]

I'm happy to fix it now

[Kim Morrison]

The right general approach is to pick a file you love, run lake exe graph --to ThatFile out.png, then find something above it that you don't love, and work out how to cut it out. :-)

[Kim Morrison]

(Alternatively you can pick a file you're less fond of, run lake exe graph --from LessLovedFile out.png, and then see what you can rescue from downstream of it. :-)

[Julian Berman]

If you love it set it free, cut it down from the import tree.

[Eric Wieser]

Yaël Dillies said:

Yes, it's avoidable, but I would claim it's not as insane as one would think at first

Presumably the alternative is that we end up with a new topology file for every kind of subobject?

[Kim Morrison]

Yeah, I may have to retract the insanity of this one...

[Eric Wieser]

Scott Morrison said:

The right general approach is to pick a file you love, run lake exe graph --to ThatFile out.png, then find something above it that you don't love, and work out how to cut it out. :-)

Shouldn't you also work out if cutting the edge actually makes much difference? Spending hours to reduce the depth by one isn't a very good use of time, if there are other edges that reduce it by 5 or 10

[Eric Wieser]

In this case, FieldTheory.Subfield imports only Algebra.Algebra.Basic, and I would guess that cutting the edge will just mean that Algebra.Algebra.Basic comes in via a different route

[Eric Wieser]

(that is, the transitive reduction when producing these graph makes it harder to tell whether an edge is important)

[Yaël Dillies]

#11104

[Yaël Dillies]

Eric Wieser said:

In this case, FieldTheory.Subfield imports only Algebra.Algebra.Basic, and I would guess that cutting the edge will just mean that Algebra.Algebra.Basic comes in via a different route

In this specific case, I'm not too sure, because Algebra seems irrelevant to most of the theory

[Eric Wieser]

I think that confirms my point; the questionable edge is the one that isn't shown in the graph above

[Yaël Dillies]

That I agree