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 LAA03680; Tue, 31 Aug 2004 11:12:00 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA01828; Tue, 31 Aug 2004 11:11:59 +0200 (MET DST) Received: from mail.math.berkeley.edu (mail.math.Berkeley.EDU [169.229.58.57]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id i7V9Bvxr025521 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Tue, 31 Aug 2004 11:11:59 +0200 Received: from blue1.Math.Berkeley.EDU (IDENT:2040@blue1.Math.Berkeley.EDU [169.229.58.58]) by mail.math.berkeley.edu (8.12.11/8.12.11) with ESMTP id i7V9Bubt084777; Tue, 31 Aug 2004 02:11:56 -0700 (PDT) (envelope-from solovay@math.berkeley.edu) Received: from localhost (solovay@localhost) by blue1.Math.Berkeley.EDU (8.12.10+Sun/8.12.10/Submit) with ESMTP id i7V9BuP8012602; Tue, 31 Aug 2004 02:11:56 -0700 (PDT) X-Authentication-Warning: blue1.Math.Berkeley.EDU: solovay owned process doing -bs Date: Tue, 31 Aug 2004 02:11:56 -0700 (PDT) From: "Robert M. Solovay" X-X-Sender: solovay@blue1 To: "Basile Starynkevitch [local]" cc: caml-list@inria.fr Subject: Re: [Caml-list] Dumping the OCaml state In-Reply-To: <20040831090343.GA22486@bourg.inria.fr> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Scanned-By: MIMEDefang 2.44 X-Miltered: at nez-perce with ID 413440DD.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 basile:01 2004:99 hol-light:01 hol-light:01 developped:01 developped:01 basile:01 bug:01 faq:01 faq:01 beginner's:01 beginners:01 bin:01 cristal:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Tue, 31 Aug 2004, Basile Starynkevitch [local] wrote: > On Mon, Aug 30, 2004 at 11:57:05AM -0700, Robert M. Solovay wrote: > > > > I am using the HOL-light proof verifier which is written in OCaml. > > If you are talking about http://www.cl.cam.ac.uk/users/jrh/hol-light/ > then it is written in CamlLight, not Ocaml. HOL-light does not seems > to be actively developped (but I don't know really and may be wrong). > CamlLight is somehow an ancestor of Ocaml, and it is not, as far as I > know, actively worked upon. The Cristal team actively work on Ocaml > and Caml Light is no more developped (but has gotten minor maintanance > fixes sometimes) The version I have of HOL -light [obtained from Harrison in private correspondence] is ported to OCaml. The interest of HOL-light [for me] is that it's what is currently being used in the Flyspeck project of Tom Hales. --Bob Solovay > > Take everything above with a grain of salt. I don't know really > HOL-light & Caml-light. > > -- > Basile STARYNKEVITCH -- basile dot starynkevitch at inria dot fr > Project cristal.inria.fr - temporarily > http://cristal.inria.fr/~starynke --- all opinions are only mine > > ------------------- > 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 > ------------------- 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