[Caml-list] ocamlbuild + Coq

[Caml-list] ocamlbuild + Coq

[Dmitry Grebeniuk]

Hello.

  Has anybody tried to compile OCaml + Coq project with ocamlbuild?
Maybe you can share myocamlbuild.ml rules for such compilation?
(I already wrote simple rule on "%.v" -> "%.ml", but dependencies'
discovering is killing me, so I'm asking here, maybe there are some
ready solutions.)

  I know about coq_makefile, but I don't want to pollute source tree with
intermediate extraction results.  I could ignore/remove .vo/.glob files,
but Coq extracts some .ml files from his stdlib, so I see no sane way
to ignore some .ml files while not-ignoring other .ml files.

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

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

[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