## Stream: new members

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

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

Screen-Shot-2020-02-07-at-5.19.02-PM.png

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

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
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 1, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.4273618459701538, "perplexity": 3780.978141758562}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 20, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2021-21/segments/1620243991413.30/warc/CC-MAIN-20210512224016-20210513014016-00411.warc.gz"}