Fix #781 PG does not position to error.

[Matafou]

We cannot use the " ^^^ " thing to compute the error location because commands are not stripped of newlines anymore (#774).

Solution: use the character position information with the following subtleties

• position are given by coq as bytes positions.
• position given by coq is the position from the previous "." fed to coq. I.e. we must be careful to strip any blank after the final "." ofthe previous (hence from all) commands.

[Matafou]

This needs a bit of a test and discussion.

It seems to work but it is difficult to be sure.

Things to check that I can think of.

• Is the computation of position robust to any encoding?
• Currently I strip trailing spaces of all commands otherwise coq's error location are wrong. Should we make this an option (in case it is not suitable for other provers)?
• test error highlighting in CI? This would need to check temporary overlays (they last 2 sec) which is not great.

[Matafou]

I just added a test that checks that the correct region is highlighted. @hendrik or @erikmd can you review pls? I sum up the fix:

Note: testing this I found something strange in error location info from coq

[Matafou]

This is not ready yet. I will try to fix this by the end of the summer.

[erikmd]

Hi @Matafou, thanks a lot for working on this!

It seems to work but it is difficult to be sure.

OK, I wouldn't have foreseen that fixing #781 would be that involved.

But anyway, if it works in practice and we can get a good CI tests coverage, that'll already be pretty good!

Is the computation of position robust to any encoding?

I saw you used byte-to-position so that should be Okay, anyway we'll be able to CI-test with a few standard encodings.

Currently I strip trailing spaces of all commands otherwise coq's error location are wrong. Should we make this an option (in case it is not suitable for other provers)?

Good question; this needs some discussion I guess, since your PR mainly touches coq.el, but also proof-shell.el.

Anyway, we don't have a CI testsuite for other provers (I had opened this issue: https://github.com/ProofGeneral/PG/issues/505 but it stalled).

test error highlighting in CI? This would need to check temporary overlays (they last 2 sec) which is not great.

I believe this is testable, and actually you already tested it IIUC:

I just added a test that checks that the correct region is highlighted.

@Hendrik or @erikmd can you review pls? I sum up the fix:

there was no sentence after your comment's colon ↑

Note: testing this I found something https://github.com/coq/coq/issues/19355

Does this mean that this PG PR will only work for Coq ≥ 8.20 ?

in this case, should we revert https://github.com/ProofGeneral/PG/pull/774 for Coq ≤ 8.19 ?

I believe the start-of-term will be dense for you as well @Matafou, but let me know (Cc @hendriktews) if you have a free slot in the upcoming days and would like to video-meet to discuss this, I'll try to join.

[Matafou]

The two failing tests are on coq-8.11. I will try to investigate but maybe this is not blocking. One problem remains: support the coq bug that has just been fixed in coq master?

[Matafou]

This seems ready. I will merge this tomorrow if no one objects. @erikmd this is an important fix imho, is there something to do to update pg distributed packages?

[Matafou]

This PR

• fixes #781
• makes use of the character location given by coq instead of the "^^^^"
• revealed https://github.com/coq/coq/issues/19355 in coq wrt to error location of curly braces.
• works around it by detecting suspicious locations (probably almost 100% accurate) and defaulting to something reasonable (beginning of command).
• introduces 2 tests of error highlighting including one specific to the workaround.
• has not been tested very widely, I guess users will complain if something is wrong.

[Matafou]

• re-introduced removal of error location from the response buffer.
• understood and partially fixed an old small bug on error locations: coq gives wrong location if one insert spaces at the end of a command (before the newline). We used to insert "Set/Unset Silent. " with a trailing space. I leave to another PR the removal of other similar wrong strings. I only fix this one because it happens all the time.

[Matafou]

I decided to add the fix of hardwired command strings (removing trailing spaces) in a separate commit of this same PR.

[Matafou]

The failed CI is not related (reached VM limit). I merge now.

[erikmd]

Thanks a lot @Matafou !

sorry for replying late

@erikmd this is an important fix imho, is there something to do to update pg distributed packages?

It depends on the distribution you think of:

• for MELPA, as soon as the PR has been merged in PG master, it is rebuilt later on during the same day
• for NonGNU-devel ELPA, this is the same
• for NonGNU ELPA (stable releases), we will need to do a release — note that a tag is not enough, see this comment by Stefan: https://github.com/ProofGeneral/opam-switch-mode/pull/10#issuecomment-1599495287