#本買った
店頭で見つけた定理証明支援系に関する書籍を衝動買いしてしまいました。
####Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化 単行本（ソフトカバー） – 2018/4/18 萩原 学 (著), アフェルト・レナルド (著)
https://www.amazon.co.jp/Coq-SSReflect-MathComp%E3%81%AB%E3%82%88%E3%82%8B%E5%AE%9A%E7%90%86%E8%A8%BC%E6%98%8E-%E3%83%95%E3%83%AA%E3%83%BC%E3%82%BD%E3%83%95%E3%83%88%E3%81%A7%E3%81%AF%E3%81%98%E3%82%81%E3%82%8B%E6%95%B0%E5%AD%A6%E3%81%AE%E5%BD%A2%E5%BC%8F%E5%8C%96-%E8%90%A9%E5%8E%9F/dp/4627062419
早速インストールだけしてしまおうと思ったのですが、本文にはwinへの導入だけが例示されていたのでmaxosxへの導入については自力でググり続けることに。
#Coqとは
以下のことがなんとなく理解できました。
- Coqと言うのが定理証明支援系の名前らしい
- SSreflect/MathCompと言うので拡張しないといけないらしい。
- どっちもopamと言うバージョン管理システムでいける。
- CoqIDEと言うのがあるからemacs使いじゃなければ使ったらいいお。
#OPAMとは
- brewとかcondaみたいにバージョン管理（OCamlの？)をしてくれる。
- そもそもOCamlがなんなのかよくわかったない。
- 多分brewでopamがインストールできる。
#なぜbrew cask installしなかったのか
そもそも
brew cask install coqide
で全てがうまくいくはずだった。それなのに、
From mathcomp
Require Import ssreflect.
が正しく動作しなかった。どうも拡張がうまくいってないらしい。しかしどうあがいても一旦入れてしまったcoqideを後から拡張することができない。そこでopamで全てを済ませることが必要らしいと言う暗礁に乗り上げることになったのである。
#opamへの道
ここで救世主現る。そう、結城氏である。
###Installing CoqIDE 8.7.0 to MacBook(結城浩のブログ)
自分の環境に
$ brew install opam
した後はこの方のやった事に追随させていただいた。気になるのはopamのversionが2系に私はなっていたことくらいだが、ありがとうございました。今度本買います。
#brewが死んだ
brew linkをどうにかしろとか言うエラーが頻出するようになった。この辺りでhome brew関連の設定というか理解を怠っていたツケが回ってきた。とりあえず、
$ brew doctor
というコマンドを知った。これにより、
- いらないファイルが置いてあるから
rmすべき旨 - 適切な
brew link hogeがなされていないからちゃんとすべき旨
を承知した。
#coqideが死んだ
$ opam install coqide.8.7.0でこけた。盛大に。
エラー文的に、一番近かったのは次の記事だった。
###CoqIDE 8.7.0 incompatible with LablGTK 2.18.6 and OCaml 4.06.0 #6140
https://github.com/coq/coq/issues/6140
$ opam switch 4.05.0で進めていたので完全には一致しないが、とにかくバージョンに関する問題が発生していると思われるので、結局、
$ opam install coqide.8.7.1
でインストール完了した。
#原因は？
もはや正確にはわからないが、opamのバージョンが2だったからいけなかった（結城氏と同じ状況にならなかった）というのが一番怪しい。確かめる気力を失ってしまったのでとりあえず本を読み進めている。
#私は何を分かっていない？
そもそもここまで買いてみて分かったが、私相当時間を無駄にしているけど理路整然と一個一個理解を深めていけばこんなに回り道しないでいけたのでは？ 教えて偉い人！
#現状
- coqideを毎回terminalから開いている（なぜ？）
- Modus Ponensとかやったわあ、学部のとき論理学基礎論でやったわあ
- ﾀﾉｼｲ！