coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with defining a new vernacular command

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Problem with defining a new vernacular command
Date: Thu, 3 May 2018 10:50:56 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay10.mail.gandi.net
Ironport-phdr: 9a23:2VWt1Rd2EsaumA8hR6GTbuKZlGMj4u6mDksu8pMizoh2WeGdxcuyZB7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM37X/ZisJwgqxYrhyuqRNwzIzIb4+aL/d+YqDQcMkGSWZdUMtcVSpMCZ68YYsVCOoBOP5VoYjnqFwSsRuxHw+sC/vuxD9Jgn/5xrM10/49EQrb2wEgEMgBv2rIrNrvMqceS++1zKjMzTrYcfxWwyv95ZPTchAiofCMRrFwccvUyUkqCQzFlE+cqYr7MDOJz+kAtXWQ4el4Ve+3lWIrtgN8riKty8swkIXFm4AYx1Pe+Slnzos5OcW0RU9lbdK+DZdcqz+WO5FrTs4tQGxkojs2x74GtJO9YSME0o4oxwTFZPyCa4WI4gzsVOKWITpgnnJqZra/iAyy8ES91uHwTMy030xLripBiNXMuWoC1xrO5ciGUPd9+Fmu2SqX2wDS7OFLP1w0mLLFJ5I8wLM8jJgevVjZEiPrmkj7j7Waelsq9+S08+jnZ6/ppp6YN496kAH+NaEul9SwAesiLAcOQ3KU+eKm2L3s/E35RK5FgeMskqnFq53aPscbp66iAw9W04Yj7hO/ACm80NgCm3kIMk5FdAqdj4f1I1HOPOz4DfCnjluwlzdr3unKMaHlApXQNXfOi6zhfLZ4605E0gU/19Ff55ROCrEAOv3/QEHxtMaLRiM+Zgez2qPsDMh3/oIYQ2OGRKGDY43ItlrdyeusP+CKU6AUvDzwMeRts/HngGMwnxkSfK2j0IELQGu7D+9lIkCcbGCqhNodRzRZ9jEiRfDn3QXRGQVYYGy/Cvplt2MLTbm+BIKGfbiDxbmI3SO1BJpTPz4UEVOdCnTpcoCJQbEKZT7Ae5Y9wAxBbqCoTsoa7T/rrBXzkuQ1NenF4S4ZsJfuzp5z6vGBzUhvpwwxNNyU1iS2d08xnm4MQGVqjrpypUVskw/F1KF5h7pXHNpf5rVPXxtobZM=

Is that make from a clean state? If it is then notice that it's not compiling foo.ml and g_foo.ml4. What's the content of foo_plugin.mllib?

NB: nowadays we recommend using foo_plugin.mlpack but I don't think that's causing the error

Gaëtan Gilbert

On 03/05/2018 09:33, Fritjof wrote:

Hi,

I have a problem defining a new vernacular since Coq 8.8.0 - I guess.
I think in a previous version this worked.

g_foo.ml4:
DECLARE PLUGIN "foo_plugin"

VERNAC COMMAND EXTEND FooBar CLASSIFIED AS QUERY
| [ "Foo" "Bar" ] -> [ Foo.bar () ]
END

Coqtop:
Coq < Declare ML Module "foo_plugin".
[Loading ML file foo_plugin.cmxs ... done]

Coq < Foo Bar.
Toplevel input, characters 0-3:

Foo Bar.
^^^

Error: Syntax error: illegal begin of vernac.

$ make
COQDEP VFILES
COQDEP foo_plugin.mllib
CAMLDEP foo.ml
CAMLDEP -pp g_foo.ml4
CAMLOPT -a -o foo_plugin.cmxa
CAMLOPT -shared -o foo_plugin.cmxs

make(1) runs with no errors.

Does anyone have a hint, why "Foo Bar." does not work, even if I defined it
and make(1)
processes the grammar file?

Best,
--f.

[Coq-Club] Problem with defining a new vernacular command, Fritjof, 05/03/2018
- Re: [Coq-Club] Problem with defining a new vernacular command, Gaëtan Gilbert, 05/03/2018
  - Re: [Coq-Club] Problem with defining a new vernacular command, Fritjof, 05/03/2018
    - Re: [Coq-Club] Problem with defining a new vernacular command, Gaëtan Gilbert, 05/03/2018
      - Re: [Coq-Club] Problem with defining a new vernacular command, Emilio Jesús Gallego Arias, 05/03/2018
      - Re: [Coq-Club] Problem with defining a new vernacular command, Fritjof Bornebusch, 05/04/2018