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

Coq

by whitequark ST3

Coq programming language support for Sublime Text

Labels syntax

Details

  • 2018.08.04.22.42.59
  • github.​com
  • 3 months ago
  • 3 minutes ago
  • 4 years ago

Installs

  • Total 893
  • Win 215
  • OS X 413
  • Linux 265
Oct 24 Oct 23 Oct 22 Oct 21 Oct 20 Oct 19 Oct 18 Oct 17 Oct 16 Oct 15 Oct 14 Oct 13 Oct 12 Oct 11 Oct 10 Oct 9 Oct 8 Oct 7 Oct 6 Oct 5 Oct 4 Oct 3 Oct 2 Oct 1 Sep 30 Sep 29 Sep 28 Sep 27 Sep 26 Sep 25 Sep 24 Sep 23 Sep 22 Sep 21 Sep 20 Sep 19 Sep 18 Sep 17 Sep 16 Sep 15 Sep 14 Sep 13 Sep 12 Sep 11 Sep 10 Sep 9
Windows 0 0 0 0 0 0 1 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 0 0 5 0 0 0 0 0 0 0 0 0 1 0 0 0 1 0 1 0 1 0
OS X 0 0 0 0 0 0 0 0 0 1 1 0 0 0 0 1 1 1 0 0 0 0 1 0 0 1 1 1 0 6 0 0 1 0 0 2 0 0 0 1 0 0 2 1 0 3
Linux 0 2 0 0 1 0 0 0 2 1 0 0 0 0 0 0 0 2 1 0 0 2 0 0 0 0 0 0 1 0 2 0 2 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!

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",
},