* [Caml-list] Dumping the OCaml state
@ 2004-08-30 18:57 Robert M. Solovay
2004-08-31 9:03 ` Basile Starynkevitch [local]
0 siblings, 1 reply; 6+ messages in thread
From: Robert M. Solovay @ 2004-08-30 18:57 UTC (permalink / raw)
To: caml-list
I am using the HOL-light proof verifier which is written in OCaml.
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.}
Thank you.
--Bob Solovay
-------------------
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
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Dumping the OCaml state
2004-08-30 18:57 [Caml-list] Dumping the OCaml state Robert M. Solovay
@ 2004-08-31 9:03 ` Basile Starynkevitch [local]
2004-08-31 9:11 ` Robert M. Solovay
0 siblings, 1 reply; 6+ messages in thread
From: Basile Starynkevitch [local] @ 2004-08-31 9:03 UTC (permalink / raw)
To: caml-list
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
^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: [Caml-list] Dumping the OCaml state
2004-08-31 9:03 ` Basile Starynkevitch [local]
@ 2004-08-31 9:11 ` Robert M. Solovay
0 siblings, 0 replies; 6+ messages in thread
From: Robert M. Solovay @ 2004-08-31 9:11 UTC (permalink / raw)
To: Basile Starynkevitch [local]; +Cc: caml-list
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
^ permalink raw reply [flat|nested] 6+ messages in thread
* RE: [Caml-list] Dumping the OCaml state
2004-09-29 23:56 Harrison, John R
@ 2004-09-30 0:14 ` Igor Pechtchanski
0 siblings, 0 replies; 6+ messages in thread
From: Igor Pechtchanski @ 2004-09-30 0:14 UTC (permalink / raw)
To: Harrison, John R; +Cc: caml-list
On Wed, 29 Sep 2004, Harrison, John R wrote:
> Bob Solovay wrote:
>
> | 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.
>
> As Carl Witty pointed out to me recently, there are quite a few
> checkpointing programs that can dump an arbitrary process so that
> it can be restarted later in the same state. I've recently been
> using "ckpt" to save an OCaml toplevel session with HOL Light
> preloaded, and it works very well. Maybe other OCaml users would
> find the same thing useful. See:
>
> http://www.cs.wisc.edu/~zandy/ckpt/
>
> The only drawback is that this program is Linux-specific. There's
> a long list of alternatives at http://www.checkpointing.org, but I
> haven't found a suitable one for Windows. If anybody knows of one
> (even if it only works under Cygwin) I'd be very interested.
>
> John.
Have you tried Cygwin's /bin/dumper.exe?
Igor
--
http://cs.nyu.edu/~pechtcha/
|\ _,,,---,,_ pechtcha@cs.nyu.edu
ZZZzz /,`.-'`' -. ;-;;,_ igor@watson.ibm.com
|,4- ) )-,_. ,\ ( `'-' Igor Pechtchanski, Ph.D.
'---''(_/--' `-'\_) fL a.k.a JaguaR-R-R-r-r-r-.-.-. Meow!
"Happiness lies in being privileged to work hard for long hours in doing
whatever you think is worth doing." -- Dr. Jubal Harshaw
-------------------
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
^ permalink raw reply [flat|nested] 6+ messages in thread
* RE: [Caml-list] Dumping the OCaml state
@ 2004-09-29 23:56 Harrison, John R
2004-09-30 0:14 ` Igor Pechtchanski
0 siblings, 1 reply; 6+ messages in thread
From: Harrison, John R @ 2004-09-29 23:56 UTC (permalink / raw)
To: caml-list; +Cc: Harrison, John R
Bob Solovay wrote:
| 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.
As Carl Witty pointed out to me recently, there are quite a few
checkpointing programs that can dump an arbitrary process so that
it can be restarted later in the same state. I've recently been
using "ckpt" to save an OCaml toplevel session with HOL Light
preloaded, and it works very well. Maybe other OCaml users would
find the same thing useful. See:
http://www.cs.wisc.edu/~zandy/ckpt/
The only drawback is that this program is Linux-specific. There's
a long list of alternatives at http://www.checkpointing.org, but I
haven't found a suitable one for Windows. If anybody knows of one
(even if it only works under Cygwin) I'd be very interested.
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
^ permalink raw reply [flat|nested] 6+ messages in thread
* RE: [Caml-list] Dumping the OCaml state
@ 2004-08-31 19:51 Harrison, John R
0 siblings, 0 replies; 6+ messages in thread
From: Harrison, John R @ 2004-08-31 19:51 UTC (permalink / raw)
To: Basile Starynkevitch [local], caml-list; +Cc: Harrison, John R
| 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
^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2004-09-30 0:14 UTC | newest]
Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2004-08-30 18:57 [Caml-list] Dumping the OCaml state Robert M. Solovay
2004-08-31 9:03 ` Basile Starynkevitch [local]
2004-08-31 9:11 ` Robert M. Solovay
2004-08-31 19:51 Harrison, John R
2004-09-29 23:56 Harrison, John R
2004-09-30 0:14 ` Igor Pechtchanski
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).