[xml protocol] [coqide] Alternative PR fixing some loc problems in master. #17382

ejgallego · 2023-03-14T20:11:05Z

@herbelin suggested to have a look at the current status of Coq master problems, so indeed, the main source of pain on what we could see is just that the locations are not fully serialized, in particular missing line number on the protocol wire impedes us to properly handle Coq locations effectively (and without hacks).

We also fix a off-by-one error we hand't spot due to the missing line info.

We have verified that this PR seems to fix the loc part of #17023 , modulo the 8.16 behavior, which as noted by Théo is:

however, in Coq 8.15-8.16, the displayed warning is associated to a (correctly located) underline, but the tooltip is broken, and if we undo and redo the last line, it does not show at all (exactly as described for the Foo command in this issue),

Not sure about the idtac display and we didn't get CoqIDE to display it, neither in 8.16.

We submit this PR for testing against #17348 , as to see if master revert to 8.16 vs master + this fix has more bugs.

Fixes #17023 fixes #16987

herbelin · 2023-03-14T21:38:23Z

Also: the PR fixes the wrong error line numbers in Errors tab.

For loading @MSoegtropIMC's test file Flocq's Pff.v, it takes for me 3mns (compared to ~1mn with coqc and ~1mn 15s with coqide 8.16). So this seems too long (but I don't know which PR caused this).

Location, message and tooltip on warnings works for e.g. Set unknown option, or Variable a:nat at toplevel. For Focus, location is ok but the tooltip is empty, apparently due a wrong stm id (so Coq side, since 8.15).

Zimmi48 · 2023-03-15T10:18:19Z

For loading @MSoegtropIMC's test file Flocq's Pff.v, it takes for me 3mns (compared to ~1mn with coqc and ~1mn 15s with coqide 8.16). So this seems too long (but I don't know which PR caused this).

I'll let @coq/coqide-maintainers be the judges, but I would tend to find this an acceptable performance regression in CoqIDE. From what I recall, the previous performance regression was way worse on this file. This should also be compared with the alternative in #17348, rather than with Coq 8.16.

Another point of comparison is that this PR currently passes CI fully, but #17348 does not (although its backport for Coq 8.17 does).

Zimmi48 · 2023-03-15T10:20:40Z

Oh, but I didn't realize that this fix actually changes the XML protocol, so would be good for Coq master only and would require documentation and fixing Coqtail + VsCoq.

So, we could merge #17381 in v8.17 and this PR in master...

ejgallego · 2023-03-15T12:35:57Z

Yes this PR changes the XML protocol hence it would be master-only. Hugo's idea was to see whether we could do better in master than just reverting to 8.16 status which had some problems on its own.

There should not be any performance regression in master w.r.t. large files, if that is happening then we got a bug, wouldn't be surprised. If someone can profile CoqIDE and see where the time is spent with this patch that could be helpful.

MSoegtropIMC · 2023-03-15T12:54:47Z

As discussed in Zulip I can test CoqIDE but I see still PRs opened. Please let me know when is a good time to test and then also which commit to test.

Zimmi48 · 2023-03-15T12:55:51Z

As discussed in Zulip I can test CoqIDE but I see still PRs opened. Please let me know when is a good time to test and then also which commit to test.

The point is precisely to test PRs before they are merged though.

ppedrot · 2023-03-15T12:58:27Z

For loading MSoegtropIMC's test file Flocq's Pff.v, it takes for me 3mns

It's standard that CoqIDE + go-to-end is slower than coqc on the same file. I'll profile this to see whether this PR has anything to do with it but this is unlikely. (Also the problem wouldn't happen in the same process, in the first case it's coqidetop but in the second it's coqide proper.)

MSoegtropIMC · 2023-03-15T13:03:02Z

The point is precisely to test PRs before they are merged though.

Sure, but afaik there are several PRs and some pushed to again and I don't have the bandwidth to test it 5 times. So I need to know what the sweet spot is.

Btw.: with CoqIDE 8.17+rc1 I get for my favourite IDE test file

https://gitlab.inria.fr/flocq/flocq/-/blob/master/src/Pff/Pff.v

a strange syntax error when stepping over the tactic definitions right at the top.

MSoegtropIMC · 2023-03-15T13:05:19Z

For loading MSoegtropIMC's test file Flocq's Pff.v, it takes for me 3mns

2..3 minutes is normal. If it is bad it is more like an hour.

ppedrot · 2023-03-15T13:14:53Z

FWIW the runtime of go-to-end with CoqIDE on Pff.v with both this PR and master are the same. Furthermore I don't see anything suspect, neither in the profiling of coqide nor on the one of coqidetop. So for me this is good.

MSoegtropIMC · 2023-03-15T13:20:05Z

@ppedrot : I guess this means you also don't get the strange syntax error I am getting with 8.17+rc1.

I am currently working on getting the smoke test kit in Coq Platform master working - in creates _CoqProject files, so one can load all files directly into CoqIDE. It should work again today evening.

ppedrot · 2023-03-15T13:21:16Z

Also, as I've already ranted about at the WG this still looks fundamentally broken to me because the protocol confuses lines with sentences. You can trigger line desynchronization with the following snippet.

Ltac wait n := match n with 0 => idtac | S ?n => wait n; wait n end.

#[deprecated(since="8.16")] Notation tt0 := tt.

Goal True.
Proof.
fail.
Qed.

Goal True.
Proof.
wait 20.
elim tt0.
Qed.

To trigger the bug, eval to end and before the "wait 20" line returns, introduce random text in the first Proof-Qed block. This will cause the warning location to be shifted by as many lines inserted. This kind of problem can only be solved by making locations sentenceid-based, but I'm not sure we want this. This would require changing the protocol, again.

herbelin · 2023-03-15T16:26:12Z

Yes this PR changes the XML protocol hence it would be master-only.

Wasn't #17348 already changing the XML protocol (in the sense of changing the conventions about the positions returned in Message outputs of Coq)?

Conversely, what convention are Coqtail or vscoq expecting the locations returned by Coq?

As far as I'm concerned, if Coqtail and vscoq are fine with the PR (i.e., see next comment, if neither #17348 nor this PR change their use of the protocol - up to adding a fallback when bol_pos and cie are not present, but this is easy to do), the locs seem good in what I tested and I would recommend merging the PR.

2..3 minutes is normal. If it is bad it is more like an hour.

Then, ok, let's not make the current 2-3mns situation "blocking" (reminding that these 2-3 mins are indeed unrelated to this PR).

the protocol confuses lines with sentences.

My (vague) perception is that the cause of the loc shift when interactively editing (also reported in #17023) is not about the use of lines per se but about how a returned message is dynamically "relocated" wrt to the beginning of the input initially sent (rather than kept relatively to the beginning of the buffer).

herbelin · 2023-03-15T16:26:30Z

So that it is possible to understand if vscoq is affected by either #17023 or PR, can someone (presumably @maximedenes or @gares I guess) explain the requirement for vscoq:

which loc is passed to coq by vscoq (absolute character, or absolute line + character from beginning of line, or relative character from beginning of evaluated sentence)?
which kind of loc is expected from coq (character only, or line + character from beginning of line)?

So that we know if has to be mandatorily a revert of #17023 or if this PR is ok (again knowing that the protocol can be made compatible if the way locs are interpreted in #17023 is not a problem).

(Incidentally has someone in mind the summary of what had been the successive conventions regarding locating the Coq output along the history of the protocol?)

jfehrle · 2023-03-15T18:01:22Z

@ppedrot You can trigger line desynchronization with the following snippet.

The fix I proposed in #17012 handles this case just fine without changing the protocol and so could be included in 8.17. (IIRC it needs a little more work to handle the case when loc is not None--I abandoned the effort when this PR was dismissed out of hand. Edit: This example does, in fact, pass loc in the XML.)

ejgallego · 2023-03-15T20:18:47Z

To trigger the bug, eval to end and before the "wait 20" line returns, introduce random text in the first Proof-Qed block. This will cause the warning location to be shifted by as many lines inserted.

Fixed by the last commit. Actually you only need to compensate for the offset difference of when the tooltip was created. At some we had a similar mechanism but was broken for other reasons, it should be now more principled.

This kind of problem can only be solved by making locations sentenceid-based, but I'm not sure we want this. This would require changing the protocol, again.

Only may be a too strong statement here, given any sentence, you can actually compute the absolute offset that the sentenced has moved when compared to its creation, so you can adjust locations that were created a sentence-creation time, as done now. So no change in the protocol needed, just proper handling of information lifetime (in particular when you wanna do some incremental stuff such as not regenerating tooltips in later parts of the document)

herbelin · 2023-03-15T20:19:48Z

@jfehrle: if I'm correct, the fix in #17012 (for None) was included in #16978, right?

I tested warnings, errors and tooltip in vscoq.

the location of Focus (as reported in Tooltips for messages with an explicit loc broken #17023) is wrong (one line above) for 8.15, 8.16, master and this PR (*); the tooltip is shown (though on the wrong location)
the location of the underlining and of the tooltip on say Variable n:nat at toplevel or of a Set UnknownFlag is correct in 8.15, 8.16, master and this PR (except that it starts from the period at the line before...)
the location of errors seems correct for 8.15, 8.16, master and this PR.
the presence of unicode does not break the locations

My conclusion on these tests is that this PR is not worse for vscoq than previous statuses.

I don't know how to test coqtail.

(*) maybe the same +1 missing somewhere in vscoq as it was in Coqide at some time?

jfehrle · 2023-03-15T20:47:55Z

@herbelin if I'm correct, the fix in #17012 (for None) was included in #16978, right?

The code for the None case looks like it's probably equivalent. The code for the Some case was not included. Hard to remember who did what when 3 months after working on it. And hard to visualize the net change when it's split across multiple PRs.

I tested warnings, errors and tooltip in vscoq.

Meaning this PR or #17012?

jfehrle · 2023-03-15T21:07:23Z

@ejgallego Fixed by the last commit. Actually you only need to compensate for the offset difference of when the tooltip was created. At some we had a similar mechanism but was broken for other reasons, it should be now more principled.

You've adopted my approach, which is to save and apply the original offset in the sentence. Earlier you were rejecting that out of hand. (At the time, you seemed unable or unwilling to understand my short code.) If you use that approach, you don't need to modify the protocol at all. That seems like a better solution.

herbelin · 2023-03-15T21:23:05Z

Same analysis with coqide (confirming the analysis of @Zimmi48 here:

the location of the warning for Focus is ok for 8.15, 8.16 and this PR; depending on position in text, tooltip is empty (only the bulb) or absent; ill-located and well-tooltipped in 8.14; not located, nor tooltipped in master
the location of the warning and of the tooltip on say Variable n:nat at toplevel or of a Set UnknownFlag is correct in 8.14, 8.15, 8.16, master and this PR
the location of errors seems correct for 8.14, 8.15, 8.16, master and this PR.
the location of errors from the error tab seems correct for 8.14, 8.15, and this PR but wrong in 8.16 and master
the presence of unicode does not break the locations
the blue display of the debugger is ok in 8.16, master and in the PR
the red display of breakpoint of the debugger is ok in 8.16, master and in the PR but the setting of the breakpoint is off by 1 in 8.16, master and the PR (you need to highlight the character preceding the first letter of the tactic name)

So, shortly, the PR looks good to me (no change for vscoq, improvement for coqide, even though the ltac breakpoint is still off by one and the tooltip on Focus is still empty).

herbelin · 2023-03-15T21:31:03Z

Meaning this PR or #17012?

This PR (with or w/o the 3rd commit, which is anyway only for the case you add text while it is running, iiuc; the extra commit does not restore the empty tooltip on Focus).

ejgallego · 2023-03-15T21:34:39Z

@herbelin the missing tooltip in focus is due to the tooltip being attached to the wrong sentence, the code in tooltip_callback will still display the icon even if no matching tooltip was setup.

That's beyond what we can fix here I think.

herbelin · 2023-03-15T21:40:50Z

That's beyond what we can fix here I think.

Yes, I don't think it is important to fix now (even if, apparently, vscoq knows how to do it correctly).

So, @Zimmi48 may merge the PR tomorrow, if no opposition?

jfehrle · 2023-03-15T22:13:25Z

@herbelin the red display of breakpoint of the debugger is ok in 8.16, master and in the PR but the setting of the breakpoint is off by 1 in 8.16, master and the PR (you need to highlight the character preceding the first letter of the tactic name)

Are you sure? I don't see that behavior with this PR. I'm on Windows+WSL if it is perhaps a machine/library version issue. (I couldn't remember the incantation to build and test on 8.16. I certainly would have noticed such an obvious debugger issue long ago.)

herbelin · 2023-03-15T22:50:06Z

I used the following example:

Ltac f := intros; idtac "A".

Set Ltac Debug.

Lemma testl :  True -> True.
f.

If I press F8 on the i of idtac, the d is red and it does not stop. If I press F8 on the space before the i, the i becomes red and it does stop (on MacOS 12). Tested with 8.16, master, and the PR.

jfehrle · 2023-03-16T03:40:02Z

You have to click before you press F8. Do you see the cursor in this position before you press F8?

If I press F8 at this point, CoqIDE highlights the "i".

Click-drag to select text works uses similar cursor positioning. If you click on the left half of a character, the cursor goes before the character and otherwise after it.

herbelin · 2023-03-16T08:30:38Z

Yes, it is like you describe. I think I just got confused with the text in the reference manual which says "position the cursor on the first character of the tactic name in an Ltac construct", which I wrongly interpreted as "select the first character of the tactic name in an Ltac construct".

Zimmi48 · 2023-03-16T14:46:16Z

If this PR is for master only, I'd rather have a CoqIDE maintainer merge it and I would handle the merging of the v8.17-only PR.

ppedrot · 2023-06-02T10:03:25Z

@ejgallego any progress on this?

ppedrot · 2023-06-23T08:58:16Z

@ejgallego This PR makes it already way better than we have on master, and it's a blocking issue for the 8.18 release. If you don't have a look soon, I'll forcefully merge this PR so that it does not delay 8.18.

Zimmi48 · 2023-06-23T11:10:27Z

Indeed! Either this PR, or the solution that was merged in v8.17, should be merged in master and available in 8.18.

Otherwise XML users can't use line number information coming from Coq.

…ove. This restores display of tooltips, same technique could be applied to other bugs.

This was a silly typo.

This was broken for a long time, likely since the debugger patch, see comment.

Turns out that we need to be a bit more careful at mark addition points as sometimes our info is coming from buffer's view and other times location information is coming from Coq which has an outdated view. For the tooltips, we make the choice to store them in Coq locations, which seems like a reasonable ground truth, as in the IDE side things could be much more dynamic, but it is also very efficient to perform the correction as the GTK iterators have the needed info in constant time. We also need to compute the drift of the line for the UTF-8 conversion fiction, otherwise we get things wrong on line-drifts.

ejgallego · 2023-06-23T15:28:40Z

Ok, found the last problem, I think this looks ready to me.

Last commit contains the detailed information, but basically we need to be careful about what our ground truth for locations are, and correct in all cases (coqide likes to use location sources with are related to the Coq location truth in different ways)

Also, due to the UTF-8 conversion routine, we need to compute line_drift.

All the examples I could come up with seem to be working now; I'd be there are more bugs lurking around (maybe the "errors" panel doesn't account for drift properly?), but IIANM, the current infrastructure should be solid in that sense and allow for quick fixes.

ppedrot · 2023-06-25T16:50:54Z

@coqbot merge now

coqbot-app · 2023-06-25T16:50:55Z

@ppedrot: You cannot merge this PR because:

There is still a needs: full CI label.

ppedrot · 2023-06-25T16:51:28Z

@coqbot merge now

coqbot-app · 2023-06-25T16:51:30Z

@ppedrot: You can't merge the PR because some changes are requested.

Stale review

ppedrot · 2023-06-25T16:52:44Z

@coqbot merge now

ejgallego · 2023-06-25T21:32:05Z

ide/coqide/coqOps.ml

@@ -40,13 +40,16 @@ module SentenceId : sig
    mutable flags : flag list;
    mutable tooltips : (int * int * string) list;
    start_offset : int;
+    (** Original start offset of the sentence, to be compared when moved *)
+    start_line : int;
+    (** Original start line of the sentence, to be compared when moved *)


To clarify semantics, "Original" here means "location Coq thinks the sentence is at."

The start / stop marks do contain the buffer real location of the sentence, so offset_compensation below can be used to apply / track the delta between the two.

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Mar 14, 2023

ejgallego force-pushed the xmlprotocol_fulllocs branch from 40ee30d to 8c37244 Compare March 15, 2023 20:14

ppedrot self-assigned this Jun 2, 2023

ejgallego added the needs: progress Work in progress: awaiting action from the author. label Jun 2, 2023

ejgallego added 9 commits June 23, 2023 16:35

[xmlprotocol] Serialize full locations

3a3de8f

Otherwise XML users can't use line number information coming from Coq.

[coqide] Fix off-by-one-error in Coq loc to GTK line loc conversion.

8df56ac

[coqide] Offset compensate location in tooltips if the sentence did m…

f465711

…ove. This restores display of tooltips, same technique could be applied to other bugs.

[test suite] Add testcase for coq#17382

be6c5c4

[coqide] Fix bol_pos calculation in coq_loc_from_gtk_offset

7c0ee03

This was a silly typo.

[coqidetop] Create properly the resumption location in coqidetop

cf32d22

This was broken for a long time, likely since the debugger patch, see comment.

[xml protocol] Changelog and correct outdated documentation.

b9490c9

[coqide] Fix typos, thanks to Jim for the review.

e15b543

ejgallego force-pushed the xmlprotocol_fulllocs branch from 1581a8f to 8192c35 Compare June 23, 2023 15:26

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 23, 2023

ejgallego removed the needs: progress Work in progress: awaiting action from the author. label Jun 23, 2023

ppedrot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 25, 2023

coqbot-app bot merged commit 78def24 into coq:master Jun 25, 2023
6 checks passed

ejgallego deleted the xmlprotocol_fulllocs branch June 25, 2023 19:24

ejgallego commented Jun 25, 2023

View reviewed changes

This was referenced Jun 30, 2023

Tooltips for messages with an explicit loc broken #17023

Closed

[coqide] Tooltip locations are broken in master #16987

Closed

[xml protocol] [coqide] Alternative PR fixing some loc problems in master. #17382

[xml protocol] [coqide] Alternative PR fixing some loc problems in master. #17382

Conversation

ejgallego commented Mar 14, 2023 • edited

herbelin commented Mar 14, 2023 • edited

Zimmi48 commented Mar 15, 2023

Zimmi48 commented Mar 15, 2023

ejgallego commented Mar 15, 2023

MSoegtropIMC commented Mar 15, 2023

Zimmi48 commented Mar 15, 2023

ppedrot commented Mar 15, 2023

MSoegtropIMC commented Mar 15, 2023

MSoegtropIMC commented Mar 15, 2023

ppedrot commented Mar 15, 2023

MSoegtropIMC commented Mar 15, 2023

ppedrot commented Mar 15, 2023

herbelin commented Mar 15, 2023

herbelin commented Mar 15, 2023 • edited

jfehrle commented Mar 15, 2023 • edited

ejgallego commented Mar 15, 2023

herbelin commented Mar 15, 2023 • edited

jfehrle commented Mar 15, 2023

jfehrle commented Mar 15, 2023

herbelin commented Mar 15, 2023

herbelin commented Mar 15, 2023

ejgallego commented Mar 15, 2023

herbelin commented Mar 15, 2023

jfehrle commented Mar 15, 2023

herbelin commented Mar 15, 2023

jfehrle commented Mar 16, 2023

herbelin commented Mar 16, 2023

Zimmi48 commented Mar 16, 2023 • edited

ppedrot commented Jun 2, 2023

ppedrot commented Jun 23, 2023

Zimmi48 commented Jun 23, 2023

ejgallego commented Jun 23, 2023

ppedrot commented Jun 25, 2023

coqbot-app bot commented Jun 25, 2023

ppedrot commented Jun 25, 2023

coqbot-app bot commented Jun 25, 2023

ppedrot commented Jun 25, 2023

ejgallego Jun 25, 2023

Choose a reason for hiding this comment

ejgallego commented Mar 14, 2023 •

edited

herbelin commented Mar 14, 2023 •

edited

herbelin commented Mar 15, 2023 •

edited

jfehrle commented Mar 15, 2023 •

edited

herbelin commented Mar 15, 2023 •

edited

Zimmi48 commented Mar 16, 2023 •

edited