simpNF failure in unrelated file

Stream: mathlib4

[Chris Hughes]

My PR !4#6617 is failing to build because of a failure in Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean. The file that's failing doesn't even import anything I've changed. What should I do here, do I just crank up the heartBeats in that file? Or is it a sign that I've done something bad in my PR?

[Ruben Van de Velde]

The linter runs on Mathlib.lean, so it imports both that file and your new files

[Ruben Van de Velde]

It seems to be trying to find a CharP instance, so maybe try commenting out charP_of_model_fieldOfChar

[Chris Hughes]

I discovered what's probably an unreleated issue, but importing FieldTheory/Adjoin into Geometry/Manifold/Algebra/LeftInvariantDerivation breaks everything because of a notation clash

[Chris Hughes]

Ruben Van de Velde said:

It seems to be trying to find a CharP instance, so maybe try commenting out charP_of_model_fieldOfChar

That's fixed it. Thanks

[Kevin Buzzard]

Interesting that char 0 was also causing timeouts recently.