Mysterious import failure

Stream: lean4

[Patrick Massot]

I have a new error message today when importing my library in some of my other projects:

import failed, environment already contains 'tactics._closed_6._cstage2'

Does someone know what those _closed_6 and _cstage2 could come from?

[Mario Carneiro]

those are auxiliary definitions containing IR for the compiler

[Mario Carneiro]

the important part is that you made the same definition in two imports

[Mario Carneiro]

you are just getting the error about the compiler decls slightly in advance of the same error saying that 'tactics' is also doubly defined

[Patrick Massot]

Thanks. A slightly more explicit error message would be useful.