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 LAA01151; Tue, 31 Aug 2004 11:04:14 +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 LAA01977 for ; Tue, 31 Aug 2004 11:04:14 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id i7V94Dot014530 for ; Tue, 31 Aug 2004 11:04:13 +0200 Received: from bourg.inria.fr (bourg.inria.fr [128.93.11.100]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA00270 for ; Tue, 31 Aug 2004 11:04:13 +0200 (MET DST) Received: from basile by bourg.inria.fr with local (Exim 4.34) id 1C24YJ-0005tj-9B for caml-list@inria.fr; Tue, 31 Aug 2004 11:03:43 +0200 Date: Tue, 31 Aug 2004 11:03:43 +0200 To: caml-list@inria.fr Subject: Re: [Caml-list] Dumping the OCaml state Message-ID: <20040831090343.GA22486@bourg.inria.fr> References: Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.6+20040803i From: "Basile Starynkevitch [local]" X-Miltered: at concorde with ID 41343F0D.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 basile:01 2004:99 hol-light:01 hol-light:01 developped:01 developped:01 restarted:01 unmaintained:01 prover:01 cristal:01 cristal:01 ocaml:01 ocaml:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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) > > What I would like to do is store the state [to an executable image] so > that I would not have to read in all the initialization files the next > time I run the program. {There used to be a command in Common Lisp "dump" > which would store an executable image to a file that could then be > restarted. My question is: is there something like this in OCaml.} Not in Ocaml, and probably not in CamlLight (which I don't know much). Did you consider using Coq? I don't know much of it, but it is actively worked on (by the Logical team). Perhaps Coq has some features you want. If I understand well the status of HOL-light, it is an unmaintained software written in a language which is no more developped - this seems to be two valid reasons to switch to some other prover, like Coq. See http://coq.inria.fr/ 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