v4.15.0 bug report - clashing Vector imports

Stream: lean4

[Eric Wieser]

I know this is an old release, but the following does not work:

import Init.Data.Vector.Lemmas
import Batteries.Data.Vector.Lemmas
-- error: ././././Batteries/Data/Vector/Lemmas.lean:20:18: 'Vector.ext' has already been declared

is there any mechanism in place to prevent this kind of regression in future?

[Eric Wieser]

(This slipped through the batteries CI because Init.lean did not transitively import Init.Data.Vector.Lemmas)

[Michael Rothgang]

Eric Wieser said:

(This slipped through the batteries CI because Init.lean did not transitively import Init.Data.Vector.Lemmas)

Is this something which can or should be linted against?

[Damiano Testa]

Would it be enough to have a CI step that imports "everything from everywhere"?

[Eric Wieser]

We already have such a test, but "everyhing" is import Mathlib,import Batteries ..., not import Mathlib.Foo import Batteries.Bar ...