fails_quickly

Stream: general

[Yaël Dillies]

#9123 is failing at the moment because @Scott Morrison's linter fails_quickly found a problem with docs#pi.has_scalar: https://github.com/leanprover-community/mathlib/runs/3665752864

I recreated the typeclass search here, as indicated:

import all

set_option trace.class_instances true

example {I : Type*} {f : I → Type*} {α : Type*} : has_scalar α (Π (i : I), f i) :=
by apply_instance

I must say I have no idea what to look for in the TC trace. module.to_distrib_mul_action_with_zero appears several times, but it doesn't seem to be looping. Could it just be that fails_quickly is a bit too severe?

[Eric Wieser]

(note to others: this problem exists only in the branch of #9123 which adds distrib_mul_action_with_zero)

[Anne Baanen]

Does that example time out or work? If it works, increasing the time limit in fails_quickly is probably OK.

[Scott Morrison]

I think it's @Floris van Doorn's linter, btw, not mine.

[Yaël Dillies]

Whoops, yup, got that wrong.

[Floris van Doorn]

(3) What error do you get?
(3a) If the error is "tactic.mk_instance failed to generate instance",
there might be nothing wrong. But it might take unreasonably long for the type-class inference to
fail. Check the trace to see if type-class inference takes any unnecessary long unexpected turns.
If not, feel free to increase the value in the definition of the linter fails_quickly.
(3b) If the error is "maximum class-instance resolution depth has been reached" there is almost
certainly a loop in the type-class inference. Find which instance causes the type-class inference to
go astray, and fix that instance.

[Anne Baanen]

I believe the new classes and instances in #16123 will require a bump of the fails_quickly linter timeout. In particular, docs#prod.nonempty and docs#pi.has_smul' trigger searches through a huge part of the algebraic hierarchy and I don't see a straightforward way to avoid that, nor do the extra instances change the search space in interesting ways beyond extending it a bit. So I think we should bump the fails_quickly timeout to something like 27500 or 30000 heartbeats.

[Anne Baanen]

If there's no objection in the next couple of hours I'll assume it's fine to bump the timeout.