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



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

Did you manage to sort it out with Lars already?

What exactly is your version of Kubuntu?

Technically, exit 133 of the isabelle process sounds like a crash of the Poly/ML runtime system. That might have a variety of reasons, such as bad luck in the gambling of libc/libc++ dependencies of the pre-compilied binaries of Isabelle2013. It might be also bad luck in conjunction with Emacs process management, so you should try using "isabelle jedit"; and there is also "isabelle tty".

We should probably make some videos on youtube that show quickly how certain elementary things work in Isabelle/jEdit. It is a bit like a computer game to do formal proofs.

When it starts up, you have your Scratch.thy already open, so producing the standard boilerplate should be sufficient ("theory Scratch imports Main begin ... end"). Then you type all commands into the body text, and hover over the grey squiggles to see the results (which are clickable for sledgehammer), or use the more conventional Output panel.


	Makarius




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