PG does not position to error

[Matafou]

This bug appeared because of PR #774. Backtracking it is not satisfying because #773 shows a good reason for it.

Example:

Require Import Utf8.
Definition trois := 3. (*test-definition*)
Definition β := 3. (*test-definition*)
Definition β' := 3. (*test-definition*)
Definition β'' := 3. (*test-definition*)
Print trois.
Eval compute in (λ γγ:nat, γγ)
                       4 +
                       (λ a:nat, a) 4
                     + ααα * trois * trois.

the error is not positioned on ααα. This has nothing to do with utf8, but any fix should check that it works ok for this.

[Matafou]

original issue by Vadim Silva on zulip.

[MackieLoeffel]

A simpler testcase that does not require Utf8 is the following:

Lemma test :
  Truea.

PG shows an error on first line for me, but it should be on the Truea in the second line. Setting proof-shell-strip-crs-from-input to t (i.e. undoing https://github.com/ProofGeneral/PG/pull/774 ) works as a workaround.

[Matafou]

Thanks for the reduced case. I am planning a fix for the end of the summer. We need proof-shell-strip-crs-from-input for other reasons (#773). FTR, this is also slowed by a bug in error location info from coq now fixed in coq master.

[RalfJung]

I am also running into this now, this bug makes it quite hard to figure out what Coq's errors mean in PG.

I tried adding

 '(proof-shell-strip-crs-from-input t)

to my custom-set-variables but that did not help unfortunately. However, reverting to PG 0e0170f96f5feaeefe59052a08373080acc20393 (just before the problematic PR got merged) helps.

[MackieLoeffel]

I am currently using the following in my .emacs file to automatically set proof-shell-strip-crs-from-input to t:

(add-hook 'coq-shell-mode-hook (lambda () (setq proof-shell-strip-crs-from-input t)))

(custom-set-variables does not work since the configuration of coq-shell-mode overrides it.)

[monnier]

(add-hook 'coq-shell-mode-hook '(lambda () (setq proof-shell-strip-crs-from-input t)))

Side note: please don't quote your lambdas.

[MackieLoeffel]

Side note: please don't quote your lambdas.

Indeed, thanks! I edited my message above in case someone copies it to their .emacs file.

[pedrotst]

I just bumped my PG from a 2 year old config and was driving myself nuts to find why the error wasn't working properly (hence got myself here). Thanks for the workaround, I can have peace again.