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

cocolog:76238664

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

JRF 2013年4月19日 (金)

[aboutme:108464] にも書いた Isabelle の 2013年版。

Isabelle 自体は、Windows 対応…といっても中身は Cygwin ですでに入ってる(古い)Cygwin との相性が気になるところだが、すんなりインストールできた。でも、ProofGeneral がぜんぜん動かない。

上の「ひとこと」を見ると、2009年版も Emacs は Windows 版ではダメで Cygwin X 版じゃないと動かなかったみたいな書きぶり。

要は Windows では ProofGeneral じゃなく jEdit 版を使えということなんだろうな…。

JRF2013年4月19日7876

まぁ、昔は tty を emacs shell から使ってたから isabelle tty コマンドを使えばいいんだけど…。

ちょっと気合い入れないと、前やってたことをもう一度やるのさえ難しそう。

2009 年と同じく今回もインストールだけに終りそうな予感…。

JRF2013年4月19日5771

……。

ただ、Windows 版。アイコンだけでなくフォルダも Desktop にインストールしちゃうのは、やめて欲しんだけど…。

でも、Windows がその辺そもそも Unix 系に比べて変態的だという主張なら、まぁ、わかるんだけどね。

JRF2013年4月19日4006

一回、追随してしまえば慣れるだろうから、年1回ぐらいの更新にちょこちょこといじってれば、このシステムを使った証明力、私程度のものなら維持できそうなんだけど…。

isabelle tty 起動するだけですごい時間かかるしな…。うーん、まぁ、しかし、1ヶ月ぐらいかける覚悟さえあれば、不可能ではないはずだし…。

でも、もう少し確率モデルのほうをいじっていたいし…。でも、それが今なかなか進まないんだよな。並行してやってるゲームもなかなか進まないし。気分転換としてやるのも…。いやいや、そういうレベルの気合じゃ対応できないから、確率モデルが犠牲になるだろう…それは避けたい。

…とかツラツラ悩む。

JRF2013年4月19日0835

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

トラックバック

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

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

他サイトなどからこの記事に自薦された関連記事(トラックバック)はまだありません。

このころのニュース