Isabelle2016 and Proof General

Question

I've been trying to learn to use Isabelle 2016. While in principle I like the idea of asynchronous proof checking, I don't like Isabelle/jEdit for a number of reasons, the most severe of which is that it uses too much memory (for me).

It'd be great if I could use the good old Proof General with Isabelle 2016. I set the variable isa-isabelle-command to point the file bin/isabelle under the Isabelle distribution directory. When I start Isabelle using Proof General's menu, Emacs hangs, and when I interrupt it by C-g, I get the following in *isabelle* buffer.

 > val it = (): unit
 ^BException- ERROR "Bad socket name: \"I\"" raised

I am aware of old postings on this site which suggest that the component of Isabelle that Proof General uses to communicate with the theorem prover was removed. Is this (still) true of Isabelle 2016? How can I use Proof General with newer versions of Isabelle?

Answer 1

Yes, it is still true; it hasn't been reintroduced. There is no way that I am aware of to run PG with Isabelle later than 2014. From the NEWS of Isabelle2015:

* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.

Answer 2

Problems should be solved where they actually occur. The Prover IDE in Isabelle2016 requires once again less resources -- that has been a common theme in recent years. When Proof General came out in 1998, it was really huge and fat for its time. In comparision Isabelle/jEdit is rather light: it should work smoothly on regular consumer machines with only 8 GB memory.

There is some chance that you are using Linux x86_64 and did not install the 32-bit C/C++ standard libraries as mentioned on the Isabelle installation page. Omitting that, doubles the ML heap requirements without doing any good.