EmacsでCoqを動かすまで（Mac）

Homebrewのインストール

Homebrew

% /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

Emacsのインストール

Emacsのインストール

% brew install emacs --cask

opamのインストール

opamを用いたOCamlプロジェクトのセットアップ方法

% brew install opam　#Homebrewを用いてopamのインストール
% opam init　#opamの初期化
% eval $(opam env)　#環境変数の更新

Coqのインストール

% opam pin add coq 8.13.0 #Coqをバージチョン指定でインストール
% opam list　#coq 8.13.0 pinned to version 8.13.0の表記があるはず

Emacsの設定

(require 'package)
;; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)

M-x package-list-packages

上のコマンドを入力して表示されたリストからproof-generalを選択し、インストール

company-coqも同様の手順で入れると便利

coqtop not found的なエラーが出たらinit.elを書き換える

(require 'package)
;;(setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)
(custom-set-variables
 ;; custom-set-variables was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 '(coq-prog-name "/Users/mayu/.opam/default/bin/coqtop") <-----
 '(package-selected-packages '(company-coq proof-general ##)) 
 '(proof-three-window-enable t))
(custom-set-faces
 ;; custom-set-faces was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 )
(add-hook 'coq-mode-hook #'company-coq-mode)

矢印の箇所はcoqtopへのpathを指定、基本[ROOT]/.opam/[Ocaml_VERSION]/bin/coqtopになるはず