Re: [isabelle] trouble with sledgehammer/ProofGeneral in Isabelle2013



On Wed, 20 Mar 2013, Makarius wrote:

On Mon, 18 Mar 2013, Randy Pollack wrote:

I just switched to Isabelle2013.  If sledgehammer returns a proof "try
...",  I see this proof message in the response buffer for second,
then "Process isabelle exited abnormally with code 133, shutting down
scripting.

I'm using Isabelle2013 64 bit, Kubuntu

The conclusion that was found privately is: Emacs 24 fails, Emacs 23.4.1 works, both with Proof General 4.2 or 4.1. So just a good old Emacs-induced crash.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.