cocolog:76238664
昔、使ってた定理証明支援システムをインストールしようとしてうまくいかない。 (JRF 9359)
JRF 2013年4月19日 (金)
まぁ、昔は tty を emacs shell から使ってたから isabelle tty コマンドを使えばいいんだけど…。
ちょっと気合い入れないと、前やってたことをもう一度やるのさえ難しそう。
2009 年と同じく今回もインストールだけに終りそうな予感…。
JRF2013年4月19日5771
……。
ただ、Windows 版。アイコンだけでなくフォルダも Desktop にインストールしちゃうのは、やめて欲しんだけど…。
でも、Windows がその辺そもそも Unix 系に比べて変態的だという主張なら、まぁ、わかるんだけどね。
JRF2013年4月19日4006
一回、追随してしまえば慣れるだろうから、年１回ぐらいの更新にちょこちょこといじってれば、このシステムを使った証明力、私程度のものなら維持できそうなんだけど…。
isabelle tty 起動するだけですごい時間かかるしな…。うーん、まぁ、しかし、１ヶ月ぐらいかける覚悟さえあれば、不可能ではないはずだし…。
でも、もう少し確率モデルのほうをいじっていたいし…。でも、それが今なかなか進まないんだよな。並行してやってるゲームもなかなか進まないし。気分転換としてやるのも…。いやいや、そういうレベルの気合じゃ対応できないから、確率モデルが犠牲になるだろう…それは避けたい。
…とかツラツラ悩む。
JRF2013年4月19日0835
[aboutme:108464] にも書いた Isabelle の 2013年版。
Isabelle 自体は、Windows 対応…といっても中身は Cygwin ですでに入ってる(古い)Cygwin との相性が気になるところだが、すんなりインストールできた。でも、ProofGeneral がぜんぜん動かない。
上の「ひとこと」を見ると、2009年版も Emacs は Windows 版ではダメで Cygwin X 版じゃないと動かなかったみたいな書きぶり。
要は Windows では ProofGeneral じゃなく jEdit 版を使えということなんだろうな…。
JRF2013年4月19日7876