Coq
Coq programming language support for Sublime Text
Details
Installs
- Total 2K
- Win 423
- Mac 714
- Linux 521
May 4 | May 3 | May 2 | May 1 | Apr 30 | Apr 29 | Apr 28 | Apr 27 | Apr 26 | Apr 25 | Apr 24 | Apr 23 | Apr 22 | Apr 21 | Apr 20 | Apr 19 | Apr 18 | Apr 17 | Apr 16 | Apr 15 | Apr 14 | Apr 13 | Apr 12 | Apr 11 | Apr 10 | Apr 9 | Apr 8 | Apr 7 | Apr 6 | Apr 5 | Apr 4 | Apr 3 | Apr 2 | Apr 1 | Mar 31 | Mar 30 | Mar 29 | Mar 28 | Mar 27 | Mar 26 | Mar 25 | Mar 24 | Mar 23 | Mar 22 | Mar 21 | |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Windows | 0 | 0 | 0 | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 |
Mac | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
Linux | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 1 | 0 |
Readme
- Source
- raw.githubusercontent.com
Sublime Coq
Extensions to the Sublime Text 3 editor for use with the Coq Proof Assistant.
Note: Coq has a great many features, and not all of them are supported in the syntax highlighter and command palette yet. If you want something or encounter a highlighting error, just open an issue!
Installation
The recommended way to install Sublime Coq is to use Package Control.
It is also possible to install it using git. Navigate to the Sublime Text Packages
folder, then run:
git clone git@github.com:whitequark/Sublime-Coq Coq
Getting Started
First, open your Coq script in a window, then select Coq: Start
in the command palette. Now you should see another pane jumping out, showing the welcome message from coqtop
.
There are several commands available now:
- Coq: Next Statement (OS X:
Super+Ctrl+n
, Win/Linux:Ctrl+Down
): Prove the current line and go to next statement. - Coq: Undo Statement (OS X:
Super+Ctrl+u
, Win/Linux:Ctrl+Up
): Undo the current proven statement and go back to the last line. UndoingQed.
undoes the entire proof. - Coq: Abort Proof (OS X:
Super+Ctrl+p
, Win/Linux:Alt+Backspace
): In a proof, undo every tactic and the theorem definition. - Coq: Run Here (OS X:
Super+Ctrl+h
, Win/Linux:Ctrl+Enter
): Prove or undo statements until the caret position is reached. - Coq: Search, Coq: Search Pattern, Coq: Search Rewrite, Coq: Search About: Search proofs, patterns and rewriting theorems, with results shown as you type. Press Enter to select a name from search results and insert it at caret.
- Coq: Stop: (OS X:
Super+Ctrl+k
, Win/Linux:Ctrl+Escape
): Stopcoqtop
and close the output pane.
After encountering an error, press Escape to clear it and see the current goals.
Path to coqtop
You might need to modify the user preference file for Sublime Coq setting coqtop_path
to a proper value (usually by running which coqtop
in a shell), so that the coqtop
program can be found.
If coqtop_path
is empty, the PATH
environment variable will be searched for a program called coqtop
.
Highlighting
In order to get nice background highlighting for the proven parts of the file, add the following snippet to your color scheme file.
For tmTheme
syntax:
dark themes
<dict>
<key>name</key>
<string>Error message</string>
<key>scope</key>
<string>message.error</string>
<key>settings</key>
<dict>
<key>foreground</key>
<string>#cc3333</string>
</dict>
</dict>
<dict>
<key>name</key>
<string>Warning message</string>
<key>scope</key>
<string>message.warning</string>
<key>settings</key>
<dict>
<key>foreground</key>
<string>#ffcc00</string>
</dict>
</dict>
<dict>
<key>name</key>
<string>Informational message</string>
<key>scope</key>
<string>message.info</string>
<key>settings</key>
<dict>
<key>foreground</key>
<string>#d5d5d5</string>
<key>background</key>
<string>#2b2b2b</string>
</dict>
</dict>
<dict>
<key>name</key>
<string>Proven with Coq</string>
<key>scope</key>
<string>meta.proven.coq</string>
<key>settings</key>
<dict>
<key>background</key>
<string>#058D050D</string>
<key>foreground</key>
<string>#05a505</string>
</dict>
</dict>
light themes
<dict>
<key>name</key>
<string>Proven with Coq</string>
<key>scope</key>
<string>meta.proven.coq</string>
<key>settings</key>
<dict>
<key>background</key>
<string>#002800</string>
</dict>
</dict>
For sublime-color-scheme
syntax:
dark themes
{
"name": "Error message",
"scope": "message.error",
"foreground": "#cc3333"
},
{
"name": "Warning message",
"scope": "message.warning",
"foreground": "#ffcc00"
},
{
"name": "Informational message",
"scope": "message.info",
"foreground": "#d5d5d5",
"background": "#2b2b2b"
},
{
"name": "Proven with Coq",
"scope": "meta.proven.coq",
"background": "#058D050D",
"foreground": "#7fa96f"
},
light themes
{
"name": "Proven with Coq",
"scope": "meta.proven.coq",
"background": "#002800",
},