coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coqdep error locations: line+column vs character number

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] coqdep error locations: line+column vs character number
Date: Tue, 3 Mar 2020 10:54:13 -0800
Authentication-results: mail3-smtp-sop.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-io1-f42.google.com
Ironport-phdr: 9a23:O8Z25RdvQfvdNbtix4o/eiEUlGMj4u6mDksu8pMizoh2WeGdxcS+YR7h7PlgxGXEQZ/co6odzbaP7+a5ATJLuMzZ+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjeu8UMnIduNqc8xhTUrndWZ+hd2H9lK0+Ukxvg6ci8+4Ju/T5NsPw77c5AVqv6f6U8TbNGCTktLn446s72uxTdVAWD/nQTXHkYnRpOGAjF8Qr1XoztvSvgt+pywzeVMMvrRr0pQzui7qNrSBj1iCcbMjMy7W/ahtBsgK9dvRmsoQF0zYzJb4GPLPdxca3dctEaS2RPXchfSjJPDZ+nYoQVE+YMJ/xVo5Xhq1YMqxa1GAmiBPnoyj9NnnL7wbY10+QgEQHd3AwvAdEOu2nIodXzLqgSV/26x7TPwDrZdPxW2Tb96JPIch8/ovGAR6h/cczLxkkpCgzJlFSQqY35PzOazekNvG2b4PBhVeKrkWIotwZxoj22y8oql4LHiIUVylXe+iV4xoY4PcG3SElhYd6iDpRQsyWaO5FoTcw/XmFkoDo1yrocuZ69YicKzJAnywTFZ/OZboeI/xTuX/uSLzdgnH9pZq6zihKo/UWjyuDwTNS43VdLoyZfndTAqHYA3AHJ5MedUPty5EKh1C6P1w/N7uFEJlg5la/BJJ4gxr48j5sTsUPeEiPvlkX7g7Gael8r+uiv7OTnbbHmqYGGO4BojQH+N7wims25AesmLggDR3aX9fi42bH5/kD0QK9GguA3n6TYqpzXKtoXqra8AwBP04Yj7xi/Dy2h0NQdhXQINklKeBKGj4jyO1HBPvP4Ae2ljFSqijhrwe3JMqfgApXMMnjDn6zsfbl460FGyQozycpT6I5TCrEEOP7zQFP+tMTEDh8lNAy52/roCNJk1o8HRW2PBrKZP7jJvF+T5uMvJvGMa5UPtDb8Lfgl/f/ugmUjlV8TZ6n6lacQPXu/B7FtJ1iTKS7nhc5EGmMXtCI/SvbrgRuMS2gASWy1WvcV7DE6E4KrDs/qQImrjPTV1S27H4ZWa2MAA1aFF3uudoSYVN8DbSuTJolqlTlSBuvpcJMoyRz77Fyy8LFgNOeBonRJ56Km78B84qjorT938DV1C8qH1GTUFjN7m2oJQ3k926Ut+BUgmGfG6rBxhrljLfIW5/5NVV1nZ5vVzug/CterHwydJJGGT1GpRtjgCjY0HIpon40+Jn1lEtDntSjtmjKwCuZMxbOODZ0wtKnb2iqpKg==

Sorry, I was looking at the wrong file. Indeed there was a stray "*)" at the location emacs jumped to on M-x goto-char 3006.

Nevertheless, I think it may be more convenient for most users if coqdep reports a line and column number instead. Many editors don't have the "jump-to-character index" feature.

-- Abhishek

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

On Tue, Mar 3, 2020 at 10:25 AM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

I get the following error:

COQDEP VFILES
File "theories/auto/timeless.v", characters 3006-3006: Syntax error

How do I go about finding this location in the file?
I did M-x goto-char 3006 in emacs and saw nothing wrong there.
Would it be more useful for coqdep to report the line number and column number instead?

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

[Coq-Club] coqdep error locations: line+column vs character number, Abhishek Anand, 03/03/2020
- Re: [Coq-Club] coqdep error locations: line+column vs character number, Abhishek Anand, 03/03/2020