Zulip Chat Archive

Stream: new members

Topic: maximum class-instance resolution depth has been reached


view this post on Zulip Kris Brown (Jun 18 2020 at 01:37):

I'm trying to prove a theorem related to permutations of finite sets. At the beginning (trying to define a predicate on permutations to assert they are cyclic) and running into an issue that I don't know how to debug. The error (which is on the very last x of the very last definition) is "maximum class-instance resolution depth has been reached". I tried restarting Lean, setting class.instance_max_depth 1000, and I turned on trace.class_instances, though that spits out something extremely long that I can't make sense of. How should I approach this error, as a beginner?

import data.equiv.basic
import data.finset

open equiv -- "perm x" is "equiv x x" AKA "x ≃ x"
open nat

-- Repeat a binary function n times
def rep {α : Type*} :   (α  α)  α  α
 | 0 _ x := x
 | (succ n) f x := f (rep n f x)

-- Π (n : ℕ), perm (fin n) → fin n → fin n
#check λ (n:) (p: perm (fin n)) (x: fin n),
        rep n p.to_fun x

-- Predicate for a permutation on a finite set to be cyclic
def cyclic {n : } (p : perm (fin n)) :=
     x : fin n, rep n p.to_fun x = x

view this post on Zulip Jalex Stark (Jun 18 2020 at 01:38):

put a newline after your backticks tog et syntax highlighting

view this post on Zulip Jalex Stark (Jun 18 2020 at 01:39):

i don't get any error

view this post on Zulip Jalex Stark (Jun 18 2020 at 01:41):

you should change your instance_max_depth back to default, this may cause slowdowns for you later

view this post on Zulip Kris Brown (Jun 18 2020 at 01:42):

Thanks! and that's interesting; I'm using Lean 3.4.2 - are there any candidates for settings I could change to match your setup?

view this post on Zulip Jalex Stark (Jun 18 2020 at 01:43):

around here the suggestion is to use that latest leanprover-community build with the latest mathlib

view this post on Zulip Jalex Stark (Jun 18 2020 at 01:43):

managing that installation is easy with the leanproject tool

view this post on Zulip Jalex Stark (Jun 18 2020 at 01:44):

https://leanprover-community.github.io/get_started.html

view this post on Zulip Jalex Stark (Jun 18 2020 at 01:46):

you can use the lean web editor in the meantime

view this post on Zulip Jalex Stark (Jun 18 2020 at 01:46):

web editor

view this post on Zulip Scott Morrison (Jun 18 2020 at 01:52):

3.4.2 is pretty old by now (it's the last "official" release before switching to community development), and in particular is missing lots of nice improvements to the typeclass search algorithm.

view this post on Zulip Kris Brown (Jun 18 2020 at 03:46):

Thanks everyone, upgrading fixed this!


Last updated: May 12 2021 at 03:23 UTC