fix: infoview performance

[mhuisi]

This PR addresses sub-optimal InfoView performance with large terms (e.g. with pp.maxSteps 5000).

The results are as follows:

• Moving the text cursor to a proof goal with a pp.maxSteps 5000 term:
  • Higher spec: ~16s (before) => ~600ms (after)
  • Lower spec: ~52s (before) => ~1s (after)
• Hovering over the top level subexpression of a proof goal with a pp.maxSteps 5000 term:
  • Higher spec: ~14s (before) => ~800ms (after)
  • Lower spec: ~76s (before) => ~1.2s (after)
• Moving the mouse away from the top level subexpression after the hover has rendered:
  • Higher spec: ~9s (before) => ~800ms (after)
  • Lower spec: ~56s (before) => ~1s (after)

I used the following benchmark with the "Messages" section collapsed:

opaque myAuxiliaryFunction : Nat → Nat → Nat
opaque anotherHelper : Nat → Nat

def f (m : Nat) : Nat → Nat
  | 0   => anotherHelper m
  | n+1 => myAuxiliaryFunction (f (anotherHelper m) n) (f (myAuxiliaryFunction m (anotherHelper m)) n)

set_option pp.maxSteps 5000

example : f a 10 = b := by
  simp [f]

Optimization techniques

1. The size of the produced DOM is important. Our subexpression hot-loop would produce five HTML elements for every subexpression because it was composed of several nicely reusable React components, each of which came with their own HTML element. This PR refactors these components to use custom React hooks instead, shifting the responsibility of correctly setting up the HTML element to the caller and significantly reducing the size of the produced DOM in the process by accumulating all subexpression-related logic in a single span. This optimization yielded a performance improvement that was roughly directly proportional to the reduced DOM size (i.e. ~5x).
2. Re-renders in the subexpression hot-loop are expensive. Specifically, after reducing the size of the DOM, we would render the whole subexpression DOM three times in total [1]. These re-renders were eliminated as follows:
   • Setting state in an effect will trigger a re-render, even if the state has not changed from its initial value. We use effects in several places to reset state when some variable changes. Most of these cases are cheap re-renders, but one of them resulted in the whole subexpression DOM being re-rendered. This was resolved by using keys to reset all state when variables change.
   • Storing DOM references in state will trigger a re-render. We do this in the subexpression hot-loop to re-render the tooltip when its anchor node changes. The re-render induced by this usage of state was eliminated by lazily setting the state corresponding to the anchor node when the tooltip is displayed, as the tooltip will only need this state when it is being displayed anyways.
3. Where possible, rendering invisible content should be avoided. When working with large terms, users are likely to collapse the "Messages" section so that they do not see the same large term twice, but we would still render the second large term in the "Messages" section even when it was collapsed. This was easy to fix with some additional conditional rendering.
4. Adding lots of event handlers to document from effects is extremely slow. At one point, these effects took up 7/8 of the rendering time in my profiling. We used to do this in two cases:
   • onKeyUp and onKeyDown listeners in SelectableLocation to listen for Ctrl inputs. Instead of adding these event listeners for every subexpression, we now only add them when the corresponding span is being hovered over. This significantly reduces the cost of these event handlers.
   • useOnClickOutside listeners in WithTooltipOnHover to collapse the tooltip when clicking outside of the tooltip. Instead of adding these event listeners for every subexpression, we now only add them for subexpressions with tooltips. This significantly reduces the cost of these event handlers.
5. Memoization can be helpful to avoid redundant re-renders. Before, we had no memoization for individual subexpression components, which lead to several redundant re-renders of the whole tree when hovering over a term, despite the fact that this only adds a CSS class and a tooltip child for that subexpression. Memoizing these components avoids this.

[1] After reducing the size of the DOM, the timings of these re-renders were roughly as follows on the lower spec machine (measured at pp.maxSteps 1000):

• First render: 227.8ms render, 16.8ms layout effects, 140.3ms passive effects
• Second render (immediate re-render): 151.1ms render, 0ms layout effects, 33.6ms passive effects
• Third render: 144.1ms render, 0ms layout effects, 54.4ms passive effects

(As an aside: I'm not sure how to explain that computing the global event handler effects was so much cheaper here than what I profiled later. This benchmark was before eliminating expensive effects and redundant re-renders, whereas the situation where 7/8 of the rendering time was spent on these effects occurred after eliminating the redundant re-renders. In any case, optimizing the expensive effects solved this issue.)

Functional changes

This PR makes a couple of minor adjustments:

• The hover selection now does not use an animation anymore. I found this to be irritating myself when moving my mouse across an expression in the InfoTree, since it would lead to the expression blinking. I personally find the hover highlighting to be much nicer without the animation.
• For simplicity, I also removed the rounded corners of the selection (which I was only barely able to notice once I was aware of it) since this allows us to get rid of the highlightable class entirely.
• The colors of hover and selection highlighting would overlap and mix. I removed this since the resulting contrast became difficult to distinguish so that hover highlighting always takes precedence over selection highlighting.

Other lessons learned

• We can profile the InfoView using npx react-devtools by adding <script src="http://localhost:8097"></script> to the InfoView head. It can also help detect the cause of a re-render. If the developer tools are launched after the InfoView, you may need to run Reload Window once before the developer tools start working.
• The developer tools are relatively unstable. Before this PR, the largest I could profile was pp.maxTerms 50 or so before the developer tools would automatically disconnect before producing a profile. For some reason, inspecting the InteractiveCodeTag component to find out which hook numbers from the profiler correspond to which actual hooks consistently leads to a timeout. It should also be possible to manually assign hook names using useDebugValue, but in the end I just ended up deleting hook after hook to figure out which ones were causing a re-render.
• The upper bound for render performance is roughly another factor 2. I determined this by removing all fancy logic from the subexpression hot loop, keeping only a single raw span for every subexpression and then profiling that. I believe that it's certainly still possible to optimize the InfoView a bit (e.g. on the higher spec machine, you can probably eliminate another 100ms that go into passive effects by attempting to replace those effects with other mechanisms), but it likely can't be much more significant than by a factor of 2.

[mhuisi]

@Vtec234

Btw, the selection highlight on parenthesized terms seems to appear twice (not a regression, it was like that before). Do you have a sense of whether the fix is easy, since you're already touching that code?

This is because both a parenthesized subexpression (foo) and its subexpression foo have the same subexpression position. I made a draft PR to change this at leanprover/lean4#4786, since it would also help cut down the size of the DOM further. Do you see any obvious issues with this?

[mhuisi]

I'm afraid that this version is slowing down the InfoView by 150ms again. I'll look into why.

[mhuisi]

I suspect the reason was that memoizing in the recursion itself is inhibiting some React optimization. For an experiment, I also tried replacing the recursive component (without memoization) with a recursive function that builds the component, but this did not yield a speed-up.

For some reason I cannot explain, this version is sometimes still 50ms slower than the version at 433fa89 with genericMemo. I don't think it's the extra component wrapper because I tried to eliminate that and it was still slower, whereas the version with genericMemo consistently seems to be a bit faster.

[Vtec234]

this version is sometimes still 50ms slower than the version at 433fa89 with genericMemo

Hm, there have been other changes (ctrl-related) since that commit. Does a direct comparison with those included result in any difference?

[mhuisi]

No, I double-checked that this is not caused by the new effects. In any case, I think it's fine to go ahead even if it is (in my profiler measurements) sometimes a tiny bit slower. It's not clear whether these kinds of smaller fluctuations when profiling things in debug mode will appear in production, either.