Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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: -- (:)
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
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

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 - temporarily --- all opinions are only mine 

To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: