Zulip Chat Archive

Stream: mathlib4

Topic: Data.SetLike.Fintype mathlib4#1727

Shreyas Srinivas (Jan 20 2023 at 15:50):

There are no errors left and locally the linter did not say anything was wrong:
However I get the simpNF linter error again : https://github.com/leanprover-community/mathlib4/actions/runs/3969088609/jobs/6803103542

Shreyas Srinivas (Jan 20 2023 at 15:51):

There are only two instances in this file and no theorems. So I am not sure where the issue is

Shreyas Srinivas (Jan 20 2023 at 15:53):

The CI linter gives this error message:

-- Mathlib.Data.Fintype.Basic
#check Fintype.univ_ofSubsingleton.{u_1} /- LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
  Fintype α
(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

Kevin Buzzard (Jan 20 2023 at 15:54):

The error it's flagging is in a completely different file to the one you're PRing, right? So somehow the instance you're adding has made type class inference go bad. Try adding it in the relevant file and experimenting there, turn the instance trace on etc. There might be a simple explanation.

Shreyas Srinivas (Jan 20 2023 at 15:57):

okay. I'll try that

Shreyas Srinivas (Jan 20 2023 at 16:25):

I can't get the linter to throw errors locally.

Last updated: Dec 20 2023 at 11:08 UTC