From mboxrd@z Thu Jan 1 00:00:00 1970 X-Sympa-To: caml-list@inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q4BAMD4X006984 for ; Fri, 11 May 2012 12:22:13 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsIBADznrE8uaUskmWdsb2JhbABEhXauTwEBAQEBCAsLGyeCFgEFIwQLAQVAEQsaAgUWCwICCQMCAQIBRRMIAheHcwQHqA6TCoEviWiCd4IOgRgEqSg X-IronPort-AV: E=Sophos;i="4.75,570,1330902000"; d="scan'208";a="143457798" Received: from 2.mo3.mail-out.ovh.net (HELO mo3.mail-out.ovh.net) ([46.105.75.36]) by mail4-smtp-sop.national.inria.fr with ESMTP; 11 May 2012 12:22:08 +0200 Received: from mail176.ha.ovh.net (b9.ovh.net [213.186.33.59]) by mo3.mail-out.ovh.net (Postfix) with SMTP id C04B4FFA147 for ; Fri, 11 May 2012 12:24:29 +0200 (CEST) Received: from b0.ovh.net (HELO queueout) (213.186.33.50) by b0.ovh.net with SMTP; 11 May 2012 12:22:07 +0200 Received: from biscottino.dsi.unive.it (HELO ?157.138.20.231?) (romain%bardou.fr@157.138.20.231) by ns0.ovh.net with SMTP; 11 May 2012 12:22:04 +0200 Message-ID: <4FACE84B.7040201@lsv.ens-cachan.fr> Date: Fri, 11 May 2012 12:22:03 +0200 From: Romain Bardou User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.3) Gecko/20120329 Icedove/10.0.3 MIME-Version: 1.0 To: caml-list@inria.fr X-Ovh-Mailout: 178.32.228.3 (mo3.mail-out.ovh.net) References: In-Reply-To: Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit X-Ovh-Tracer-Id: 16738753915469879072 X-Ovh-Remote: 157.138.20.231 (biscottino.dsi.unive.it) X-Ovh-Local: 213.186.33.20 (ns0.ovh.net) X-OVH-SPAMSTATE: OK X-OVH-SPAMSCORE: 15 X-OVH-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrfeegjedrtddtucetufdoteggodetrfdofgetucfrrhhofhhilhgvmecuqfggjfenuceurghilhhouhhtmecufedttdenucgfrhhlucfvnfffucdludehmdenucfhrhhomheptfhomhgrihhnuceurghrughouhcuoegsrghrughouheslhhsvhdrvghnshdqtggrtghhrghnrdhfrheqnecuffhomhgrihhnpegsihhtsghutghkvghtrdhorhhgnecujfgurhepkfffhfgfggfvufhfjggtgfesthekrgdttdefje X-Spam-Check: DONE|U 0.5/N X-VR-SPAMSTATE: OK X-VR-SPAMSCORE: 15 X-VR-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrfeegjedrtddtucetufdoteggodetrfdofgetucfrrhhofhhilhgvmecuqfggjfenuceurghilhhouhhtmecufedttdenucgfrhhlucfvnfffucdludehmdenucfhrhhomheptfhomhgrihhnuceurghrughouhcuoegsrghrughouheslhhsvhdrvghnshdqtggrtghhrghnrdhfrheqnecuffhomhgrihhnpegsihhtsghutghkvghtrdhorhhgnecujfgurhepkfffhfgfggfvufhfjggtgfesthekrgdttdefje X-Validation-by: bardou@lsv.ens-cachan.fr Subject: Re: [Caml-list] Re: ocamlbuild + Coq 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