Hi all,
Yong Kiam showed me something very useful today, so I'd like to share it
with you all. If you're using HOL with Poly/ML, then there are functions
PolyML.SaveState.saveState and PolyML.SaveState.loadState, both of type
string -> unit, which save the state of the REPL in a file (the string is
the filename). This can be used in the middle of an interactive proof, in
the middle of a long script file, to avoid the need to rebuild if the
session is exited (accidentally or not).
Of course this doesn't help if there are logical reasons why things need to
be rebuilt, but as long as those can be ignored...
Cheers,
Ramana
------------------------------------------------------------------------------
Slashdot TV.
Video for Nerds. Stuff that matters.
http://tv.slashdot.org/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
