Email Gateway (Aug 19 2022 at 10:31): Email Gateway (Aug 19 2022 at 10:31):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Hi,
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, ProofGeneral 4.1, emacs
23.4.1. Same problem with PG 4.2 and with emacs 24.
Works with Isabelle2012 package; also works in Isabelle2012 using PG
4.2 and emacs 24.
Other users must have used sledgehammer in ProofGeneral, so I must be
doing something wrong, but what?
Thanks for any help,
Randy
Email Gateway (Aug 19 2022 at 10:32):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 10:33):From: Makarius <makarius@sketis.net>
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
Last updated: May 06 2024 at 16:21 UTC