inputs all at once.
Michael
From: Yassmeen Derhalli
Date: Friday, 21 September 2018 at 08:11
To: Thomas Tuerk
Cc: "hol-info@lists.sourceforge.net"
Subject: Re: [Hol-info] Exception raised while using HOL in hol-mode
Hi,
thank you for your reply.
I am using an oracle virtual machine on
Hi,
thank you for your reply.
I am using an oracle virtual machine on my laptop
running ubuntu-16.04.4-desktop-i386. I have been using this machine for
about three months now, and I have not had any problem until yesterday.
Best Regards,
Yassmeen
On Thu, Sep 20, 2018 at 5:25 PM, Thomas Tuerk
Hi,
I believe this is due to how hol-mode copies input from emacs buffers to
HOL. Look at HOL-DIR/tools/hol-mode.el line 802 ff.
(https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools/hol-mode.src#L800).
If a chunk of text you want to send exceeds a certain size, it is
written to a temp-file
