The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Consider A.v:

Require Import NArith.

Definition xxx2aaaaa :=2.
Lemma xx : 2 = 1+1.
Proof using.
  reflexivity.
Qed.

coqc produces the following A.glob file for it:
DIGEST 582ed5cc0da4be8a628fbad21346a25b
Fvok.A
R15:20 Coq.NArith.NArith <> <> lib
def 35:43 <> xxx2aaaaa
prf 56:57 <> xx
R62:64 Coq.Init.Logic <> ::type_scope:x_'='_x not
R66:66 Coq.Init.Peano <> ::nat_scope:x_'+'_x not

In particular, in A.glob, note the line starting with prf which says that the proof (lemma) xx

is defined at characters 56:57 in the file.

When I tell emacs to jump at character offset 56 (using (goto-char 56)) in A.v, it goes to the 

whitespace character just after "Lemma" in A.v, which is correct, e.g. when using for "jump to definition" of xx.

But when I start using unicode characters, this gets messed up.

Suppose that I now change the 'a' to \gamma in A.v:

Require Import NArith.

Definition xxx2γγγγγ :=2.
Lemma xx : 2 = 1+1.
Proof using.
  reflexivity.
Qed.

Now, coqc produces the following A.glob:

DIGEST fe6c13708e4f56188975fb9fe403c8a6
Fvok.A
R15:20 Coq.NArith.NArith <> <> lib
def 35:48 <> xxx2γγγγγ
prf 61:62 <> xx
R67:69 Coq.Init.Logic <> ::type_scope:x_'='_x not
R71:71 Coq.Init.Peano <> ::nat_scope:x_'+'_x not

Note that the offsets in the prf line got increased by 5, exactly the number

of unicode characters. Note that the position of "Lemma xx" in A.v hasn't changed: I just replaced characters, didn't move anything

Now, my .glob-file based jump to definition jumps at the wrong location.

For a file with a lot of unicode, this becomes very annoying.

Is there a way to get coqc to produce the "correct" offsets in .glob files:where it doesnt count unicode characters as multiple files?

Alternatively, is there some variant in goto-char in emacs that can account for the double counting of unicode characters?

-- Abhishek

http://www.cs.cornell.edu/~aa755/