On Mon, Jun 11, 2012 at 1:12 AM, <gottfried.bar...@gmx.com> wrote: > I'm using HOL4 in the Windows console. I load a file using the "use" > command, like this: > > use "E:/E_main2/binp/HOL4k7/examples/euclid.sml"; >
On windows I usually run HOL4 under emacs. But of course that's just personal preference. > I then edit some ML scripts in an editor and load them into HOL4 using > the "use" command. My scripts get errors, so when I try to load > "euclid.sml" again as shown above, I get errors in HOL4 which I didn't > get before. Most operations in HOL4 have been designed to be idempotent, i.e., if you call them once without error, you should be able to call them again without error (and get the same result!). However, HOL4 does have some internal state which can get muddled by re-invocations. In some cases, this has to do with the HOL4 grammar. SML itself can fail on re-invocation, typically with "infix" declarations. Send (or post) a minimal failing version and the maintainers can help you. > I close the HOL4 window, and then start HOL4 again, but it doesn't start > up instantly. I haven't encountered this problem (on XP). > Is there a command I can use to reinitialize HOL4 without closing it and > restarting it? I don't think so. Cheers, Konrad. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
