Isabelle2016 и Proof General

Question

Я пытался научиться использовать Isabelle 2016. Хотя в принципе мне нравится идея проверки асинхронных проверок, мне не нравится Isabelle/jEdit по ряду причин, самые серьезные из которых что он использует слишком много памяти (для меня).

Было бы здорово, если бы я мог использовать старый добрый доказательство с Isabelle 2016. Я установил переменную isa-isabelle-command, чтобы указать файл bin/isabelle под каталогом распространения Isabelle. Когда я запускаю Isabelle, используя меню «Доказательство», Emacs зависает, и когда я прерываю его на C-g, я получаю следующее в буфере *isabelle*.

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

Я знаю старые проводки на этом сайте, которые свидетельствуют о том, что компонент Изабелле, что Доказательство общего пользования для связи с теоремой испытатель была удалена. Действительно ли это (правда) Изабель 2016? Как я могу использовать Proof General с новыми версиями Isabelle?

Answer 1

Да, это все еще так; он не был повторно введен. Там нет никакого способа, которым я знаю, чтобы запустить PG с Изабеллой позже, чем 2014. Из NEWS из Isabelle2015:

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

Answer 2

проблемы должны быть решены, когда они на самом деле происходит. Prover IDE в Isabelle2016 требует еще меньше ресурсов - это была общая тема в последние годы. Когда в 1998 году вышел Proof General, он был действительно огромным и жирным для своего времени. В сравнении Isabelle/jEdit довольно лёгкий: он должен работать плавно на обычных потребительских компьютерах с объемом памяти 8 ГБ.

Существует некоторая вероятность того, что вы используете Linux x86_64 и не установили 32-битный C/C++ стандартные библиотеки, как указано на странице Isabelle installation. Опуская это, удваивает требования кучи ML, не делая ничего хорошего.