Hi John and Cris,

Many thanks for your responses.

On Tue, Oct 18, 2016 at 4:25 AM, Cris Perdue <c...@perdues.com> wrote:

> On Sun, Oct 16, 2016 at 12:44 PM, <john.harri...@cl.cam.ac.uk> wrote:
>> Hi Adnan,
>> | I have another query. Can anybody know the way to reduce the loading
>> time
>> | of HOL-Light theories?
>> If you are using some version of Linux there are checkpointing options,
>> as explained in the README file. Personally I tend to just have a few
>> HOL Light sessions open. I agree this is somewhat inconvenient though.
Checkpointing options are good to go with, in order to avoid loading
theories each time.

>> John.
> Correct me if I'm wrong, but the last I looked, the checkpointing could
> only work in versions of Linux that are now several years old.
> Another option that does work is to use machine virtualization software
> such as VirtualBox to create a Linux environment you can start under
> Windows, Mac, or even Linux, load your preferred theories into HOL Light
> within that VirtualBox environment, and then save the state of the virtual
> machine into a snapshot on disk.  You can restart the snapshot at any time,
> which for me is a lot quicker than reloading theories.

VirtualBox is another good alternative and right now, I am using this
option. But again, sometime, I want to load theories and I was searching
for some permanent solution.

In HOL4, there are some commands in the Emacs mode, which are documented at:


By using those, one can quickly load the theories without printing each of
the theorem on the screen, which takes a lot of time.

So I was basically searching for something like that. But, currently, I
have to go with one of the above alternatives.

Thanks again.



Check out the vibrant tech community on one of the world's most 
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
hol-info mailing list

Reply via email to