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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and