The Coq mailing list

[Fritjof Bornebusch <fritjof AT uni-bremen.de>]

On Thu, May 03, 2018 at 01:28:29PM +0200, Gaëtan Gilbert wrote:

Hi,

> 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?
>

for some reason it's working now.

The only things I changed were:
* rename file 'Make' to _CoqProject
* changed the order of files in foo_plugin.mllib - as they are in your file
* and remove: R . Foo
  from the file: Make (_CoqProject)

Can't tell what was the problem part.

> > 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.
> 

I see, thank you both for the explanation.

> 
> Gaëtan Gilbert
> 

--f.

> 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