English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
[Caml-list] Dumping the OCaml state
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2004-08-31 (09:04)
From: Basile Starynkevitch [local] <basile.starynkevitch@i...>
Subject: Re: [Caml-list] Dumping the OCaml state
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