Zulip Chat Archive

Stream: new members

Topic: Deterministic timeout after mathlib upgrade


Antoine Chambert-Loir (Aug 25 2022 at 06:52):

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 (Aug 25 2022 at 07:14):

I can give it a try.

Antoine Chambert-Loir (Aug 25 2022 at 07:38):

Thank you.

Antoine Chambert-Loir (Aug 25 2022 at 07:39):

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

Antoine Chambert-Loir (Aug 25 2022 at 11:30):

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 (Aug 29 2022 at 15:24):

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 (Aug 29 2022 at 16:38):

Never open_locale classical, it's mostly deprecated.

Antoine Chambert-Loir (Aug 30 2022 at 07:10):

Thanks for the advice!

Jeremy Avigad (Aug 30 2022 at 11:52):

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 (Aug 30 2022 at 11:54):

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).


Last updated: Dec 20 2023 at 11:08 UTC