Zulip Chat Archive

Stream: new members

Topic: Maximum Class-instance resolution depth has been exceeded


view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Feb 08 2020 at 19:10):

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

view this post on Zulip Rocky Kamen-Rubio (Feb 08 2020 at 19:11):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip 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