Zulip Chat Archive
Stream: general
Topic: instance max depth
Sebastien Gouezel (May 05 2020 at 17:46):
What has happened to mathlib? I am revisiting an old file (on smooth functions between smooth manifolds, with normed spaces and smooth functions and a bunch of complicated stuff). In this file, written a few months ago, there was a line set_option class.instance_max_depth 150 (and this was really needed, 100 was not enough since earlier in the file it was set to 100 and I had to increase it). It turns out that this line can now be removed and, even better, setting the max depth to 10 works fine! (9 is not enough, though :-)
Sebastien Gouezel (May 05 2020 at 17:50):
Just for fun, I started commenting the set_option class.instance_max_depth in random files, and it seems to work all the time!
Kevin Buzzard (May 05 2020 at 18:00):
Open a bug report!
Sebastien Gouezel (May 05 2020 at 18:07):
I have commented all of them and mathlib builds without one single error!
Kenny Lau (May 05 2020 at 18:19):
what changed? I remember doing stuff with tensor products and having to set it to 37
Sebastien Gouezel (May 05 2020 at 18:40):
I had to set it to 360 in a file on multilinear maps. Now 11 is enough... In between, there was #1724 and related work on a priority linter for instances (and possibly other stuff that had some influence on this and that I didn't notice).
Kevin Buzzard (May 05 2020 at 18:43):
Can you also prove false?
Reid Barton (May 05 2020 at 18:45):
The default is something like 20, right?
Reid Barton (May 05 2020 at 18:46):
This is nice to hear because that #1724 also needed to raise some other instance_max_depths, I think
Reid Barton (May 05 2020 at 18:47):
because of the perhaps counterintuitive definition of "depth" in this context
Sebastien Gouezel (May 05 2020 at 18:47):
The default is 32.
Sebastien Gouezel (May 05 2020 at 19:14):
Patrick Massot (May 05 2020 at 19:33):
Amazing...
Patrick Massot (May 05 2020 at 19:34):
Recently I was worried by all those changes without any performance impact study. But that PR makes me feel much better. Surely this max_depth improvement should come with a speed improvement.
Reid Barton (May 05 2020 at 19:41):
#1724 was supposed to make instance lookup faster... which apparently means it would actually have made it a bit slower.
Johan Commelin (May 05 2020 at 19:47):
What do you mean?
Johan Commelin (May 05 2020 at 19:47):
Why is it actually slower?
Patrick Massot (May 05 2020 at 19:48):
I think he simply refer to the general trend of effect inversion
Last updated: Dec 20 2023 at 11:08 UTC