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
RE: [Caml-list] toplevel with pre-installed printers
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2006-01-20 (20:19)
From: Harrison, John R <johnh@i...>
Subject: RE: [Caml-list] toplevel with pre-installed printers
| Under "Linux" ckpt is not available. I tried this, since HOL Light
| ages to load. I even tried to build ckpt from source with no luck.
| Maybe it works for x86 .. but I'm running an x86_64.

I wasn't aware of that problem. It works fine on 32-bit x86, though
are some peculiarities of certain Linux variants. I'll look into this,
since I suppose I'll want it myself one day.

| Is there some reason HOL Light doesn't load bytecode?

It's not so much the code (of automated proof procedures etc.) that
the load down, but actually running the proofs to arrive at the basic
core of theorems. Loading as bytecode won't help that significantly.

It would be possible to restructure the code to completely separate data
(theorems) from code (proof procedures), load the former via marshalling
and the latter as bytecode. But it's not very natural to do so, since
often wants to introduce theorems and proof procedures in a tightly
interleaved manner.