| Under "Linux" ckpt is not available. I tried this, since HOL Light
takes
| 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
there
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
slows
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
one
often wants to introduce theorems and proof procedures in a tightly
interleaved manner.

John.