Re: [Caml-list] Re: ocamlbuild + Coq

[Romain Bardou <bardou@lsv.ens-cachan.fr>]

Le 11/05/2012 11:54, Dmitry Grebeniuk a écrit :
> Hello.
>
>    I've asked about ocamlbuild on irc, but without any success,
> so I'll try to ask in caml-list now.
>
>>   Has anybody tried to compile OCaml + Coq project with ocamlbuild?
>
>    Here is an attempt to make plugin:
>
> https://bitbucket.org/gds/ocamlbuild-coq-attempt
>
> , but the plugin doesn't work as expected: it fails to use rule
> "ocaml: mli ->  cmi" to produce String0.cmi from the existing
> String0.mli file.  If you run script "./run.sh" from repository,
> you'll see the problem.
>
>    ygrek gave me the idea that ocamlbuild doesn't see
> _build/String0.mli because it doesn't know that this file
> was produced by extraction (it seems that ocamlbuild
> internally stores known files from _build directory).
>    I have no way to tell ocamlbuild in advance which
> files will be produced extracting the .v file.
>    Maybe there are ways to tell ocamlbuild "just use _build
> contents without questions" or "rescan _build directory"?
> Or maybe there are other ways to deal with this issue?
>
>    (the ultimate goal of this plugin is to have source .v and .ml
> files in project's source tree, without any Coq-extracted
> intermediate .ml files, which should reside in _build.)
>
>

Hello,

I think I was once faced with a similar problem. We can tell Ocamlbuild 
when we discover new dependencies (and it will dynamically build them) 
but we cannot declare "dynamic productions", i.e. unexpected new files. 
I think I discussed this with Nicolas Pouillard at some point and he 
agreed it would be a nice addition.

Sorry I don't have any solution though :p

Cheers,

-- 
Romain Bardou