Isabelle2016 und Proof General

Question

Ich habe versucht, Isabelle 2016 zu lernen. Während ich grundsätzlich die Idee der asynchronen Proofüberprüfung mag, mag ich Isabelle/jEdit nicht aus einer Reihe von Gründen, von denen die schwerwiegendsten sind ist, dass es zu viel Speicher verwendet (für mich).

Es wäre toll, wenn ich den guten alten Proof General mit Isabelle 2016 verwenden könnte. Ich setze die Variable isa-isabelle-command, um die Datei bin/isabelle unter dem Isabelle-Distributionsverzeichnis zu zeigen. Wenn ich Isabelle mit Proof General's Menü starte, hängt Emacs, und wenn ich es unter C-g abbringe, bekomme ich folgendes in *isabelle* Puffer.

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

Ich bin mir bewusst, alter Nachrichten auf dieser Seite, die darauf hindeuten, dass die Komponente von Isabelle, dass Proof General verwendet, um mit dem Theorembeweisers entfernt zu kommunizieren. Gilt das (noch) für Isabelle 2016? Wie kann ich Proof General mit neueren Versionen von Isabelle verwenden?

Answer 1

Ja, es ist immer noch wahr; es wurde nicht wieder eingeführt. Es gibt keine Möglichkeit, die ich kenne, PG mit Isabelle laufen spätestens 2014 aus dem NEWS von Isabelle2015:

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

Answer 2

Probleme gelöst werden sollten, wo sie tatsächlich auftreten. Die Prover IDE in Isabelle2016 benötigt noch einmal weniger Ressourcen - das war in den letzten Jahren ein gemeinsames Thema. Als Proof General 1998 herauskam, war es für seine Zeit wirklich riesig und fett. Im Vergleich dazu ist Isabelle/jEdit eher leicht: Es sollte auf normalen Consumer-Computern mit nur 8 GB Speicher problemlos funktionieren.

Es gibt einige Chance, dass Sie Linux x86_64 verwenden und nicht installierten die 32-Bit-C/C++ Standardbibliotheken wie auf der installation Seite Isabelle erwähnt. Ohne dies zu tun, verdoppelt sich die ML-Heap-Anforderungen, ohne etwas Gutes zu tun.