Build failing: declaration not allowed to be imported

Stream: mathlib4

[Christian Merten]

The PR #9879 was delegated to me and after adapting the last suggestion by @Joël Riou, I waited for CI to pass (which it did) and then commented bors r+. Now the bors build is failing with Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean:407:18: error: Declaration Field is not allowed to be imported by this file. This error did not appear in the previous CI builds. Is this related to the changes in #9879? Maybe the import that I added to the FinCategory file?

[Christian Merten]

And, why did that not cause failure in regular CI builds?

[Christian Merten]

I traced it back: I think it is indeed the line import Mathlib.CategoryTheory.SingleObj in the FinCategory file because the former transitively imports Mathlib.Algebra.Field.Defs which causes this error.

[Oliver Nash]

It looks like you need to get the latest master and merge it into that branch. The error will then surface for you locally and you can fix it. And then you can send it back to bors.

[Kim Morrison]

Possibly the solution is to split up SingleObj into a part with just the basic definitions, and another part that gives the connections with various algebraic structures.

[Kim Morrison]

Another approach would be to create a new file importing both FinCategory and SingleObj.

[Kim Morrison]

(I just added this assert_not_exists this week. Apologies that it had tripped you up, but good to know it is doing its job. :-)

[Christian Merten]

Scott Morrison said:

Possibly the solution is to split up SingleObj into a part with just the basic definitions, and another part that gives the connections with various algebraic structures.

I just went with moving the instance from the FinCategory file to SingleObj and importing FinCategory there, this fixed the assert_not_exists error.

[Christian Merten]

The only "algebraic" import in SingleObj is Mathlib.Algebra.Category.MonCat.Basic which is necessary for the definition, so I think splitting up SingleObj wont help here.