おそらく今後も使わないけど、Isabelle2009 の cygwin…

おそらく今後も使わないけど、Isabelle2009 の cygwin 版をインストール。ProofGeneral の設定が難しい。Meadow だとシンボリックリンクの関係でうまくいかなかった。xemacs も何かおかしい。GNU Emacs 23 だとわりとうまくいった。
JRF 2009年9月3日

xemac も GNU Emacs も cygwin の X から起動している。

今入ってるバージョンは xemacs 21.4 (patch 22)、GNU Emacs 23.0.92.1。

それぞれの .emacs を編集するのに時間がとられた。ProofGeneral が起動して適度なフォントサイズで utf-8 ぐらいは使えるようにする…ということに絞って設定した。(なんと xemacs はデフォルトだと
 utf-8 を使えない。ググると (require 'un-define) とかしないといけないらしい。)

JRF 2009年9月3日

ちょっと字を大きくするフォントの設定は xemacs が
(custom-set-faces
'(default ((t (:size "14pt" :family "Courier"))) t))

GNU Emacs が
(if window-system
(set-default-font
"-*-fixed-medium-r-normal-*-16-*-*-*-*-*-fontset-standard"))
JRF 2009年9月3日

ProofGeneral は isatool じゃなくなって /usr/local/Isabelle/bin/isabelle を使う。よって次の設定があるといい。

(if (file-directory-p "/usr/local/ProofGeneral/generic")
    (progn
      (load-file "/usr/local/ProofGeneral/generic/proof-site.el")
      (setq isa-isatool-command "/usr/local/Isabelle/bin/isabelle")))

JRF 2009年9月3日

…しかし、thy ファイルも書き方がずいぶん変わった。Isar って何？私が使ってたころは Isabelle「2009」とか年数がつかず「無印」だった。(98 とかでもないよ。)ZF のドキュメントがデフォルトで消えてるらしいのもちょっとショック。まぁ、大学院を出ていらい実質使ってないから、それぐらいの変化は当然だろうけど。


JRF 2009年9月3日

あと emacs で color-mate は普通使わないようになったんですね。jka-compr-ccrypt が使えない(使うと  .gz が読めなくなる)のも地味に痛い。
JRF 2009年9月3日

使ってないから Isabelle の記事は書いてない。思い出を元に書いたのが↓か。

メタ論理: 演驛と帰納 [ JRF の私見：雑記 ]
http://jrf.cocolog-nifty.com/column/2006/01/post_10.html
JRF 2009年9月4日

Trackbacks:

《cocolog:76238664》 from JRF のひとこと
http://jrf.cocolog-nifty.com/statuses/2013/04/post-b278.html

昔、使ってた定理証明支援システムをインストールしようとしてうまくいかない。 

受信： 2013-06-30 00:01:21 (JST)