On 6/11/2012 12:26 PM, Konrad Slind wrote:
> On Mon, Jun 11, 2012 at 1:12 AM,<[email protected]> wrote:
> On windows I usually run HOL4 under emacs. But of course that's
> just personal preference.
I tried to load hol-mode.el in xemacs running under Cygwin, but I
couldn't get it to work.
>> 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).
I just meant that it takes 15 seconds for HOL4 to load after the console
window comes up. If it takes me 5 seconds to edit a script, and I run it
40 times, 15 seconds is a long time to wait.
I've figured out my solution: start 3 HOL4 sessions at a time so I don't
have to wait after a session goes bad.
> Send (or post) a minimal failing version and the maintainers can help
> you.
I thought it was me causing problems by loading my own scripts after
"HOL/examples/euclid.sml", but it wasn't.
I don't really care about these errors, since it's not my fault, but
here's the input and output (I typed it by hand, so there might be some
errors):
- use "E:/E_main2/binp/HOL4k7/examples/euclid.sml";
...goes through the proof
> val EUCLID_AGAIN = |- !n. ?p. n < p /\ prime p : thm
[closing file "C:\Users\jv\AppData\Local\Temp\mosml68.hol"]
> val it = () : unit
- use "E:/E_main2/binp/HOL4k7/examples/euclid.sml";
[opening file "C:\Users\jv\AppData\Local\Temp\mosml69.hol"]
on line 23, characters 3-13:
No rule for [divides, TM]
Exception raised at Absyn.Absyn:
on line 23, characters 3-31:
No rule for [divides, TM]
! Uncaught exception:
! HOL_ERR
[closing file "C:\users\jv\AppData\Local\Temp\mosml69.hol"]
-
Konrad, thanks for the information.
--GB
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
