Proof-Generalを用いたCoqの環境構築
はじめに 久々に Coq で遊びたくなったので、M1 Mac にインストールしてみた。 最近の Coq は VSCode で書くのが主流？らしいが、今回は Emacs + Proof-General で環境構築を行う。 環境構築の方法 基本的にbrewやmelpaなどの package 管理システムになるべく依存した形で環境構築を行う。 はじめに、Coqのインストール(–build-from-source をつけないとcoqtop実行時にエラーが出た。) brew install coq --build-from-source GUI 版 Emacs のインストール brew install emacs --cask Emacs の設定 次は Emacs の設定を行う。 Emacs の設定ファイルは~/.emacs.d/init.elに記載する。 まずはmelpa(Emacs のプラグインのパッケージマネージャー)のセットアップを行う。 ~/.emacs.d/init.elに以下を記載し、 (require 'package) (let* ((no-ssl (and (memq system-type '(windows-nt ms-dos)) (not (gnutls-available-p)))) (proto (if no-ssl "http" "https"))) (add-to-list 'package-archives (cons "melpa" (concat proto "://melpa.org/packages/")) t)) (package-initialize) emacs を起動して...