simpNF linter

Stream: general

[MohanadAhmed]

In PR #6042 the CI run 15248409473 fails at the simpNF linter and produces the following output. I thought it could have been the simp lemmas I added (similar to this zulip thread interfering with something so I disabled all simp lemmas in the PR. Still the same thing!

I also looked at zulip discussion here and here and searching for simpNF but could not find something applicable.

Note again the PR does not touch these files Mathlib/Data/Fin/Basic.lean and Mathlib/Topology/ContinuousFunction/Bounded.lean where the linter is reporting errors

/- 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.Data.Fin.Basic
Error: ./Mathlib/Data/Fin/Basic.lean:959:1: error: Fin.add_one_lt_iff LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CovariantClass (Fin (n + 2)) (Fin (n + 2)) (fun x x_1 => x + x_1) fun x x_1 => x < x_1
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
Error: ./Mathlib/Data/Fin/Basic.lean:987:1: error: Fin.lt_add_one_iff LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CovariantClass (Fin (n + 1)) (Fin (n + 1)) (fun x x_1 => x + x_1) fun x x_1 => x < x_1
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
Error: ./Mathlib/Data/Fin/Basic.lean:2039:1: error: Fin.sub_one_lt_iff LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  CovariantClass (Fin (n + 1)) (Fin (n + 1)) (fun x x_1 => x + x_1) fun x x_1 => x < x_1
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

-- Mathlib.Topology.ContinuousFunction.Bounded
Error: ./Mathlib/Topology/ContinuousFunction/Bounded.lean:917:1: error: BoundedContinuousFunction.norm_normComp.{u, v} LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  Nontrivial (BoundedContinuousFunction α ℝ)
(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: The process '/usr/bin/env' failed with exit code 2
Remove matcher: gcc

[MohanadAhmed]

Any thoughts as to what could be the source of these problems in the linter in CI

[Kevin Buzzard]

I had the same issue with exactly those three Fin simp lemmas in #5959. Same error. Note that the instance which it's failing to synthesize doesn't exist because the class is not covariant with respect to those operations.

I fixed the issue with the rather brutal approach of just removing @[simp] from the lemmas in question; mathlib still compiled, so I think the lemmas are somehow bad in some way but we're never using them anyway (perhaps because they never fire).

I can't comment on the Mathlib.Topology.ContinuousFunction.Bounded lemma. I was messing around with instance priorities in some low-level file so weird failures were perhaps not surprising for me. I'm a little more surprised that your work is causing this issue. It might be worthwhile tracking down what the heck is going on with these failures.

By the way, on a pretty much unrelated issue, your PR is essentially unmergeable because it is so large. We recommend PRs of <= 300 lines, and for newcomers we prefer <= 150 lines of changes because we're fussy about code style. I conjecture that your PR will just sit going stale for a long time in its current state. Can you break off e.g. just one file and PR that instead?

[MohanadAhmed]

Kevin Buzzard said:

I can't comment on the Mathlib.Topology.ContinuousFunction.Bounded lemma. I was messing around with instance priorities in some low-level file so weird failures were perhaps not surprising for me. I'm a little more surprised that your work is causing this issue. It might be worthwhile tracking down what the heck is going on with these failures.

Any suggestions on how to do this tracking down? Is there some verbose mode for the linters to emit more information ?

By the way I notice the simps in these locations are just simps, i.e. not squeezed simps or (lean 4 simp?). Is there any thought behind putting them as simp without the concrete lemmas? Is there a problem with me doing simp? and replacing with simp only [... relevant lemmas]

Kevin Buzzard said:

By the way, on a pretty much unrelated issue, your PR is essentially unmergeable because it is so large. We recommend PRs of <= 300 lines, and for newcomers we prefer <= 150 lines of changes because we're fussy about code style. I conjecture that your PR will just sit going stale for a long time in its current state. Can you break off e.g. just one file and PR that instead?

Ouch. That is going to be a psychologically draining process!
On that note are there any contribution guidelines and style guides somewhere? They might help me (and others) avoid some annoying painful mistakes

[MohanadAhmed]

Do the style guides for mathlib3 still apply?

[Eric Wieser]

Not the ones about whitespace, at least not without modification

[Alex J. Best]

Well just looking at your project it seems some of the files make sense individually and PRing those one by one would be a good start.
The style guide for mathlib3 is mostly still in effect, but with some changes of course. The spacing around arguments and in terms looks a bit strange in your code, if you look at the code in mathlib4 you can find many examples of how it should be. Maybe if you open one file as a PR first we can give you some good line by line feedback (like RankMulIsUnit.lean does that really depend on IsROrCStarOrderedRing?)

[MohanadAhmed]

Alex J. Best said:

Well just looking at your project it seems some of the files make sense individually and PRing those one by one would be a good start.
The style guide for mathlib3 is mostly still in effect, but with some changes of course. The spacing around arguments and in terms looks a bit strange in your code, if you look at the code in mathlib4 you can find many examples of how it should be. Maybe if you open one file as a PR first we can give you some good line by line feedback (like RankMulIsUnit.lean does that really depend on IsROrCStarOrderedRing?)

OK on that last point here is #6051. You are right it does not depend on IsROrCStarOrderedRing.

[Scott Morrison]

A few of us have now left comments on that first PR. Please make sure to also apply the suggestions to your later files, where they generalise.

[Kevin Buzzard]

Another couple of things to add about this process:

Ouch. That is going to be a psychologically draining process!

Don't think like that! The work is a useful addition to mathlib (you convinced me of this in Leiden!) and will get there; it's just that the process of getting it there isn't "dump it all in one PR", it's "write it all" (which you did) "and then make several PRs" (which you're now doing). In fact the process you went through (writing a bunch of code in one batch and then PRing it in chunks) is normal for projects of this size.

On that note are there any contribution guidelines and style guides somewhere? They might help me (and others) avoid some annoying painful mistakes

I would "learn on the job", given where we are now. Make the PRs, small chunks at first, and you'll get feedback from the community which will just show you by example the kind of guidelines which have been figured out by the community.