« 前のひとこと | トップページ | 次のひとこと »

aboutme:108464

おそらく今後も使わないけど、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年09月03日 1407

ちょっと字を大きくするフォントの設定は 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年09月03日 2600

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年09月03日 7736

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

JRF 2009年09月03日 5181

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

JRF 2009年09月03日 2565

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

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

JRF 2009年09月04日 8227

« 前のひとこと | トップページ | 次のひとこと »

トラックバック

この記事のトラックバックURL:
http://app.cocolog-nifty.com/t/trackback/93568/51548519

トラックバックのポリシー

他サイトなどからこの記事に自薦された関連記事(トラックバック)の一覧です。

» cocolog:76238664 from JRF のひとこと

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

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

このころのニュース