The Coq mailing list

[Ali Assaf <ali.assaf AT inria.fr>]

Hello,

I have a problem writing a coq plugin that depends on external OCaml libraries. This is the logical continuation of a previous thread called "[Coq-Club] coq_makefile and ocamlfind". Suppose I have a plugin MyPlugin that loads an ML module MyModule that depends on external libraries Lib1, Lib2, Lib3. The file MyPlugin.v looks like this:

    Declare ML Module "lib1".

    Declare ML Module "lib2".

    Declare ML Module "lib3".

    Declare ML Module "myModule".

I can successfully compile the plugin I give the proper search paths to ocamlc and coqc:

    ocamlc -I path/to/lib1 -I path/to/lib2 -I path/to/lib3 myModule.ml

    coqc -I path/to/lib1 -I path/to/lib2 -I path/to/lib3 MyPlugin.v

The problem is that I cannot load my plugin in Coq without explicitly giving the paths to the external libraries, every time I want to use it, either when calling coq:

    coqc -I path/to/lib1 -I path/to/lib2 -I path/to/lib3

or by using the Add Path commands in coq:

    Add ML Path "path/to/lib1".

    Add ML Path "path/to/lib2".

    Add ML Path "path/to/lib3".

Only then can I load the shiny new module:

    Require MyPlugin.

As you can guess, this is very cumbersome. Has anyone faced this problem before? Is there any way to solve it in a portable way (by not hardcoding the paths in MyPlugin.v)? I tried looking for a way to package the libraries with the plugin but so far I have not been successful.

Thanks,

Ali Assaf