From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q4B9sJ2d005267 for ; Fri, 11 May 2012 11:54:19 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhgCAFDhrE/RVaA2imdsb2JhbABEhXauJAgiAQEBCgkNGQYjghYBAQQSAg8EGQEbHgMMBgULDwImAgIiAREBBQEcO4ddAQMLC5wiCQOLVFCCc4UfChknDVeIdgEFC4EkjF+CDoEYBIhejR+OYD2EDw X-IronPort-AV: E=Sophos;i="4.75,570,1330902000"; d="scan'208";a="157981610" Received: from mail-pb0-f54.google.com ([209.85.160.54]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-MD5; 11 May 2012 11:54:14 +0200 Received: by pbbro2 with SMTP id ro2so4054661pbb.27 for ; Fri, 11 May 2012 02:54:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type:content-transfer-encoding; bh=t+kdeeO7yuRdYcVdgLrKmUaj5Mpn5Y4jo1cy1mdQ4KE=; b=m7gucIy15fwdtIpZOtnkg2iH5TBIS2eFb3bWruQXIMTn5wXs1z79I9ZA9YQHpvNv0i YDtYn0MNr6z7QsqmxdWuuJKLshWr48diTvaDKAaYPs+1PY1YJQCV842mCm3qogsCN5uE y6XdJIiPXSAhNb/ZQQJk32OH/+XwAVC/FaH1X0snN0LiQ32bmy7w+5rj5OmHPmxKKpeu hv+kF+0TTQfZfNegntPhoiJsDTrEDqNBpmCE2jP3bLxjOPkMsEdcqb4qtpoXG3qq32Nk M1Xd/M6JAQoNRFaV1qVq1LYmI4ZXpa4ixQoFT9RYLYP3Ob2L+DzXtKCsZXx1pYZ1Ibbg ojvw== MIME-Version: 1.0 Received: by 10.68.223.231 with SMTP id qx7mr29831491pbc.134.1336730052454; Fri, 11 May 2012 02:54:12 -0700 (PDT) Received: by 10.66.46.175 with HTTP; Fri, 11 May 2012 02:54:12 -0700 (PDT) In-Reply-To: References: Date: Fri, 11 May 2012 12:54:12 +0300 Message-ID: From: Dmitry Grebeniuk To: caml-list@inria.fr Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q4B9sJ2d005267 Subject: [Caml-list] Re: ocamlbuild + Coq 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.)