instance fails_quickly

Stream: general

[Yakov Pechersky]

In #9891, I am refactoring bounds out of the lattice hierarchy. Everything builds, but I am hitting the fails_quickly linter on:

instance nat.subtype.order_bot (s : set ℕ) [decidable_pred (∈ s)] [h : nonempty s] :
  order_bot s :=
{ bot := ⟨nat.find (nonempty_subtype.1 h), nat.find_spec (nonempty_subtype.1 h)⟩,
  bot_le := λ x, nat.find_min' _ x.2 }

I haven't been able to root-cause analyze this -- adding all sorts of shortcut instances for nat didn't seem to help. Can a TC expert help here please?

[Yakov Pechersky]

I see in nolints that we have apply_nolint nat.subtype.semilattice_sup_bot fails_quickly. Should I also nolint my new instance?

[Floris van Doorn]

Did you read the error message that the linter gave? Were the instructions unclear on how to debug the issue?

This linter won't be happy by adding shortcut instances, it is a linter to find loops. In this case, the loop is caused by these three instances:

#check @order_bot.to_has_bot
#check @has_bot_nonempty
#check @nat.subtype.order_bot

nat.subtype.order_bot seems like a bad candidate for a global instance.
That said, it makes sense to not fix the issue in your PR, as you're not creating the problem, just slightly changing it.

[Eric Wieser]

(docs#nat.subtype.semilattice_sup_bot)

[Yaël Dillies]

Floris van Doorn said:

Did you read the error message that the linter gave? Were the instructions unclear on how to debug the issue?

#9123 and #10011 are both stuck because of fails_quickly. The instructions are clear (although I spent a day finding how to run mk_all) but I just don't know how to interpret the TC inference trace. I couldn't see anything visibly wrong.

[Floris van Doorn]

I can write a library note (or blog post?) with instructions how to debug type class problems.

[Yaël Dillies]

Yes please! I would love to have that.

[Floris van Doorn]

#9123 seems to be stuck on building mathlib?

[Yaël Dillies]

I can fix quickly. It rotted a bit.

[Johan Commelin]

In LTE we have the following:

@[nolint unused_arguments]
def rescale (N : ℝ≥0) (V : Type*) := V

namespace rescale

variables {N : ℝ≥0} {V : Type*}

instance [i : add_comm_monoid V] : add_comm_monoid (rescale N V) := i
instance [i : add_comm_group V] : add_comm_group (rescale N V) := i

end rescale

The fails_quickly linter complains. Why is this bad? This shouldn't create a loop, right?

[Eric Rodriguez]

can you give an mwe? this doesn't seem to fail for me:

image.png

[Johan Commelin]

For context, I'm trying to clean up

rg -B1 quickly scripts/nolints.txt
103--- for_mathlib/simplicial/iso.lean
104:apply_nolint category_theory.simplicial_object.is_iso_of fails_quickly
--
129--- locally_constant/Vhat.lean
130:apply_nolint SemiNormedGroup.normed_with_aut_LCC fails_quickly
131:apply_nolint SemiNormedGroup.normed_with_aut_LocallyConstant fails_quickly
--
171-apply_nolint LC.T_inv unused_arguments
172:apply_nolint LC.obj.normed_with_aut fails_quickly
--
174-apply_nolint LCFP.Tinv unused_arguments
175:apply_nolint LCFP.obj.normed_with_aut fails_quickly
--
202--- rescale/basic.lean
203:apply_nolint rescale.add_comm_group fails_quickly
204:apply_nolint rescale.add_comm_monoid fails_quickly
--
209--- rescale/pseudo_normed_group.lean
210:apply_nolint rescale.comphaus_filtered_pseudo_normed_group fails_quickly
211:apply_nolint rescale.profinitely_filtered_pseudo_normed_group fails_quickly
212:apply_nolint rescale.profinitely_filtered_pseudo_normed_group_with_Tinv fails_quickly
213:apply_nolint rescale.pseudo_normed_group fails_quickly

[Johan Commelin]

In the hope that it will have a positive effect on the speed of the project

[Johan Commelin]

@Eric Rodriguez I don't have an mwe, just a complaining linter

[Eric Rodriguez]

and I'm trying to say that the linter doesn't fail for me

[Eric Rodriguez]

or does fails_quickly not run with #lint?

[Johan Commelin]

Je ne sais pas

[Eric Rodriguez]

it does seem to run as I can run #lint fails_quickly. what's the imports in the LTE file?

[Johan Commelin]

import polyhedral_lattice.basic

which is part of LTE.

[Eric Rodriguez]

even running it on LTE it seems to work fine: image.png maybe just try remove the nolint and see if it shouts? seems to be fixed as far as I can tell..

[Johan Commelin]

But it doesn't make sense to me that this no_lint would influence the fails_quickly linter

[Eric Rodriguez]

urgh, I'm trying to look into this but ./scripts/get-cache.sh seems to say that the LTE cache isn't up, even though Github seems to be done

[Johan Commelin]

@Floris van Doorn Do you have some time to debug this in LTE? I really don't know what is wrong with the instances that are currently being flagged.

[Eric Rodriguez]

I managed to build it by hand, and try to lint it by hand, and I think the nolints are spurious, I think you can remove them and there won't be linting errors

[Floris van Doorn]

I forgot to respond here. Can I still be useful here? What failure do you want me to look at?
The fails_quickly linter is a global linter, so it's possible that it succeeds on a declaration, but then fails if you import more files. Those files could have instances that loop or take a very long time to fail.

[Floris van Doorn]

For rescale: the instances you posted are no problem, but there is likely another instance (possibly having nothing to do with rescale) that is an issue.

[Floris van Doorn]

I'm unable to download the lean-liquid oleans with scripts/get-cache.sh, so it's hard for me to reproduce locally.