coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about writing plugins/vercular commands extension

From: Talia Ringer <tringer AT cs.washington.edu>
To: Coq-Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Question about writing plugins/vercular commands extension
Date: Fri, 31 Jan 2020 10:21:00 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=None smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-io1-f65.google.com
Ironport-phdr: 9a23:sjtBixxIz8cnXQXXCy+O+j09IxM/srCxBDY+r6Qd2+sTIJqq85mqBkHD//Il1AaPAdyHra4cwLOO6eigATVGvc/a9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMucQam4RvJro+xhfUvndEZfldyWd0KV6OhRrx6dq88ZB5/yhMp/4t8tNLXLnncag/UbFWFiktPXov5M3suxnDTA+P6WUZX24LjBdGABXL4Q/jUJvpvST0quRy2C+BPc3rVr80Qiit771qSBDzligKMSMy/XzNhcxxiKJbpw+hpwB6zoXJboyZKOZyc6XAdt4cWGFPXNteVzZZD4yzYYsADeoPM+hboYfguVUBsQCzChOwCO710DJEmmP60K883u88EQ/GxgsgH9cWvXrKttr1MKYSXvqox6fUzDXDafxW1inn6IPVdR0hveuMXbN2ccre10YvDRjIgUmLqYD/MTKazP8Ns2ia7+pmWuKvl2knqwdrrjex28gsl5DEi4QIwV7K8iV5xZw6Jdy+SENjbt6kEYdQtyGHN4RtWM8tX2ZouCM8x7YbupC7ZDAHxIo7yxPbcfCKcIiF7gj+WOuQIDp0nnNodbK5ih2v60av0Pf8WdOx0FtSripKjN3MtncV2hzW8MeHS/998l6g2TaIygzf8+9ELEE0mKbBJJ4hxbkwlpUXsUvdBCP5hEL2jKqOekUl/Oin9fjnb634qpOAM4J4kALzP6Q0lsCiAOk1MxICUmmb9Oik0b3s50z5QLFEjv0slanZtYjXJdgBpq64BQ9V3Zgs6wykAji6y9QUh3cGI0heeBKHjojpPV7OIOz/Dfe5mVijjipkx+3eMr37HprNNmTDkKvmfbtl90FczxMzwclD6JJQF7EOO+n+WlTxtdzdFh82KRa4w+fhCNVn14MRQ3iDAqGDMPCajVjdzeU2ZsKIeYVd7D36Mr0u4+PkpX4/g14UO6ezi8g5cne9S8hvJ0SQKUDthNgMCy9eohA/SuPnknWJSnhMbm2yXqQz+jY9To+qENGQFciWnLWd0XLjTdVtbWdcBwXUSCa6R8C/Q/4JLRmqDIpkmz0AW6KmTtZwhxq18hDz0LpmKOXI/SteuJ7+hoAsur/j0Coq/DkxNPyzlmGAS2YuwzENTj4ymaF4+AlzlArF3q9/jPhVU9dU4qERC1toBdvn1+V/TuvKdEfZZN7QGQStWZO5CCoxT9Q+39gIJUtxBof6gw==

In that case, if you suspect it's an import, perhaps try copying the imports from the 8.9 version of the file you linked to: https://github.com/coq/coq/blob/v8.9/plugins/ltac/g_ltac.ml4

Perhaps something moved between 8.9 and 8.10? Just a guess, again. For example, the old file has:

open Vernac_classifier

while the new file does not.

On Fri, Jan 31, 2020 at 10:08 AM Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com> wrote:

On Jan 31, 2020, at 12:55 PM, Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com> wrote:

Ah, that’s an interesting observation. My file is an .ml4 file (which seems deprecated for this purpose, but I never knew until now) and the syntax is exactly the syntax that I use in the file (in fact the {} syntax gives me a syntax error in .ml4). But I’ll try to change it to .mlg and see if that works.
My file is an .ml4 file (which seems deprecated for this purpose, but I never knew until now) and the syntax is exactly the syntax that I use in the file (in fact the {} syntax gives me a syntax error in .ml4).

Actually, it seems that for the version of Coq that we’re using (8.9.1) there’s support for .ml4 files only.

[Coq-Club] Question about writing plugins/vercular commands extension, Zoe Paraskevopoulou, 01/30/2020
- Re: [Coq-Club] Question about writing plugins/vercular commands extension, Talia Ringer, 01/31/2020
- Re: [Coq-Club] Question about writing plugins/vercular commands extension, Gaëtan Gilbert, 01/31/2020
  - Re: [Coq-Club] Question about writing plugins/vercular commands extension, Zoe Paraskevopoulou, 01/31/2020
    - Re: [Coq-Club] Question about writing plugins/vercular commands extension, Zoe Paraskevopoulou, 01/31/2020
      - Re: [Coq-Club] Question about writing plugins/vercular commands extension, Talia Ringer, 01/31/2020
        
        Re: [Coq-Club] Question about writing plugins/vercular commands extension, Zoe Paraskevopoulou, 01/31/2020