ctrl+shift+p filters: :st2 :st3 :win :osx :linux
Browse

Coq

by whitequark ST3

Coq programming language support for Sublime Text

Labels syntax

Details

  • 2020.02.13.23.28.08
  • github.​com
  • github.​com
  • 4 years ago
  • 2 hours ago
  • 10 years ago

Installs

  • Total 2K
  • Win 401
  • Mac 697
  • Linux 502
Mar 28 Mar 27 Mar 26 Mar 25 Mar 24 Mar 23 Mar 22 Mar 21 Mar 20 Mar 19 Mar 18 Mar 17 Mar 16 Mar 15 Mar 14 Mar 13 Mar 12 Mar 11 Mar 10 Mar 9 Mar 8 Mar 7 Mar 6 Mar 5 Mar 4 Mar 3 Mar 2 Mar 1 Feb 29 Feb 28 Feb 27 Feb 26 Feb 25 Feb 24 Feb 23 Feb 22 Feb 21 Feb 20 Feb 19 Feb 18 Feb 17 Feb 16 Feb 15 Feb 14 Feb 13
Windows 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 2 0 0 0 0 0 0 1 0 0 0 0 0 0 0
Mac 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0
Linux 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 0 0 0 0 0 0 0 0 0 0 0 0 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. Undoing Qed. 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): Stop coqtop 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",
},