feat: respond to info view requests as soon as relevant tactic has finished execution #4727
Conversation
| let nextLine := { line := pos.line + 1, character := 0 } | ||
| let t := doc.cmdSnaps.waitUntil fun snap => filemap.lspPosToUtf8Pos nextLine ≤ snap.endPos | ||
| mapTask t fun (snaps, _) => do | ||
| let some snap := snaps.getLast? | ||
| | return ⟨∅⟩ | ||
| runTermElabM snap do | ||
| mapTask (findInfoTreeAtPos doc <| filemap.lspPosToUtf8Pos pos) fun | ||
| | some infoTree@(.context (.commandCtx cc) _) => | ||
| ContextInfo.runMetaM { cc with } {} do |
There was a problem hiding this comment.
@Vtec234 Could you explain why this request handler used a very different waiting/position searching logic from other requests and how it should behave under incremental tactic execution?
There was a problem hiding this comment.
Am I reading correctly that the only difference is the use of waitUntil versus waitFind? (which is what withWaitFindSnap uses)? I honestly don't remember, but my guess would be that this is because nextLine need not be a valid position in the file (it might be one more than the last line), so if you use waitFind? and ask for a snapshot whose endPos is at least nextLine, you might get none. But waitUntil will give you the entire list in case nothing matching the predicate is found. This is correct as it'll give us the last snapshot in the file. From this we can retrieve the widgets. Whatever adaptations you made to the other handlers should be made here, modulo the above observation.
There was a problem hiding this comment.
Oh, and we use nextLine because we want to show widgets appearing anywhere on pos.line, regardless of column/character.
There was a problem hiding this comment.
Do you have an example where showing all widgets in a line is valuable, considering that this is not how the rest of the info view behaves? To be clear, the one regression I see in my changes is that if someone puts multiple tactics in a single line, they will only see the widgets of the selected tactic. Which sounds pretty acceptable to me in any case.
There was a problem hiding this comment.
Yup, the motivation is described in the last bullet of #2963.
There was a problem hiding this comment.
That justification just links to another uncommented code blocks devoid of actual documented motivation :( . Getting to the bottom of this is very frustrating and I'm inclined to go forward with changing the semantcs (in the minor way described above) to what makes the most sense to me in the long term.
There was a problem hiding this comment.
Actually it might be fine to break that since we now have widget messages. The motivation I linked (and the undocumented piece of 'Try this' code) were about making the 'Try this' widget be displayed under the same conditions (any on the line, ignoring columns) as diagnostics. But now we can put 'Try this' in a diagnostic.
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added
breaks-mathlib
|
Mathlib CI status (docs):
|
leodemoura
force-pushed
the
master
branch
2 times, most recently
from
32d60c5 to
696f70b
Compare
After each tactic step, we save the info tree created by it together with an appropriate info tree context that makes it stand-alone (which we already did before to some degree, see
Info.updateContext?). Then, in the adjusted request handlers, we first search for a snapshot task containing the required position, if so wait on it, and if it yielded an info tree, use it to answer the request, or else continue searching and waiting, falling back to the full info tree, which should be unchanged by this PR.The definition header does not report info trees early as in general it is not stand-alone in the tactic sense but may contain e.g. metavariables solved by the body in which case we do want to show the ultimate state as before. This could be refined in the future in case there are no unsolved mvars.
The adjusted request handlers are exactly the ones waited on together by the info view, so they all have to be adjusted to have any effect on the UX. Further request handlers may be adjusted in the future.
No new tests as "replies early" is not something we can test with our current framework but the existing test suite did help in uncovering functional regressions.