CoqIDEをMacに入れたかった（本買った）

本買った

店頭で見つけた定理証明支援系に関する書籍を衝動買いしてしまいました。

Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化 単行本（ソフトカバー） – 2018/4/18 萩原 学 (著), アフェルト・レナルド (著)

早速インストールだけしてしまおうと思ったのですが、本文にはwinへの導入だけが例示されていたのでmaxosxへの導入については自力でググり続けることに。

Coqとは

以下のことがなんとなく理解できました。

• Coqと言うのが定理証明支援系の名前らしい
• SSreflect/MathCompと言うので拡張しないといけないらしい。
• どっちもopamと言うバージョン管理システムでいける。
• CoqIDEと言うのがあるからemacs使いじゃなければ使ったらいいお。

OPAMとは

• brewとかcondaみたいにバージョン管理（OCamlの？)をしてくれる。
• そもそもOCamlがなんなのかよくわかったない。
• 多分brewでopamがインストールできる。

なぜbrew cask installしなかったのか

そもそも

brew cask install coqide

で全てがうまくいくはずだった。それなのに、

p.17

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

$ opam switch 4.05.0で進めていたので完全には一致しないが、とにかくバージョンに関する問題が発生していると思われるので、結局、

$ opam install coqide.8.7.1

でインストール完了した。

原因は？

もはや正確にはわからないが、opamのバージョンが2だったからいけなかった（結城氏と同じ状況にならなかった）というのが一番怪しい。確かめる気力を失ってしまったのでとりあえず本を読み進めている。

私は何を分かっていない？

そもそもここまで買いてみて分かったが、私相当時間を無駄にしているけど理路整然と一個一個理解を深めていけばこんなに回り道しないでいけたのでは？　教えて偉い人！

現状

• coqideを毎回terminalから開いている（なぜ？）
• Modus Ponensとかやったわあ、学部のとき論理学基礎論でやったわあ
• ﾀﾉｼｲ！