本買った

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

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

Coqとは

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

そもそも

brew cask install coqide

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

p.17

From mathcomp
Require Import ssreflect.

が正しく動作しなかった。どうも拡張がうまくいってないらしい。しかしどうあがいても一旦入れてしまったcoqideを後から拡張することができない。そこでopamで全てを済ませることが必要らしいと言う暗礁に乗り上げることになったのである。

ここで救世主現る。そう、結城氏である。

自分の環境に

$ brew install opam

した後はこの方のやった事に追随させていただいた。気になるのはopamのversionが2系に私はなっていたことくらいだが、ありがとうございました。今度本買います。

brew linkをどうにかしろとか言うエラーが頻出するようになった。この辺りでhome brew関連の設定というか理解を怠っていたツケが回ってきた。とりあえず、

$ brew doctor

というコマンドを知った。これにより、

を承知した。

$ opam install coqide.8.7.0でこけた。盛大に。
エラー文的に、一番近かったのは次の記事だった。

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

$ opam install coqide.8.7.1

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

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

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