cocolog:83987061

定理証明システム Isabelle (現バージョンは Isabelle2015)をインストールして、その勉強をしている。 (JRF 3697)

JRF 2015年11月26日 (木) Tweet

《Isabelle》
https://isabelle.in.tum.de/
http://www.cl.cam.ac.uk/research/hvg/Isabelle/

JRF2015/11/268708

Isabelle/HOL の tutorial.pdf については次の「ひとこと」([cocolog:83987064])で感想(?)を述べるとして、こちらの「ひとこと」では、まず、インストール後から、Isabelle の統合環境を自分好みにしていったことについて述べたい。

JRF2015/11/262258

……。

2015-11-20 に Isabelle2015 を install。私は ZF を使いたかったので、まず、そこでつまづく。jEdit の右肩の Theories のパネルを開くと、"ZF" がない。"ZF-AC" とか "ZF-ex" とかはあるのに。これは、ZF が "Logics_ZF" で入っているからだと気付くまでにしばらくかかった。

使いはじめるときは Logics_ZF を選択したあと一回終了して、起動しなおせば良かった。

JRF2015/11/262843

……。

覚悟していたのが、isabelle が cygwin を使っていて、私が使っている古めのバージョンの cygwin とバージョン違いのためにエラーを起こすのではないかということ。他のソフトを使っていて "This problem is probably due to using incompatible versions of the cygwin DLL" というエラーは何度か見たことがある。

JRF2015/11/266206

でも、Isabelle2015 のほうで何か対策をしているのか、そのエラーが発生せずに違うバージョンの cygwin の同時起動が実現できているようだ。不便を覚悟していただけに、予期せぬ幸せでうれしい。

JRF2015/11/264831

ちなみに私以外の人ではめったに起こらない不具合だが、IME を『風』にしていると、Cygwin-Terminal.bat で起動したウィンドウでは入力ができない。Ctrl+Shift で IME を標準のものに切り換えると入力できる。これは、普通の DOS窓などでもそうなので、Isabelle が悪いわけではない。

JRF2015/11/265683

……。

2015-11-21 に jEdit を Emacs バインドにしようとして、plugin を探し、↓を見て試したがうまくいかない。

《Emacs Macros for jEdit - Other Software》
http://software.clapper.org/jedit-emacs/

JRF2015/11/268021

が、しかし、その後、jEdit の Utilities -> Global Options の中の Shortcuts に Choose keymap の項目があって、そこで Emacs にすればはじめからよかったんだと気付いた。(でも、C-x C-s と C-s とかキー設定を自分の好みで変えないといけない部分があるようす…。)

JRF2015/11/267159

……。

2015-11-22 に jEdit で auto translation というか replacement というか font substitution というか、symbol が勝手に書き換えられちゃうやつ。…例えば、"A ~: B" とか書くと "~:" の部分が Unicode 記号になってセーブされると \<notin> になっちゃうやつね。これ、ブログとかで引用したり、ソースを Emacs などから見るときに不便で、私は昔の表記に慣れているから、off にしようと思った。

JRF2015/11/264090

jEdit の Plugins -> Plugin Options の Isabelle の General の中の "Completion Immediate" の項目のチェックボタンをオフにすることで、なしにすることができた。けど、Immediate をオフにしただけなので、Completion で記号が出したいときは出せるのかと思っていたら、出せたり、出せなかったり。\<notin> を出そうと思ったら、下の Symbols パネルから探して入力する必要があった。

(今はだいたい出せてる。最初のときだけバグって出せなかったのか？)

JRF2015/11/265874

……。

2015-11-24 に Isabelle を起動中にご飯を食べに休憩したとき、PC のスクリーンセーバー(ディスプレイの電源が切れるタイプ)になったんだけど、その後、マウスを動かしてもディスプレイの電源がオンにならなかった。普段はこんなことないんだけど…。Isabelle が使うメモリのサイズがデカいから、不具合が生じたのかな？

JRF2015/11/265713

……。

2015-11-25 に、Isabelle を起動中に他のエディタ(Emacs)に入力しようとしたのが、jEdit への中途半端な入力になったらしくヌルポ(Null Pointer Assignment)のエラーダイアログが表示された。

JRF2015/11/269361

……。

上で書いた不具合はいずれも再現性がなく、いっしょに起動している Firefox のほうがおかしくなったりということがあったくらいで、うちのシステム全体がメモリの使い過ぎ等で少し不安定になっているのかもしれない。

が、不安定さは「少し」で、スクリーンセーバーから復帰できないのも一度経験したのみで、それ以降は安定して復帰できているし、Firefox の不具合も、Firefox を起動しなおすだけで直った。

私が使ってる PC は自慢じゃないが貧弱なものなので、そのほうに問題があると思う。だから、他の人のところではもっとまともにサクサク動いているのではないか。

JRF2015/11/265043

Isabelle2015、概して、問題ないっすよ。

JRF2015/11/260259

……。

追記。

JRF2015/12/60194

2015-12-06 に気になっていたことを解決した。thm で表示したときもそうなんだけど特に proof state で気になっていた。jEdit で、"[| P; Q |] ==> P & Q" みたいに入力しても、tutorial.pdf にあるような "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> Q" という表示ではなく \<Longrightarrow> だけを使った表示である " P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" という表示になっていた。

JRF2015/12/60168

"isabelle only Longrightarrow" や lbrakk や rbrakk を付けたり足したりしてググっていたが見つからず、jEdit の Plugin Options にやっと Print Mode という空欄を見出してもしやと思って "isabelle print mode jedit" でググると、↓がヒットした。

JRF2015/12/64311

《How do I display brackets around assumptions in Isabelle/jEdit? - Stack Overflow》
http://stackoverflow.com/questions/15939265/how-do-i-display-brackets-around-assumptions-in-isabelle-jedit

JRF2015/12/68251

それによると Plugins -> Plugin Options の Isabelle の General の Print Mode に brackets と設定すればいいようだ。デフォルトだと no_brackets が設定されている状態になっているらしい。有効にするためには設定したあとに再起動する必要がある。

JRF2015/12/60827