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):

#2608

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