Coq programming language support for Sublime Text
- Total 764
- Win 187
- OS X 353
- Linux 224
|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||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|
Extensions to the Sublime Text 3 editor for use with the Coq Proof Assistant.
Currently, Sublime-Coq plugin is not as flexible as you might hope, but it is still working well. First, open your coq script in a window, then select
Sublime-Coq: Run in the command palette. Now you should see another pane jumping out, showing the welcome message from
All your editing operations should be done at the script pane, while all commands should be issued only at the
There are several commands available now:
- Next statement (OS X:
ctrl+down): Prove the current line and go to next statement
- Undo statement (OS X:
ctrl+up): Undo the current proven statement and go back to the last line. NOTE: it seems not working as smoothly as CoqIDE now, but you can try it several times and see how it behaves.
- Success: (OS X:
ctrl+enter): Mark current line as proven and go to next line. Similar to Next statement but you don't send anything to
- Clear: (OS X:
ctrl+backspace): Clear the output information on
- Stop: (OS X:
ctrl+escape): Stop the
coqtopand close the output pane.
You might need to modify the user preference file for Sublime-Coq, change
coqtop_path to a proper value (usually from
which coqtop or similar way), so the
coqtop program can be correctly found.
The default value will simply be
coqtop, but during initialization,
$PATH will also be searched.
In order to get nice background highlighting for the proven parts of the file, add this to your theme (for light backgrounds):
<dict> <key>name</key> <string>Proven by Coq</string> <key>scope</key> <string>meta.coq.proven</string> <key>settings</key> <dict> <key>background</key> <string>#dcffcc</string> </dict> </dict>
- Enrich the language spec
undoseems not working well sometimes