performance regression in nightly-2021-08-04?

Stream: lean4

[David Renshaw]

I'm noticing that some of my code got noticeably slower in nightly-2021-08-04. In particular,

[David Renshaw]

https://github.com/dwrensha/lean4-maze/blob/5121db6df78c6ab4d26afcfae77f62172dade1a8/Maze.lean#L392-L396

[David Renshaw]

When I move my cursor through that tactic proof in emacs, it now seems to take about 2 seconds for the goal view to update.

[David Renshaw]

Before I updated to nightly-2021-08-04, it was more like a half second.

[David Renshaw]

nightly-2021-08-03 does not seem to have this problem, so it seems that something changed in the last day or so to cause this

[Daniel Selsam]

can you pls try setting set_option pp.analyze false?

[David Renshaw]

ah, that makes things snappy once again!

[Daniel Selsam]

It got merged yesterday, and it hasn't been perf-stress-tested yet. I will investigate.

[David Renshaw]

https://github.com/leanprover/lean4/pull/575

[David Renshaw]

(^ link to what seems to be the relevant pull request, for context)

[Daniel Selsam]

@David Renshaw I issued a PR that speeds your example up a good deal (https://github.com/leanprover/lean4/pull/605). There is still some overhead though with pp.analyze true, since the analyzer still preprocesses your big terms even though its annotations are ignored by your custom delaborator. There is probably more relatively low hanging fruit to optimize the analyzer further, but note that your example is the epitome of one where you don't want pp.analyze to run. It is not clear yet whether it is appropriate for pp.analyze to be the default, but I think your example is "advanced" enough already such that needing to explicitly disable it for best performance would be reasonable.