From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id HAA28866; Sat, 19 Jun 2004 07:59:35 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id HAA28857 for ; Sat, 19 Jun 2004 07:59:34 +0200 (MET DST) Received: from nexus.stwing.upenn.edu (NEXUS.STWING.UPENN.EDU [165.123.132.61]) by concorde.inria.fr (8.12.10/8.12.10) with ESMTP id i5J5xWSH015513 for ; Sat, 19 Jun 2004 07:59:33 +0200 Received: from force.stwing.upenn.edu (force.stwing.upenn.edu [165.123.132.65]) by nexus.stwing.upenn.edu (8.12.10/8.12.9) with ESMTP id i5J5xVfn016099 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Sat, 19 Jun 2004 01:59:31 -0400 (EDT) Received: from force.stwing.upenn.edu (localhost [127.0.0.1]) by force.stwing.upenn.edu (8.12.10/8.12.9) with ESMTP id i5J5xUhs009908 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Sat, 19 Jun 2004 01:59:31 -0400 (EDT) Received: (from wlovas@localhost) by force.stwing.upenn.edu (8.12.10/8.12.9/Submit) id i5J5xUZl009907 for caml-list@inria.fr; Sat, 19 Jun 2004 01:59:30 -0400 (EDT) Date: Sat, 19 Jun 2004 01:59:30 -0400 From: William Lovas To: caml-list@inria.fr Subject: Re: [Caml-list] installing caml-light Message-ID: <20040619055929.GA7685@force.stwing.upenn.edu> Mail-Followup-To: caml-list@inria.fr References: Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.4i X-Miltered: at concorde with ID 40D3D644.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; lovas:01 wlovas:01 stwing:01 caml-list:01 2004:99 maggesi:01 hol-light:01 prover:01 ocaml:01 ocaml:01 caml:01 caml:01 compile:02 pointer:03 wrote:03 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Hi Marco, On Fri, Jun 18, 2004 at 04:44:00PM +0000, Marco Maggesi wrote: > The only reason I have to compile Caml-light is that I would like to > give a try to HOL-light, the prover of John Harrison. How hard is to > translate a Caml-light program into an OCaml program? You might be interested in the last question answered at http://caml.inria.fr/ocaml/bigpicture.html entitled, "How hard is it to convert code from Caml Light to Objective Caml?" It even has a pointer to an automatic translator! Hope this helps. cheers, William ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners