Coq
Sublime Text的Coq编程语言支持
标签 语法
详细信息
安装次数
- 总数 2K
- Win 406
- Mac 701
- Linux 511
| 8月6日 | 8月5日 | 8月4日 | 8月3日 | 8月2日 | 8月1日 | 7月31日 | 7月30日 | 7月29日 | 7月28日 | 7月27日 | 7月26日 | 7月25日 | 7月24日 | 7月23日 | 7月22日 | 7月21日 | 7月20日 | 7月19日 | 7月18日 | 7月17日 | 7月16日 | 7月15日 | 7月14日 | 7月13日 | 7月12日 | 7月11日 | 7月10日 | 7月9日 | 7月8日 | 7月7日 | 7月6日 | 7月5日 | 7月4日 | 7月3日 | 7月2日 | 7月1日 | 6月30日 | 6月29日 | 6月28日 | 6月27日 | 6月26日 | 6月25日 | 6月24日 | 6月23日 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Windows | 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 | 1 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| Mac | 1 | 1 | 0 | 0 | 1 | 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 | 0 |
| Linux | 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 | 1 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 |
自述文件
Sublime Coq
Sublime Text 3编辑器用于Coq证明辅助工具的扩展。
注意：Coq有很多特性，但其中并非所有都在语法高亮和命令面板中得到支持。如果您有需求或者遇到高亮错误，请提交问题！
安装
推荐使用Package Control来安装Sublime Coq。
也可以使用git进行安装。导航到Sublime Text的Packages文件夹，然后运行
git clone [email protected]:whitequark/Sublime-Coq Coq
入门指南
首先，在一个窗口中打开您的Coq脚本，然后在命令面板中选择Coq: Start。现在您应该看到一个弹出的面板，显示来自coqtop的欢迎消息。
目前有多个命令可用
- Coq: 下一个语句 (OS X:
Super+Ctrl+n，Win/Linux:Ctrl+Down)：证明当前行并跳转到下一个语句。 - Coq: 撤销语句 (OS X:
Super+Ctrl+u，Win/Linux:Ctrl+Up)：撤销已证明的语句并返回上一行。撤销Qed.将撤销整个证明。 - Coq: 中断证明 (OS X:
Super+Ctrl+p，Win/Linux:Alt+Backspace)：在一个证明中撤销每个策略和定理定义。 - Coq: 运行到此处 (OS X:
Super+Ctrl+h，Win/Linux:Ctrl+Enter)：证明或撤销语句，直到光标位置。 - Coq: 搜索，Coq: 搜索模式，Coq: 搜索重写，Coq: 搜索关于：搜索证明、模式和重写定理，结果会在您输入时显示。按Enter键从搜索结果中选择名称并插入到光标位置。
- Coq: 停止: (OS X:
Super+Ctrl+k，Win/Linux:Ctrl+Escape)：停止coqtop并关闭输出面板。
出现错误后，按Escape键清除它并查看当前目标。
到coqtop的路径
您可能需要修改Sublime Coq设置的用户首选项文件中coqtop_path的值（通常通过在shell中运行which coqtop来实现），以便能找到coqtop程序。
如果coqtop_path为空，环境变量PATH将被查找以查找名为coqtop的程序。
高亮显示
为了为文件中的已证明部分获取漂亮的后台高亮，请将以下片段添加到您的调色板文件中。
对于tmTheme语法
深色主题
<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>
浅色主题
<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>
对于sublime-color-scheme语法
深色主题
{
"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"
},
浅色主题
{
"name": "Proven with Coq",
"scope": "meta.proven.coq",
"background": "#002800",
},