Coq の設定

ふと思い立ち定理証明について勉強することにした。Coq は使ったことすらない。以下の本を買ったのでまずは Coq の設定から。

Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化

ググったところ Mac への install は結構大変らしい。

溝口先生の以下のスライドに従いやってみる。

使っている Mac は macOS Monterey 12.4。Intel Mac.

CoqIDE のインストール

brew install coqide --cask
==> Downloading https://github.com/coq/coq/releases/download/V8.13.1/coq-8.13.1-
==> Downloading from https://objects.githubusercontent.com/github-production-rel
######################################################################## 100.0%
==> Installing Cask coqide
==> Moving App 'CoqIDE_8.13.1.app' to '/Applications/CoqIDE_8.13.1.app'
🍺  coqide was successfully installed!

install 後には Mac の "システム環境設定" の "セキュリティとプライバシー" からダウンロードしたアプリケーションの実行許可で "開く" を行う必要がある。

MathComp のインストール

$ git clone git@github.com:math-comp/math-comp.git

# ~/.bash_profile に以下を追加
export PATH=/Applications/CoqIDE_8.13.1.app/Contents/Resources/bin:$PATH

$ source ~/.bash_profile
$ which coqc
/Applications/CoqIDE_8.13.1.app/Contents/Resources/bin/coqc

$ cd math-comp/mathcomp
$ make
$ sudo make install

動いた！溝口先生に感謝。