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 VAA28011; Tue, 31 Aug 2004 21:53:38 +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 VAA29363; Tue, 31 Aug 2004 21:53:36 +0200 (MET DST) Received: from fmsfmr004.fm.intel.com (fmr11.intel.com [192.55.52.31]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id i7VJrZ2h000711; Tue, 31 Aug 2004 21:53:36 +0200 Received: from petasus.fm.intel.com (petasus.fm.intel.com [10.1.192.37]) by fmsfmr004.fm.intel.com (8.12.9-20030918-01/8.12.9/d: major-outer.mc,v 1.15 2004/01/30 18:16:28 root Exp $) with ESMTP id i7VJtrrg030075; Tue, 31 Aug 2004 19:55:53 GMT Received: from orsmsxvs041.jf.intel.com (orsmsxvs041.jf.intel.com [192.168.65.54]) by petasus.fm.intel.com (8.12.9-20030918-01/8.12.9/d: major-inner.mc,v 1.11 2004/07/29 22:51:53 root Exp $) with SMTP id i7VJlnql032647; Tue, 31 Aug 2004 19:53:38 GMT Received: from orsmsx331.amr.corp.intel.com ([192.168.65.56]) by orsmsxvs041.jf.intel.com (SAVSMTP 3.1.2.35) with SMTP id M2004083112523003428 ; Tue, 31 Aug 2004 12:52:30 -0700 Received: from orsmsx407.amr.corp.intel.com ([192.168.65.50]) by orsmsx331.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.0); Tue, 31 Aug 2004 12:52:31 -0700 X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0 Content-class: urn:content-classes:message MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Subject: RE: [Caml-list] Dumping the OCaml state Date: Tue, 31 Aug 2004 12:51:49 -0700 Message-ID: <012676D607FCF54E986746512C22CE7D0FE795@orsmsx407> Thread-Topic: [Caml-list] Dumping the OCaml state Thread-Index: AcSPOaxDNEJyy/RFQ7uvRo65ancupwAWS1VQ From: "Harrison, John R" To: "Basile Starynkevitch [local]" , Cc: "Harrison, John R" X-OriginalArrivalTime: 31 Aug 2004 19:52:31.0277 (UTC) FILETIME=[0D35ADD0:01C48F94] X-Scanned-By: MIMEDefang 2.31 (www . roaringpenguin . com / mimedefang) X-Miltered: at concorde with ID 4134D73F.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 johnh:01 hol-light:01 unmaintained:01 developped:01 rectify:99 ocaml:01 ocaml:01 exists:01 dumping:04 impression:06 pressing:07 matters:07 mistaken:07 written:08 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk | If I understand well the status of HOL-light, it is an unmaintained | software written in a language which is no more developped HOL Light is actively maintained, and is used for verification here at Intel. Moreover, as Bob Solovay has already noted, an OCaml port exists. However, there has been no recent public release, so I can see how you might have got a mistaken impression. I hope to rectify this situation soon, but various more pressing matters keep arising. John. ------------------- 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