Isabelle2016 и Proof General
Я пытался научиться использовать Isabelle 2016. Хотя в принципе мне нравится идея асинхронной проверки корректности, мне не нравится Isabelle/jEdit по ряду причин, наиболее серьезной из которых является то, что она использует слишком много памяти (для меня).
Было бы здорово, если бы я мог использовать старый добрый Proof General с Isabelle 2016. Я установил переменную isa-isabelle-command указать файл bin/isabelle в каталоге распространения Изабель. Когда я запускаю Изабель с помощью меню Proof General, Emacs зависает, а когда я прерываю его, C-gЯ получаю следующее в *isabelle* буфер.
> val it = (): unit
^BException- ERROR "Bad socket name: \"I\"" raised
Я знаю о старых публикациях на этом сайте, которые предполагают, что компонент Изабель, который Proof General использует для связи с доказателем теорем, был удален. Это (все еще) верно для Изабель 2016? Как я могу использовать Proof General с более новыми версиями Isabelle?
2 ответа
Да, это все еще правда; это не было повторно введено. Я не знаю, как запустить PG с Изабель позже 2014 года. NEWS Изабель 2015:
* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
Проблемы должны быть решены там, где они действительно происходят. IDE Prover в Isabelle2016 снова требует меньше ресурсов - это стало общей темой в последние годы. Когда в 1998 году вышел Proof General, он был действительно огромным и толстым для своего времени. В сравнении Isabelle/jEdit довольно легок: он должен работать бесперебойно на обычных потребительских компьютерах с только 8 ГБ памяти.
Существует некоторая вероятность того, что вы используете Linux x86_64 и не установили 32-битные стандартные библиотеки C/C++, как указано на странице установки Isabelle. Опуская это, удваивает требования к куче ML, не делая ничего хорошего.