## Stream: new members

### Topic: Maximum Class-instance resolution depth has been exceeded

#### Rocky Kamen-Rubio (Feb 07 2020 at 22:21):

Does anyone know anything about this error message? Can't seem to find anything about it on previous threads or in the tutorials/manuals about lean. Thanks! [Screen-Shot-2020-02-07-at-5.19.02-PM.png]

#### Rocky Kamen-Rubio (Feb 07 2020 at 22:22):

Does anyone know anything about this error message? Can't seem to find anything about it on previous threads or in the tutorials/manuals about lean. Thanks!
Screen-Shot-2020-02-07-at-5.19.02-PM.png

#### Ryan Lahfa (Feb 07 2020 at 22:30):

Does anyone know anything about this error message? Can't seem to find anything about it on previous threads or in the tutorials/manuals about lean. Thanks!
Screen-Shot-2020-02-07-at-5.19.02-PM.png

Have you tried to do a set_option class.instance.max_depth 150000 and see if it creates a timeout (?). Otherwise, you can also trace the class instances resolution and try to find what Lean is trying to instantiate.

#### Bryan Gin-ge Chen (Feb 07 2020 at 23:02):

What are you trying to do exactly?

By the way, if you paste your code here (or a "minimum working example"), we can more easily figure out what's going on.

#### Rocky Kamen-Rubio (Feb 08 2020 at 19:09):

I tried adding this line to the top of my code but it's giving me this error. Screen-Shot-2020-02-08-at-2.08.45-PM.png

#### Bryan Gin-ge Chen (Feb 08 2020 at 19:10):

There was a typo, it should be set_option class.instance_max_depth

#### Rocky Kamen-Rubio (Feb 08 2020 at 19:11):

You're right. The whole thing is working correctly now. Thanks you!!!

#### Bryan Gin-ge Chen (Feb 08 2020 at 19:11):

I think the VS Code extension's autocomplete menu should show the correct option while you're typing it.

#### Ryan Lahfa (Feb 08 2020 at 19:28):

You're right. The whole thing is working correctly now. Thanks you!!!

The idea of upping the max depth is only a temporary fix IMHO, you should try to see what's taking so long and see if you can shortcut the search, otherwise, you might encounter timeouts from Lean

#### Kevin Buzzard (Feb 08 2020 at 19:39):

Sometimes a comment from an expert (perhaps fiddling with a typeclass parameter) can make the end user experience much better. Using Lean with lag is never fun.

#### Sebastien Gouezel (Feb 08 2020 at 19:40):

Sometimes math is complicated, and you have to accept it. I am currently in a file where the max depth is set at 370, and this is not a problem at all.

#### Ryan Lahfa (Feb 08 2020 at 19:44):

Sometimes math is complicated, and you have to accept it. I am currently in a file where the max depth is set at 370, and this is not a problem at all.

Though, isn't there some way to always shortcut the instance resolution and provide the instance ourselves?

#### Kevin Buzzard (Feb 08 2020 at 19:44):

In Lean 4 the system will be completely different and, hopefully, much better. The computer scientists listened to the concerns of mathematicians.

#### Ryan Lahfa (Feb 08 2020 at 19:47):

In Lean 4 the system will be completely different and, hopefully, much better. The computer scientists listened to the concerns of mathematicians.

But ; is Lean 4 compatible with the current mathlib… :D ?

#### Kevin Buzzard (Feb 08 2020 at 19:54):

yeah they're going to write a regexp as soon as the tactic framework is ready.

Last updated: May 12 2021 at 23:13 UTC