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?
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.