Declaration is not allowed to exist

Stream: mathlib4

[Iván Renison]

Hello, I made a commit and the CI failed with an error mentioning a file that I didn't modify: https://github.com/leanprover-community/mathlib4/actions/runs/7213319694/job/19652944627
I modified the files Mathlib/Data/Fin/Basic.lean, Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean and Mathlib/Combinatorics/SimpleGraph/Hasse.lean.
The CI says when building Mathlib/Data/Fin/Basic.lean:

Error: ./././Mathlib/Data/Multiset/FinsetOps.lean:286:18: error: Declaration Set.sInter is not allowed to exist in this file

Does somebody know what is the error?

[Patrick Massot]

This is CI checking the import graph has not been messed up.

[Patrick Massot]

Did you modify the import graph?

[Iván Renison]

I added:

import Mathlib.Data.Nat.Parity
import Mathlib.Algebra.Parity
import Mathlib.Init.CCLemmas

In Mathlib/Data/Fin/Basic.lean

[Yaël Dillies]

Yeah, that's pretty messed up in terms of imports.

[Patrick Massot]

You have your answer then.

[Arthur Paulino]

For the sake of clarity, what does "messed up" mean in this context? The message Declaration Set.sInter is not allowed to exist in this file is not very insightful

[Yaël Dillies]

Data.Fin.Basic is one of the earliest files in mathlib. In comparison, Data.Nat.Parity imports the first part of the algebraic order hierarchy because it uses order properties of the naturals

[Arthur Paulino]

So it's a cyclic import?

[Iván Renison]

I can delete import Mathlib.Algebra.Parity and import Mathlib.Init.CCLemmas and it still works
Data.Nat.Parity I used it for the following theorem:

theorem Even_iff_even_val (u : Fin 2) : Even u ↔ Even u.val := sorry

But I guess I have to move it to another file, right? And to what file should I move it?

[Yaël Dillies]

Data.Fin.Parity, maybe?

[Yaël Dillies]

Arthur Paulino said:

So it's a cyclic import?

Not quite, because we avoid importing Fin in the most basic parts of the library, including the algebraic order hierarchy.

[Iván Renison]

Yaël Dillies said:

Data.Fin.Parity, maybe?

Ok, I will do that

[Iván Renison]

Maybe I can write some other basic theorems about parity of Fin and make a separate pull request

[Eric Wieser]

Iván Renison said:

I can delete import Mathlib.Algebra.Parity and import Mathlib.Init.CCLemmas and it still works
Data.Nat.Parity I used it for the following theorem:

theorem Even_iff_even_val (u : Fin 2) : Even u ↔ Even u.val := sorry

But I guess I have to move it to another file, right? And to what file should I move it?

I think @Yury G. Kudryashov already has a PR with this result

[Yaël Dillies]

#8960

[Kyle Miller]

Iván Renison said:

Error: ./././Mathlib/Data/Multiset/FinsetOps.lean:286:18: error: Declaration Set.sInter is not allowed to exist in this file

Does somebody know what is the error?

There's a comment about the purpose of the check in the file it's referencing, right before line 286. (It's Data/Multiset/FinsetOps.lean, not Data/Fin/Basic.lean by the way).

https://github.com/leanprover-community/mathlib4/blob/3465d1aaae242475fad59e688648a2285031d19e/Mathlib/Data/Multiset/FinsetOps.lean#L284-L286

[Kyle Miller]

I guess someone could make assert_not_exists accept a docstring and have it print the docstring as an additional error message, but at least the error shows a file and line number.

[Scott Morrison]

#9070 expands on the error message that assert_not_exists produces, hopefully making it clearer what is going on!