COQ – Calculus of Inductive Constructions – Sublime – OS X 10.10.X

  • Post published:March 18, 2015

0. Preparation
As of OS X 10.10 the official coq IDE version (Coq 8.4pl5) is not working.

0.1 Install brew
Enter your terminal ans execute:
ruby -e “$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)”

0.2 Install coq
brew install coq

0.3 Install coqide
brew install Caskroom/cask/coqide

 

1. Install “Sublime Package Control”:
If for some reason the console installation instructions do not work for you (such as having a proxy on your network), perform the following steps to manually install Package Control:

  1. Click the Preferences > Browse Packages… menu
  2. Browse up a folder and then into the Installed Packages/ folder
  3. Download Package Control.sublime-package and copy it into the Installed Packages/ directory
  4. Restart Sublime Text

2. Install Coq Support:
Click: Sublime Preferences >Package Control > Install Package > Select/Search Coq

 

3. Setup Sublime Coq – Build:
More info here: http://sublimetext.info/docs/en/reference/build_systems.html#build-systems

Click: Sublime Tools >Build System > New Build System… > Copy and Paste Code below
Save file as /Users/<name>/Library/Application Support/Sublime Text 3/Packages/User/coq.sublime-build

{
    “cmd”: [“/usr/local/Cellar/coq/8.4pl5/bin/coqc”, “$file”],
    “file_regex”: “^[ ]*File \”(…*?)\”, line ([0-9]*)”,
    “selector”: “source.coq”,
}