coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Fritjof <fritjof AT uni-bremen.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Problem with defining a new vernacular command
Date: Thu, 3 May 2018 11:19:26 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=SoftFail smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT lnv-91185.sb.dfki.de
Ironport-phdr: 9a23:tTlLGxVOz3qEJcXc0phbVFWM8cbV8LGtZVwlr6E/grcLSJyIuqrYYxWAt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/ZisJ+kr9VrhGvpxNw34HbfY6bO/hlc6PBft4XX3ZNUtpNWyFDBI63cosBD/AGPeZdt4Tzp0EOrRqiBQmuA+PvxCJDi3j43a0g0uQhDQPG3AsuH98VrXTUqtT1OL4JXuCv0qbIyCvMb/VM1Tjg9ofFaxYsquyPU7Joacfd1EciGgzfgliUqIHpJS6Z2+AQv2SB8uZtVuKih3Y6pwx/rTWj3NoghpXXio4P1FzI6CZ0zJwrKdC4VUJ2Z8OvHoFKuCGALYR2R9svQ2F2tyY+zb0LoZq7fC4UyJg+wxPTduGLfouI7x75T+aeOi10i29reLK8hha+61WvxfPkWsm11lZFsDZFn8HRun0D2BHf8MyKR/pn8ku83TuDyhrf5vxHLE00jabbLoQuwr80lpodq0TDGSr2lV34jK+Md0Uk5uqo6+PpYrj9u5+cMY50hhjlPaQ0hMO/BPo3Mg4UU2eG5+uwzKfj8lHhQLVWkv02lbHUv4zdJcQCv6K2HwtV0ps45BukFDen0NEYnWEdI15feRKHiZLpO1DUL/ziA/e/mQfkrDA+zPffe7blH5/lL37Zkb6nc6wuxVRbzV8d19FD5ZVaQuUPOvPvWEj/nMHeD1ozKQGxzuChBNgrhdBWYn6GHqLMaPCailSP/O96e7DdNr9Qgy70Lr0e39CriHY4nVEHeqzwgMkKbnH9FO5rJkifJ3bh0IxYTTU6+zEmRemvs2WsFCZJbi/vDb8653QxEo+jAIGFSo3/2OXcjhf+JYVfYyV9Mn7JEXrscN/eCfMKdmfDe5Yxz3ofX/6tRYwgkx2j5lf3

On Thu, May 03, 2018 at 10:50:56AM +0200, Gaëtan Gilbert wrote:
> 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?
>

Yes it is compiled from a clean state.

foo_plugin.mllib:
Foo
G_foo

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

Whats the difference between mllib and mlpack?

> Gaëtan Gilbert
>

Best,
--f.

> 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