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:
https://hol-theorem-prover.org/hol-mode.html
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.
-Cris
>
--
Adnan
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
