The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

> I have extracted a program that uses Coq.Lists.List. I am linking this
> against an OCaml program that uses the OCaml stdlib (actually not even
> using stdlib's List, although I want to); I get the following error:
> Files list.cmx
> and /Users/jay/Development/dists/ocaml/godi/lib/ocaml/std-lib/stdlib.cmxa
> both define a module named List
>
> Does anyone know the appropriate magic to get this to work?

Here are two suggestions.

1- Post-extraction rewriting.  After generating the extracted Caml
files, do

     mv list.ml coqlist.ml
     mv list.mli coqlist.mli
     perl -pi 's/\bList\b/Coqlist/g;' <all extracted .ml and .mli files>

Then compile as usual.  Not pretty, but you can hide this in a
Makefile.

2- OCaml kung-fu.  Put your extracted Caml files and your hand-written
Caml files in two different directories, say ./extr and ./caml.  Then:

- In ./extr, compile all files with ocamlopt -for-pack Extracted -c

- Still in ./extr, "pack" those files together:
      ocamlopt -pack -o ../caml/Extracted.cmx <.cmx for extracted files>

- In ./caml, compile your hand-written Caml code normally.  Remember
  to refer to a module A extracted from Coq not as "A" but as "Extracted.A".

- Link with
       ocamlopt -o myprog extracted.cmx <.cmx for hand-written files>

Solution 2 is cleaner but will not work if you have complex
dependencies between hand-written and extracted modules.
(E.g extracted module A refers to hand-written Caml module B,
because a Parameter in A is implemented by a function in B, and B
itself refers to an extracted module C.)

Hope this helps,

- Xavier Leroy