Debounce refreshes of the info-mode #11
Conversation
lean4-info.el
Outdated
| ;; That is, we maintain the timing invariant that the time lean4-info-buffer-redisplay | ||
| ;; is invoked is at least (debounce-interval-seconds) after the last redisplay request. |
There was a problem hiding this comment.
That logic looks kind of wrong to me; we should refresh at most duration-seconds (you used three different names btw) after any request. Otherwise with sufficiently frequent requests such as from building dependent files, we would not show anything at all for quite a while.
There was a problem hiding this comment.
@Kha Ah, I didn't know that there are cases where we get many requests. I was under the impression that a single request is generated per user movement command.
The current code "delays" rendering by duration-seconds, to wait for more changes that might come in. Do you suggest we add another timer (say, debounce-upper-bound-duration) which is a somewhat long duration such as 0.5sec? This is so that in the case where we get a large sequence of requests, we do render some information once in a while.
There was a problem hiding this comment.
Hmm, do you think one refresh every 0.1s is too often? Because in that case one timer would suffice. But I'm okay with either solution.
|
@Kha To check I understand commit conventions, I should call this |
Yeah, looks appropriate. |
This prevents emacs from lagging when scrolling
through a file that has many `#print` messages, or when
there are many errors.
;; Debouncing
;; ~~~~~~~~~~~
;; We want to update the Lean4 info buffer as seldom as possible,
;; since magit-section is slow at rendering. We
;; wait a small duration ('debounce-delay-sec') when we get a
;; redisplay request, to see if there is a redisplay request in the
;; future that invalidates the current request (debouncing).
;; Pictorially,
;; (a) One request:
;; --r1
;; --r1.wait
;; ----------r1.render
;; (b) Two requests in quick succession:
;; --r1
;; --r1.wait
;; --------r2(cancel r1.wait)
;; --------r2.wait
;; ---------------r2.render
;; (c) Two requests, not in succession:
;; --r1
;; --r1.wait
;; ---------r1.render
;; ------------------r2
;; ------------------r2.wait
;; -------------------------r2.render
;; This delaying can lead to a pathological case where we continually
;; stagger, while not rendering anything:
;; --r1
;; --r1.wait
;; --------r2(cancel r1.wait)
;; --------r2.wait
;; --------------r3(cancel r2.wait)
;; ---------------r3.wait
;; ---------------------r4(cancel r3.wait)
;; ---------------------...
;; We prevent this pathological case by keeping track of when
;; when we began debouncing in 'lean4-info-buffer-debounce-begin-time'.
;; If we have been debouncing for longer than
;; 'lean4-info-buffer-debounce-upper-bound-sec', then we
;; immediately write instead of debouncing;
;; 'max-debounces' times. Upon trying to stagger the
;; 'max-debounces'th request, we immediately render:
;; begin-time:nil----t0----------------nil-------
;; -------r1 |
;; -------r1.wait |
;; -------|-----r2(cancel r1.wait)
;; -------|-----r2.wait |
;; -------|-----------r3(cancel r2.wait)
;; -------|-----------r3.wait
;; -------|-----------------r4(cancel r3.wait)
;; -------|-----------------|
;; >-----------------<
;; >longer than 'debounce-upper-bound-sec'<
;; -------------------------r4.render(FORCED)
bollu
force-pushed
the
debounce-info-mode-refresh
branch
from
9a7749d
to
e6738ea
Compare
|
@Kha I request a review, as I've changed the rendering code to add an upper bound to the debounce. |
I see that didn't work out 😅 . But the code looks good, thanks! |
|
Yes, because I fixed it in the merge |
This prevents emacs from lagging when scrolling
through a file that has many
#printmessages, or whenthere are many errors.
This was discovered when writing this lean file with many errors.
The profiler output (use
M-x profiler-find-profileto view is below:The debounce implementation was taken from lsp-lens