!4#2798 simpNF

Stream: mathlib4

[Jeremy Tan]

!4#2798 is failing in the lint stage repeatedly

[Jeremy Tan]

should the currently running bors build be stopped?

[Jeremy Tan]

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
#check CategoryTheory.Functor.map_add.{u_4, u_3, u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.Functor.mapAddHom_apply.{u_1, u_2, u_3, u_4} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.Functor.map_neg.{u_4, u_3, u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.Functor.map_sub.{u_4, u_3, u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.Functor.map_sum.{u_5, u_4, u_3, u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject D
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.AdditiveFunctor.forget_map.{u_4, u_3, u_2, u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject (C ⥤ D)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.AdditiveFunctor.ofLeftExact_map.{v₁, v₂, u₁, u₂} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject (C ⥤+ D)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.AdditiveFunctor.ofRightExact_map.{v₁, v₂, u₁, u₂} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject (C ⥤+ D)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
#check CategoryTheory.AdditiveFunctor.ofExact_map.{v₁, v₂, u₁, u₂} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CategoryTheory.Limits.HasZeroObject (C ⥤+ D)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit) -/
make: *** [GNUmakefile:16: lint] Error 1
Error: Process completed with exit code 2.

[Johan Commelin]

@Jeremy Tan Thanks! I took it of the queue.

[Johan Commelin]

Wait, that's the wrong PR!

[Jeremy Tan]

Umm... I believe I put the right PR here

[Johan Commelin]

The linting errors are all about category theory. But that PR doesn't have anything to do with it.

[Jeremy Tan]

The errors all relate to the CategoryTheory.Preadditive.AdditiveFunctor port that was pushed a mere hour ago. Perhaps the "ripple effect" changes from Data.Fintype.Basic need to be extended to that file

[Chris Hughes]

!4#2797 is currently failing. I think that was the problem

[Jeremy Tan]

Right...

[Chris Hughes]

Although it is very strange that that file would cause problems

[Jeremy Tan]

Maybe it's just bors getting confused, instead of mathport

I saw the build for !4#2798 fail three times

[Johan Commelin]

Hmmm, that is very weird indeed

[Johan Commelin]

Ok, I took it of the queue again

[Chris Hughes]

I ran the Linter for !4#2797 locally and it failed. Although #lint in the file where it failed seemed to succeed.

[Chris Hughes]

I guess maybe runLinter checks for simpNF after importing everything and #lint doesn't do that?

[Jeremy Tan]

Jeremy Tan said:

Maybe it's just bors getting confused, instead of mathport

I saw the build for !4#2798 fail three times

Re this: https://lichess.org/twejU3rW/black

image.png

[Chris Hughes]

I just tried runLinter on current master and it failed

[Chris Hughes]

That's the problem

[Chris Hughes]

Sorry, that's not the problem, I had old oleans.

[Kyle Miller]

@Jeremy Tan Something to know about bors that might not be obvious is that it merges batches of PRs and does a single build. When there are build failures it rebuilds subsets.

[Notification Bot]

Jeremy Tan has marked this topic as resolved.

[Notification Bot]

Jeremy Tan has marked this topic as unresolved.

[Jeremy Tan]

merge conflict at !4#2803

[Jeremy Tan]

also it looks like some more PRs could be marked as ready

[Jeremy Tan]

*to merge

[Johan Commelin]

@Jeremy Tan ready-to-merge is added automatically when a maintainer gives the bors r+ (= bors merge) command.

[Jeremy Tan]

yeah I know that

[Johan Commelin]

If there are some PRs that you have reviewed and you think they look good, then please "Approve" them using the github interface.

[Johan Commelin]

This is very helpful for maintainers, because they get the signal that another person think a PR is ready

[Jeremy Tan]

so, like this? !4#2782

[Jeremy Tan]

!4#2769 just failed with the simpNF errors, that's got to be the one

[Kyle Miller]

How do you mean? It's not on the bors queue, unless you're inferring something from whatever mattrobball merged something into this an hour ago.

[Matthew Ballard]

I did some poking at this.

• everything builds fine
• #lint is clear on CategoryTheory/Preadditive/AdditiveFunctor.lean
• #synth Limits.HasZeroObject D fails after L54 on the same file
• runLinter fails on this branch on my machine
• runLinter succeeds on master on my machine
• runLintersucceeds on this branch after removing CategoryTheory/Abelian/Basic.lean (the only new file)

The errors from simpNF all complain about missing HasZeroObject instances on things where they should not be necessary (Preadditive does not extend HasZeroObject unless I mistaken).

[Matthew Ballard]

If simpNF is trying to go from Preadditive to Abelian something is weird

[Matthew Ballard]

Lean knows it does not need the HasZeroObject instances (as it shouldn't) but for some reason simpNF is looking for them

[Matthew Ballard]

I probably won't have much time to look at this more until this evening. Anyone should feel free to diagnose and cure. (And then we can knock off another target.)

[Jeremy Tan]

Typo fix: !4#2816

[Jeremy Tan]

…now I'm getting the same problem in the workflow for my own !4#2816 !!!