Deterministic timeout after mathlib upgrade

Stream: new members

[Antoine Chambert-Loir]

I have done a massive upgrade of mathlib yesterday on branch#acl-Wielandt, and many things that used to work ended up with a Deterministic timeout. I can't understand what happened.
I could arrange some stuff by splitting it into smaller lemmas, but now I'm stuck at the 3-line proof of is_maximal_stab'_temp (see https://github.com/leanprover-community/mathlib/blob/ba7beaa6083cacd48a6878a8bd7d25464c285df6/acl-sandbox/group_theory/jordan/alternating-iwasawa.lean#L140) can't compile. Unfortunately, I don't see how to do a MWE.

This stuff used a lot of fintype. May this deterministic timeout be related to the introduction of finite ?

[Yaël Dillies]

I can give it a try.

[Antoine Chambert-Loir]

Thank you.

[Antoine Chambert-Loir]

(I am willing to use finite, if needed, but a lot of stuff still relies on fintype…)

[Antoine Chambert-Loir]

Yaël Dillies said:

I can give it a try.

I haven't the impression to have done anything, but reboot the computer, and it seems to work better… Sorcery…

[Antoine Chambert-Loir]

Problem solved, although it will require a better understanding of what happens.
It was apparently due to Lean being confused between an explicit instance of [decidable_eq α] and another one computed via classical.

(The whole theory of permutations requires decidable_eq α on the type α, and this seems to be incompatible with what the classical Linter urges me to do…)

[Kevin Buzzard]

Never open_locale classical, it's mostly deprecated.

[Antoine Chambert-Loir]

Thanks for the advice!

[Jeremy Avigad]

Never open_locale classical, it's mostly deprecated.

Has something changed recently to make it unnecessary, e.g. when dealing with lists or finsets of noncomputable objects?

[Yaël Dillies]

I wouldn't be as dogmatic as Kevin, but recently Eric fixed the priorities of the classical instances so that classical and open_locale classical aren't synonym of rapid death. In particular, it's now much easier to mix decidable and classical stuff, so open_locale classical is less useful (in the sense that it was a way to avoid that mixing).