coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] correct offsets in .glob files when unicode characters are present

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] correct offsets in .glob files when unicode characters are present
Date: Thu, 23 Mar 2023 14:50:17 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f44.google.com
Ironport-data: A9a23:1JrAc6IvZF07FLSRFE+RCJElxSXFcZb7ZxGr2PjKsXjdYENS02YOm 2ofXWyGOv6OZzTwe4t2O4uwpE1Qu5/TzINhGwYd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fSLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWCfg71s9JIGjhMsfnb80k05K6aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0Luf0nK0clhHAYMZ6Y/xuYpL31gr qcZEWVYBvyDr7reLLOTT+BtgoE8NpCuMt9D/H5nyj7dALAtRpWrr6fiv4cJmmdtwJoURLCCO 6L1ahI3BPjESxRFOlYMCJ892u6uj3/zNTxZtF29qq8+4myVxwt0uFToGIuFKoTUHJ4N9qqej m2ewEGnUiMoDteOlHmZ1lmSpv/soAquDer+E5XhrqIw6LGJ/UQYDwRTXl+mq9Gim0umUpReL VYV82wgt8APGFeDS9D8W1inuifBsEJAHdVXFOI+5UeGza+8Dxul6nYsQgxneuAppIgMHxcN6 l/Xsc/HXmduiejAIZ6CzYu8oTS3MCkTCGYNYy4YUAcIi+UPRqlj3nojqf4zQMaIYs3J9SLYm G/V8XBv71kHpYtaiPXhpAGvbyeE/8CRFmYIChPrsnVJBz6Viaagbo2srEfBtLNOcNrfQV6Gs 3wJ3cOZ6Yji7K1hdgTcGY3h/5nzv55p1QEwZ3YxRPHNEBzzoRaekXh4um0WGauQGp9slcXVS EHSoxhNw5RYIWGna6R6C6roVZt7kPCxRY+7B6iMBjarXnSXXF/XlM2JTR7At10BbGBx+U3CE c3KKpj8UC5y5VpPkGbuGI/xLoPHNghnnT+JLXwK5xug1rWaaRaopUQtYTOzghQCxPrc+m39q o4PX+PTkkk3eLCgP0H/rNFLRXhUdyRTLc6t8KR/KLXTSjeK7Ul4VZc9N5t9JtY190mU/8+Ul kyAtrhwkwWn2SCfd1nbNRiOqtrHBP5CkJ7yBgR0VX7A5pTpSd/HAH43JsBvL4o0vvdu1+B1R PQjcsCNSKYHADfe9jhXKdG3oIV+fV75zUiDLgi0UggZJpRAfg3u/sO7Xw3N8CJVMDG7m/Fjq JKd1yTaY6E5eSJcMOjsZsiSkmyB5UompLoqXm/jAMViR0H3wY07dw3zlqAWJu8PGzXixxyb9 QCcPjkAr8KQoYVvqNjtroKHprePDOFRMBd7HW7azLDuLgjc3DOp7rFhWdayXwL2dT3L6oT7Q s5K3dTQDeYhoG9al6ZdT5N60rMY5fb0gr1RkzRfA3TAamq0BoNaInWp2ddFsotPzOR7vTSad 12u+N5IH6egI+LgTUAsITQ6YtS51f07nifY6dI3Kh7Y4A515L+2blVADSKTiSByLKpHD619+ L0P4PUp0g2YjgYmFv2kjSoOrmSFESEmYpUd75ofBNfmtxovxlR8eqfjMy7R4q/eT/VXM0IvH C2Yu7qauZRY2Xj5UiQSEVrj4LNjoKog6TFw8U86BlWWm9D6qOc98z9P/B8WEAlE7BV1/NhiG 2psNkdKC72E1G4zj8puQ1KuIlllARGH8Bb90GkyyW/TFRGpckfvL2QNH/mH025E0mBbfxldp Kq5zkS8WxnUXcjB5AkAcm87lO7GUvpw6RzkpMCrO++nDqsKS2PprYH2bFVZtia9J906gXP2g NVD/cFyWPXdDjERqahqMLuq/+0cZz7cLVMTXMw72r0CGFzdXzSA2TKuDUSVUeEVLtzo9X6IM eBfFvhtZT+fihnX9is6AJQSKYBahPQqvdoOWo36LF487oewkGBbj4LyxAPf2kkbG85jgOQsG LP3LjiiKFGdtVFQum3KrfRHBFaGXMk5VFX88d2xoco0FMMlkeBzcEsN/KO+kFeLPSBGoR+Fn gPxSJXH7u5lyLY2xovlLbpeNl/lNfLyS+W63wShuPtebd70EJnvtiFEjnLFLghpLb8qdNAvr ou0sfnzx1LjgLktdnLwwr2tKvFs3tqje8ZyKef1HWl+sQrZf/G0+DoF2WSzCaIRoeNn/sP9G jeJMpqhR+AaS/J25SNweSNBNz0/Fq6uTKPrhR3lnsS2EhJHjDD2doK2x0TIM1NeWDQDYaDlK wnOvP2r2NBUgaJMCDIABNBkG5VIG0Dia4R3a+zOsSSkMUfwjmOgorfCkT8S2QPPAFSAE+f45 svLeEGvPlD68qTF18pQvIFOrwUaRiQ1y/U5ekUGvcV6kXamBWoBNv4QKogCFooSqCHpyZXkf 3vYWQPO08kmsehsKn0QIegPXztzwsQLM9b9YyMzpgaaN3vwC4SHD79ssCxn5h+av9clIP6Pc bkjFr/YZ3BdAa2Fgc4c4/W6haFswfayKrcg5xXmi8Kra/oBKexi6ZGidTahkQTIFsjMkAPAI m1dqaWohq2kYRaZLPuMsEK51P3UUP0DAtnogeqyLA7jhrim
Ironport-hdrordr: A9a23:7ZWhR62GMkWnJDAv1wFWHAqjBIwkLtp133Aq2lEZdPUnSL39qy nIpoV86faUskd3ZJlD8ersBEDkex/hHPFOj7X5UY3SPzUO21HIEGgB1+TfKlTbckWUnNK1vp 0QEZSWZueAaGSSwfyb3OHMeOxQueVuucuT9J/j80s=
Ironport-phdr: A9a23:Olj9Fxci4ZxZRoQKeJqgksqClGM+1tfLVj580XLHo4xHfqnrxZn+J kuXvawr0AWUG9+Ht7kd0reempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmjqwbalsI Bi5ogjdudQajZZiJ60s1hbHv3xEdvhZym9vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2T qFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4 qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhNwzY7bYoGbOvR9cK3AY90VWXFMUdxNWyFbGI6wc 5cDAugHMO1Fr4f9vVwOrR6mCASwH+zvyj5IhmT23aIk0OQqDB3L3Ao6ENIIrXvfsdL4O70JX uC1zanI1jXDYO1V2Tvn8ofIdAouofeRUr5qcMrRyFUvFwzeg1WfrIzqJTKV1uAXv2eH6OpgU Puihmg6oA5+vjah3N0jipXVho0L0FDE8z10zJgxKNGlSEB3f8CpHptMuiybK4d6X8wvT391t Ssn17AItpC2cSYKxZooyBPTdeCLfomU7xztV+ufITl2iXZqdb+5mh28/0+gyujmWcm11lZHt jZKkt7WtnALyRPT7syHRuFj8Ui8xDaDzxzc6uZeIUAyi6XbL5ohzqQqmpUNrEvDAyn7k1j1g q+Obkgo5PSk5uD9brjlppKQLZF4hh/jPqg0lcGyDuI1ORUUUWeB4+Szzrjj8FX5QLpUiv02l bHUsJXAKsQaoq61GgFU0pw+5xqmATer39sVkWMILFJCfxKHgIzpNE/ULP/kCve/hkygkDZtx //YIr3sGovBImTHnbv7frtw61RQxBQtwdxC/Z5ZBb4MLOr2WkDrtdzYChE5Mxazw+biENhyz JgRWWKOAq+CMKPdr1yI6vg1LOmKfoAVvivyJ+Ik5/7vkX85lkQQfaas3ZQNaXC4Gu5qLFmeY XrpmtsBF3wFsRIkTOP2kF2CTSJTZ3GqUq4h/j07Ep6pDZ/fRoCxh7yMxDu0HppPZmxfFl+MF WroeJ6fVvcXaCOSJ9dhnSYeWbigTY8hzxCuuxXgx7ppNOqHshEf4JnkzZ1+4/DZvRA07z19S cqHgE+XSGQht2kIRiQ20aM3iEp0zFvLhaFyg/1DFdFQofpPWwE2c5/d0+NSBNX7WwaHddCMH gX1Cu66CC08G4pii+QFZFxwTo3KZnHr2iOrB+VQjLmXHNku9ama2XHtJsF7wnKA1a87jlBgT NEcfXa+iPtZ8A7eT5XMj13fj7yjIK0W3C/W9GqAi2OItUdUFg9xTartUnUWZ0+QptP8tQvZV 7H7Mb08KUNazNKabK5Da9nnl1JDEf7pONXFY2+y3W62DBCEgLKNcIXCdGAU3SGbA08BwEgI5 XjTEw84C2+6pn7GSjxjEVW6e0T37ex3s2+2VGcxxgCOKlJ7jv+7pkJTivubRPcemLkDvU/Ns h1SG1Cwl5LTAtuE/U96eblEJMk66xFB3H7YsAp0OtqhKbpjjxgQaVY/uUSmzBhxBoha9Kpi5 Ho30Ap/L76Z21JdZnuZ2573ILjeNmj1+limdafX3ljU1Nve9L0I7bw0rFDqvQfhEURHkT0v2 tNV0mCc65aMBQwbV563U0cr+DB1orjbZm824IaVnXxgPK+osyPTjsozDbhAqF7odNNePaWYU Q7qRpdCVo7+dapwwQHvMk5XWYIavLQ5NM6nafacjauiPeI62SmjkXwC+od2lESF6yt7TOfMm ZcD2fCRmAWdBFKexB+stN76nYdcaHQcBG26nGLtDo5Qfa1/fsACD26oL4u2x8lxr5HoUn9cs lWkAhlVva3hMQrXdFH70QBKgA4eq3ymgiu1zHp9lTgvouye3TDB6+vnfRsDfGVMQSMx6DWka ZjxhNccUk+yagEvnxbw/kf2yZ9Qo6FnJnXSS0NFF8TvB1lrSbD49r+LYsoVrYgtrT0SSuO3J 1aTVr/6pRIelSLlBWpXgj4hJXmmvZDwnhoyj2z4Tj47pXDZeNpwyBSZ7drVQ/IX3zsaSwF3j DDWAh63ONzh8diPlpjFu/yzTCr7DswVIXStl9nZ8nfnrWRxZH/31+i+gNjmDRQ33Wfg2t9mW D+J5Bfwb4/31rirZOduf01mHlj5uIJxHoBzlJd1hYlFgyBLwMXIuyBdyCGvbYY+u+q2dncGS D8VzsSA5QHk3BcmNXeV38fjUX7bxMJ9Zt68a2dQ2yQn7skMBr3Hid4M1SZzvFe8qhrcJPZnm TJIg/Ik6H8Bg+wK/gMrxyORRLETAUZwMinllhDO5Ne75vYyBi7nYf2r2UxykMr0RriIogBHW Hv6PJ4kFCl8qMR+LF3k33j664Wic97VJ4F21FXcg1LLiO5bL4g0n/wBiH98OG7zinYizvYyk R1k2Zzp9JjCMWhm+7i1RwJJLjCgLd1G4Snj1OwN+6Tel5DqBJhqHS8HGYflXe79WixHruzpb k6PCGFu8SrdQOuHW1XDtwE+6CiTW5GzayPJeD9Dlo4kHUfFYhQY2VFxPn1yn4ZlRF70gpW5K gEhoGhWvAawqwMQmLw2cUOjAyGP/EHwLW1sAJmHcEgJtEcbuwGMYJbYtqUqT0Q6ttWgtFDfd TDdPl4VSzlPAgvdWRjiJuX8vIGQtbHHWazuaaOJO+zGqPQCBa7XntT2g9cgp3DUcZzRWxsqR /wjhhgZBSE/S5mfwm9fDXRQzn2FbtbH9k3lpGsq/obmoa6tAEW2tMOOE+cAa4wxvUrt0OHYb ajIw38oTFQQnoUFwXuCoFQG9HgVjSwmNzykELBa8DXIULqVgKhcSRgSdyJ0MsJMqaM6xAhEf 8DB2Jvz0fZjg/g5Bk0gNxSpk9y1ZcEMP2C2NU/WTEeNOrOcIDTXwsbxKaqiQLxUhe9QulW+o zGeW0PkOz2CkXHuWXXNealUizqHORVFpIynWhNkCGymU8i/LxPnbJl4ijo5xbByjXTPdCYdP TV6b0JRv+iQ4Cdf0ZAdUyRK6ntoK/XBmj7MtbGJbMZL96ExW2Ioy7E/gjxy0bZe4SBaSeYgn SLTqoQruFS6iqyVzTEhVhNSqzFNjYbNvEN4OKyf+IMTPBSMtB8L82iUDAwH4tV/Ddi68alay tnUlK/wbj5E+tTYu8odG8f8J8eOMX5nOh3sUm2xbkNNXXuwOGfTilYI2umV7WGQp4Mmp4LEn ZMPTvpETgVwGK9GTEtiG9MGLdF8WTZuwtv5xIYYoHG5qhfWXsBTuJvKA+mTDfvYIzGclbBYZ hEMzNsQwqwcM4T63wppbVwoxewi/mLfWNlMpmtqaQpm+C2lEVB7R2w3nl3/M0ajvCNVGvmzk Ro7zAB5ZLZ1nAo=
Ironport-sdr: 641c9f8f_no6NhLWnodTMbeEwCSoZdZBXOKl2VH8LxME5rh/wKdp1NcO +rK0t/YcXMjUNS7WJ+R60vG7nUN6fpntK9qRE/Q==

Sorry I misunderstood the suggestion of Rodolphe.

The function to use is byte-to-position instead of position-bytes.

(When I said it worked, it worked accidentally: for some reason, position-bytes was returning nil and thus my version of company-coq was falling back to the regexp method of locating definition in a file and thus computing the right target to jump. a big problem with the regexp method is that it doesn't work in files that have multiple same-named definitions in the same file, e.g. under different Modules)

-- Abhishek

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

On Thu, Mar 23, 2023 at 1:22 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Thanks. Indeed, Rodolphe Lepigre just suggested doing
goto-char (position-bytes (pos-computed-from-glob-file)) instead of goto-char (pos-computed-from-glob-file) and it works. Issue closed.

Thanks
-- Abhishek
http://www.cs.cornell.edu/~aa755/

On Thu, Mar 23, 2023 at 1:09 PM Jim Fehrle <jim.fehrle AT gmail.com> wrote:
The parser returns byte offsets, not Unicode offsets. Not sure we'd rush to change that--it could be significant work and it would disrupt existing code that relies on byte offsets. It would be odd to use a different convention for offsets just for .glob. In code such as your .glob-file based jump to definition, it shouldn't be hard to convert from a byte offset to a unicode offset.

On Thu, Mar 23, 2023 at 9:43 AM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:
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.
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/

[Coq-Club] correct offsets in .glob files when unicode characters are present, Abhishek Anand, 03/23/2023
- Re: [Coq-Club] correct offsets in .glob files when unicode characters are present, Jim Fehrle, 03/23/2023
  - Re: [Coq-Club] correct offsets in .glob files when unicode characters are present, Abhishek Anand, 03/23/2023
    - Re: [Coq-Club] correct offsets in .glob files when unicode characters are present, Abhishek Anand, 03/23/2023
- Re: [Coq-Club] [Emacs] correct offsets in .glob files when unicode characters are present, Stefan Monnier, 03/23/2023