New name conflict with mathlib

Stream: CSLib

[Ching-Tsun Chou]

After the recent toolchain bump to v4.27.0, a theorem name used in my PR cslib#278, IsRegular.mul, becomes in conflict with a mathlib theorem:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Regular/Basic.html#IsRegular.mul
But git blame on the above mathlib file tells me that that theorem has been in existence since 2024. So what change in v4.27.0 has caused this name conflict?

[Jireh Loreaux]

I'm speaking without any knowledge here, but if I were guessing: it's that the Mathlib declaration was not previously imported in CSLib, but now is.

[Ching-Tsun Chou]

I doubt it. I did git grep -I Mathlib.Algebra in cslib commits before and after the toolchain bump and didn't see any difference.

[Eric Wieser]

I would guess you have a namespace issue in your PR, and intended to write Language.IsRegular.mul but wrote IsRegular.mul instead

[Eric Wieser]

Perhaps you dropped a namespace Language by accident when resolving a merge conflict

[Eric Wieser]

To help more we need to know more about what you mean by "becomes in conflict"; what was the actual error message?

[Ching-Tsun Chou]

In the file Cslib/Computability/Automata/NA/Pair.lean in cslib#278, there is a grind call on line 56:

  grind [IsRegular.mul, LTS.pairLang_regular]

which stopped working after I merged in the v4.27.0 bump in cslib's main branch, because IsRegular.mul now refers to the theorem in Mathlib.Algebra.Regular.Basic rather than the the theorem in Cslib/Computability/Languages/RegularLanguage.lean. Adding the Language. prefix fixes the problem:

  grind [Language.IsRegular.mul, LTS.pairLang_regular]

But the question is why IsRegular.mul worked before but doesn't now. The theorem Language.IsRegular.mul was not introduced in this PR or cslib#249 (on which this PR depends) but has been in cslib's main for a while. I did not encounter any merge conflicts when I merged the toolchain bump into cslib#249 or cslib#278.

[Chris Henson]

My assessment is the same as Jireh's, probably a change in what is transitively imported based on changes upstream in Mathlib.

[Ching-Tsun Chou]

Any way to find out for sure? I still have a repo which has not been bumped.

[Eric Wieser]

Sure, you can do #check _root_.IsRegular.mul in the unbumped repo and verify that it doesn't resolve

[Eric Wieser]

Or you could explicitly add the import to the old version of the file and verify that it breaks

[Eric Wieser]

I'm not sure I'd recommend it, but if you want to be immune to mathlib import restructuring, you can just import Mathlib everywhere

[Eric Wieser]

That way you always get everything and won't be surprised by things appearing and disappearing

[Chris Henson]

We've avoided this intentionally so far. For anything that's in main already, you'll get a failure in nightly-testing, so it won't be a complete surprise.

[Chris Henson]

Ching-Tsun Chou said:

Any way to find out for sure? I still have a repo which has not been bumped.

But to answer this, I have done everything but track down the Mathlib PR. The only thing that changed was the dependencies, and I can check out commits before and after and see that the resolution changes.

[Ching-Tsun Chou]

I just verified that #check _root_.IsRegular.mul doesn't resolve in the un-bumped repo. However, #check _root_.IsRegular does and points to the IsRegular defined in Mathlib.Algebra.Regular.Defs. So something happened in the version bump that put IsRegular.mul in the top level.

[Eric Wieser]

Right, what happened is that Mathlib.Algebra.Regular.Defs became transitively imported, as was discussed above

[Eric Wieser]

I'm not sure this is worth digging into further.

[Chris Henson]

Yes, seems resolved to me. Also note that this release is perhaps expected to be noisy as this included running the new module-aware shake in Mathlib. We are also planning (as soon as I make the PR) to unpin the Mathlib revision and move to more frequently running lake update, so in the future these kinds of changes will land in the main branch more frequently. (Not that this completely helps the case when a PR is open across these changes)

[Jireh Loreaux]

In addition, @Chris Henson, I think it's reasonable to alert the Mathlib maintainers if churn in Mathlib is becoming burdensome in CSLib. I think probably this instance doesn't rise to that occaision, but it's worth noting for future reference. Of course, the response might be "we're cleaning up the import hierarchy", but alternatively it may force us to keep a closer eye on things like this.

[Eric Wieser]

I think this is naturally something that module-izing mathlib will help address; removing public imports reduces the potential for leaked transitive results like this