Isabelle2016 and General Information

Question

I tried to learn how to use Isabelle 2016. Although I basically like the idea of ​​checking asynchronous checks, I don’t like Isabelle / jEdit for a number of reasons, the most serious of which is that it uses too much memory (for me).

It would be great if I could use the good old proof with Isabelle 2016. I set the isa-isabelle-command variable to specify the bin/isabelle in the Isabelle mailing directory. When I start Isabelle using the General menu, Emacs freezes, and when I interrupt Cg , I get the following in the *isabelle* buffer.

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

I am aware of old posts on this site that show that the Isabel component that Proof General uses to communicate with the theorist has been removed. Is this (true) Isabelle 2016? How can I use Proof General with newer versions of Isabelle?

Answer 1

Yes, this is still the case; it has not been re-entered. I do not know how I can start PG with Isabelle later than 2014. From NEWS Isabelle2015:

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

Answer 2

Problems should be addressed where they actually occur. The Isabelle2016 Prover IDE requires even less resources - this has been a common theme in recent years. When Proof General came out in 1998, it was really huge and bold for its time. In comparison, Isabelle / jEdit is quite lightweight: it should work smoothly on ordinary consumer computers with 8 GB of memory.

It is likely that you are using Linux x86_64 and do not install the 32-bit standard C / C ++ libraries, as indicated by the Isabelle installation . Omitting this, doubles the ML heap requirements without doing anything good.