Maximum Class-instance resolution depth has been exceeded

Stream: new members

[Rocky Kamen-Rubio]

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]

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]

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]

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]

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]

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

[Rocky Kamen-Rubio]

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

[Bryan Gin-ge Chen]

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

[Ryan Lahfa]

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]

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]

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]

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]

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

[Ryan Lahfa]

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]

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