[Caml-list] Re: ocamlbuild + Coq

[Dmitry Grebeniuk]

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


--
Caml-list mailing list. Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Romain Bardou]

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