The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Tue, 10 Jun 2003, David Pichardie wrote:

> Hi,
>
> I don't manage to extract module. Here is a simple example :
>
> ---- coq file ---
>
> Module Bob.
>
> Definition t:=nat.
> Definition x:t := O.
>
> End Bob.
>
> Extraction Module Bob.
>
> ---- end coq file ---
>
> Ok but now, where is Bob.ml ?
>
> Best regards,
>
> David.

Ok, it's not a bug, but a really inadequate feature. I have already
had some feedback like yours concerning Extraction Module not working.

The trouble is that Extraction Module come from a time where a Coq
module can only be a *.v(o) file. The semantics of Extract Module foo_bar
was to take the whole contain of a foo_bar.vo, extract it, and put it in
foo_bar.ml.

In your example, Bob isn't a *.vo, so it does nothing (strange it doesn't
complain...)

The workaround for Coq 7.4 is either:
- to extract something INSIDE the module. Then the whole module will be
extracted. Here you can do a 'Extraction "bob.ml" Bob.x'. Dirty, isn't it?

- to put your module in a toto.v file, compile toto.v, and in a new
session, do a 'Require toto. Extraction Module toto.' This will produce a
toto.ml with module Bob inside.

I apologize for this mess, but the fact is that extraction of Coq new
modules was ready only a few days before the 7.4 release, so I hadn't have
time to make them user-friendly. I'm currently working on it (changing
command names and/or semantics).

Pierre Letouzey