The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

I can't reproduce.
If you try with the files I attached does the error still happen for 
you? If so can you spot any difference with your files?

> Whats the difference between mllib and mlpack?

Suppose we have foo.mllib containing Bar and Baz (on separate lines as 
usual)
Then compilation depends on those modules and will produce a binary 
called foo.cm* (depending on native vs byte etc). Linking that gives 
access to the modules Bar and Baz.
If instead we use foo.mlpack then linking the resulting foo gives access 
to Foo.Bar and Foo.Baz.

Using mlpack avoids name collisions (you can have 2 modules called Foo 
so long as they're in different packs) and helps enforce modularity 
(dependencies between packs must be acyclic, so eg if you have 1 pack 
per directory you control dependencies between directories)

Emilio might have more to say about this / I might have misunderstood 
something or said something unclear.


Gaëtan Gilbert

On 03/05/2018 11:19, Fritjof wrote:
> 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.
foo.ml
g_foo.ml4
foo_plugin.mllib


let bar () = ()
Foo
G_foo

DECLARE PLUGIN "foo_plugin"

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