From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <ygrek@autistici.org>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by sympa.inria.fr (Postfix) with ESMTPS id 4DB9880208
	for <caml-list@sympa.inria.fr>; Sat,  9 Sep 2017 18:06:55 +0200 (CEST)
Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ygrek@autistici.org; spf=Pass smtp.mailfrom=ygrek@autistici.org; spf=Pass smtp.helo=postmaster@perdizione.investici.org
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  ygrek@autistici.org) identity=pra; client-ip=94.23.50.208;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="ygrek@autistici.org";
  x-sender="ygrek@autistici.org"; x-conformance=sidf_compatible
Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of
  ygrek@autistici.org designates 94.23.50.208 as permitted
  sender) identity=mailfrom; client-ip=94.23.50.208;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="ygrek@autistici.org";
  x-sender="ygrek@autistici.org";
  x-conformance=sidf_compatible; x-record-type="v=spf1"
Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of
  postmaster@perdizione.investici.org designates 94.23.50.208
  as permitted sender) identity=helo; client-ip=94.23.50.208;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="ygrek@autistici.org";
  x-sender="postmaster@perdizione.investici.org";
  x-conformance=sidf_compatible; x-record-type="v=spf1"
IronPort-PHdr: =?us-ascii?q?9a23=3AOh5wPRb8ALNlHhuxEjtd0cb/LSx+4OfEezUN459i?=
 =?us-ascii?q?sYplN5qZpsq4bnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjc?=
 =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76vnYuHUD0PA9x?=
 =?us-ascii?q?bvnuF5TJx5C83uW2vpnSeBlghTynYLo0Ig/g/ivLscxDkIR4J6V5ngrGuHZLU+?=
 =?us-ascii?q?1L2WJzOVOYnlD7/Mjmr80ryDhZp/90r50Iaq79ZaltFbE=3D?=
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BKDAAXEbRZl9AyF15cHAEBBAEBCgEBF?=
 =?us-ascii?q?wEBBAEBCgEBhBNuJ4N3kFOJcIF0mDsKI4RMTwKEC0MUAQEBAQEBAQEBAQESAQE?=
 =?us-ascii?q?BAQEIFgZXgjMigkQBBAEjHQEBOAQLCwkRAgUhAgIPSAYTihkDDQwMrHxrgieDC?=
 =?us-ascii?q?QEBBYgrAQEBBwEBAQEcAwWBDoIdggKBT4UMgliCH4MTgkIfoHmDEYRKjGkNgXu?=
 =?us-ascii?q?JWYcdlSuBOTaBLoEECEqFCR+BdHWIAwEBAQ?=
X-IPAS-Result: =?us-ascii?q?A0BKDAAXEbRZl9AyF15cHAEBBAEBCgEBFwEBBAEBCgEBhBN?=
 =?us-ascii?q?uJ4N3kFOJcIF0mDsKI4RMTwKEC0MUAQEBAQEBAQEBAQESAQEBAQEIFgZXgjMig?=
 =?us-ascii?q?kQBBAEjHQEBOAQLCwkRAgUhAgIPSAYTihkDDQwMrHxrgieDCQEBBYgrAQEBBwE?=
 =?us-ascii?q?BAQEcAwWBDoIdggKBT4UMgliCH4MTgkIfoHmDEYRKjGkNgXuJWYcdlSuBOTaBL?=
 =?us-ascii?q?oEECEqFCR+BdHWIAwEBAQ?=
X-IronPort-AV: E=Sophos;i="5.42,367,1500933600"; 
   d="scan'208";a="236890196"
Received: from perdizione.investici.org ([94.23.50.208])
  by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 09 Sep 2017 18:06:29 +0200
Received: from [94.23.50.208] (perdizione [94.23.50.208]) (Authenticated sender: ygrek@autistici.org) by localhost (Postfix) with ESMTPSA id A92CE120052
	for <caml-list@inria.fr>; Sat,  9 Sep 2017 16:06:28 +0000 (UTC)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=autistici.org;
	s=stigmate; t=1504973188;
	bh=UaqF/7fJ7rgP/7BOMRXo6e6jppJ2SB8xIPtEHp4sZUM=;
	h=Date:From:To:Subject:In-Reply-To:References;
	b=fbaX5kZJhyrijUn68WG4vXypPmAEXxwftazjB/2DR5YJYTnXCu0Ev6nvlytVGNlnf
	 oIlCDsoGytpXA7THFvREil9FyB6NnXpLXaWFG7/UyeyPw5Ewq91jxh3hEIR6rYg+bL
	 crIoiW4O0Elmgfw3/u7C9zHfq2etbB2+zHthdiVk=
Date: Sat, 9 Sep 2017 17:06:28 +0100
From: ygrek <ygrek@autistici.org>
To: caml users <caml-list@inria.fr>
Message-ID: <20170909170628.31bac90a@kiwi.local.tld>
In-Reply-To: <6543AF55-7E89-462E-8AF9-DFF3091C1599@gmx.net>
References: <6543AF55-7E89-462E-8AF9-DFF3091C1599@gmx.net>
X-Mailer: Claws Mail 3.14.1 (GTK+ 2.24.30; x86_64-pc-linux-gnu)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Subject: Re: [Caml-list] How to generate source files with ocamlbuild

On Fri, 8 Sep 2017 21:02:53 -0500
Helmut Brandl <helmut.brandl@gmx.net> wrote:

> Now I want to use coq to verify the critical part of my project and gener=
ate ocaml source files with coq. Is there a simple way to tell ocamlbuild t=
hat it has to use coq and some =E2=80=98*.v=E2=80=99 files to generate ocam=
l source files before calling the compiler?

Yes, ocamlbuild can be extended to add build rules, see https://ocaml.org/l=
earn/tutorials/ocamlbuild/Making_plugins.html
Example: https://github.com/ygrek/extunix/blob/master/myocamlbuild.ml#L920

--=20