6

私は Isabelle 2016 の使い方を学ぼうとしています。基本的には非同期プルーフ チェックのアイデアが好きですが、Isabelle/jEdit はいくつかの理由で好きではありません。最も深刻な理由は、メモリを使いすぎることです。 （私のため）。

Isabelle 2016 で古き良き Proof General を使用できれば素晴らしいと思います。Isabelle 配布ディレクトリの下のisa-isabelle-commandファイルを指すように変数を設定しました。bin/isabelleProof General のメニューを使用して Isabelle を起動すると、Emacs がハングしC-gます*isabelle*。

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

Proof General が定理証明者と通信するために使用する Isabelle のコンポーネントが削除されたことを示唆する、このサイトの古い投稿を認識しています。これは、Isabelle 2016 にも (まだ) 当てはまりますか? 新しいバージョンの Isabelle で Proof General を使用するにはどうすればよいですか?

4

2 に答える 2

6

はい、それはまだ真実です。再導入されていません。2014年以降にIsabelleでPGを実行することを私が知っている方法はありません.Isabelle2015のよりNEWS:

* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
于 2016-02-22T06:24:43.830 に答える