whitequark/sublime-coq

Coq programming language support for Sublime Text

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 [email protected]: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",
},

sublime-coq's Issues

Not working on Sublime Text build 3211 (Ubuntu)

Hello,

After installing the package, I do get the (Coq: Start) option in the command palette, but once I select it all I get is a blank COQTOP window and the only option in the palette is (Coq: Restart).
Does anybody have a clue how to fix this...?

Evaluation goes past cursor

Take the following incomplete proof (the | marking my cursor)

Lemma nat_not_negative : forall i : nat, ~(i < 0) .
Proof.
   intro i. |
Qed.

Note the space between the . and my cursor. If you then instruct the plugin to evaluate to the cursor it will also evaluate the Qed, and then complains the proof is incomplete. This seems to be caused by the fact that the evaluate to cursor doesn't consider where the check will end up after evaluating one extra statement, instead it just checks if we are still before the cursor. So unless the cursor is right after the . it will always evaluate an extra statement.

Undo/Redo freezing ST when read_only is set

ST would freeze (and has to be killed) during a coqtop session when
the cursor is positioned after the "proven" region, so the view is not read-only, but an undo action affects the contents of the proven region.
To workaround this issue I disabled undo/redo when the session is ongoing, but it's less than ideal,
see https://github.com/bordaigorl/Sublime-Coq/tree/fix-undo-readonly

Ideally, one would be able to predict the extents of the undo/redo action but that's not supported by the current API.
A less efficient (conservative) workaround would be to save the depth of the history-stack when executing "next statement", and disallow undo/redo beyond that depth.
I don't like any of these options.
Apparently there is no way to set read-only just for a region.

Error on launch and no output

I get the following error dialog when I run "Coq: Start".

Error loading syntax file "Packages/Sublime-Coq/Coq Toplevel.sublime-syntax": Unable to read Packages/Sublime-Coq/Coq Toplevel.sublime-syntax

After dismissing it, the *COQTOP* pane opens but there is no output. I also tried creating a user settings file containing

{
	"coqtop_path": "/usr/local/bin/coqtop"
}

but it has no effect. How can I debug this?

seems some new keywords are not supported

e.g. Module and `End'.
see file Arguments.v from Coq repo.

(* coq-prog-args: ("-top" "Arguments") *)
Arguments Nat.sub n m : simpl nomatch.
About Nat.sub.
Arguments Nat.sub n / m : simpl nomatch.
About Nat.sub.
Arguments Nat.sub !n / m : simpl nomatch.
About Nat.sub.
Arguments Nat.sub !n !m /.
About Nat.sub.
Arguments Nat.sub !n !m.
About Nat.sub.
Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
  fun x => (f (fst x), g (snd x)).
Declare Scope foo_scope.
Declare Scope bar_scope.
Delimit Scope foo_scope with F.
Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
About pf.
Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
Arguments fcomp {_ _ _}%type_scope f g x /.
About fcomp.
Definition volatile := fun x : nat => x.
Arguments volatile / _.
About volatile.
Set Implicit Arguments.
Section S1.
Variable T1 : Type.
Section S2.
Variable T2 : Type.
Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat :=
  match n, m with
  | 0,_ => 0
  | S _, 0 => n
  | S n', S m' => f x y n' v m' end.
About f.
Global Arguments f x y !n !v !m.
About f.
End S2.
About f.
End S1.
About f.
Eval cbn in forall v, f 0 0 5 v 3 = 2.
Eval cbn in f 0 0 5 tt 3 = 2.
Arguments f : clear implicits and scopes.
About f.
Record r := { pi :> nat -> bool -> unit }.
Notation "$" := 3 (only parsing) : foo_scope.
Notation "$" := true (only parsing) : bar_scope.
Delimit Scope bar_scope with B.
Arguments pi _ _%F _%B.
Check (forall w : r, pi w $ $ = tt).
Fail Check (forall w : r, w $ $ = tt).
Axiom w : r.
Arguments w  x%F y%B : extra scopes.
Check (w $ $ = tt).
Fail Arguments w  _%F _%B.

Definition volatilematch (n : nat) :=
  match n with
  | O => O
  | S p => p
  end.

Arguments volatilematch / n : simpl nomatch.
About volatilematch.
Eval simpl in fun n => volatilematch n.

Module Formatting.

Parameter A : Type.
Parameter f : forall (xxxxxxxxxxxxxx : A) (xxxxxxxxxxxxxx' : nat) (xxxxxxxxxxxxxx'' : nat) (xxxxxxxxxxxxxx''' : nat), xxxxxxxxxxxxxx' + xxxxxxxxxxxxxx' + xxxxxxxxxxxxxx'' = 0.
Print f.

End Formatting.

support _CoqProject files

coqide, proofgeneral, vscoq all support _CoqProject; it would be nice if sublime-coq could too. not sure how the correct way to invoke it though

No output on launch, no error message (Windows)

• Installed via Package Control on a completely new ST3 3211
• Able to use command palette to run "Coq: Start", which opens the Coq pane, however no output is written to the pain, and none of the shortcuts seem to do anything at all.

I've spent the day trying to debug the issue but honestly have gotten nowhere.

I've created the user settings file which contains:
{ "coqtop_path": "C:/Coq/bin/coqtop.exe" }
and I've also tried numerous different ways of specifying the path, from 'C:\Coq\...', 'C:/Coq/...', etc. None seem to have any effect.

seems double-quoted strings are not supported

file Arguments.v from Coq official repo has them.

Notation "$" := 3 (only parsing) : foo_scope.
Notation "$" := true (only parsing) : bar_scope.

strange highlight in ST4

File is Arguments.v from the Coq GitHub repo.
Why red highlights?

(* coq-prog-args: ("-top" "Arguments") *)
Arguments Nat.sub n m : simpl nomatch.
About Nat.sub.
Arguments Nat.sub n / m : simpl nomatch.
About Nat.sub.
Arguments Nat.sub !n / m : simpl nomatch.
About Nat.sub.
Arguments Nat.sub !n !m /.
About Nat.sub.
Arguments Nat.sub !n !m.
About Nat.sub.
Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
  fun x => (f (fst x), g (snd x)).
Declare Scope foo_scope.
Declare Scope bar_scope.
Delimit Scope foo_scope with F.
Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
About pf.
Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
Arguments fcomp {_ _ _}%type_scope f g x /.
About fcomp.
Definition volatile := fun x : nat => x.
Arguments volatile / _.
About volatile.
Set Implicit Arguments.
Section S1.
Variable T1 : Type.
Section S2.
Variable T2 : Type.
Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat :=
  match n, m with
  | 0,_ => 0
  | S _, 0 => n
  | S n', S m' => f x y n' v m' end.
About f.
Global Arguments f x y !n !v !m.
About f.
End S2.
About f.
End S1.
About f.
Eval cbn in forall v, f 0 0 5 v 3 = 2.
Eval cbn in f 0 0 5 tt 3 = 2.
Arguments f : clear implicits and scopes.
About f.
Record r := { pi :> nat -> bool -> unit }.
Notation "$" := 3 (only parsing) : foo_scope.
Notation "$" := true (only parsing) : bar_scope.
Delimit Scope bar_scope with B.
Arguments pi _ _%F _%B.
Check (forall w : r, pi w $ $ = tt).
Fail Check (forall w : r, w $ $ = tt).
Axiom w : r.
Arguments w  x%F y%B : extra scopes.
Check (w $ $ = tt).
Fail Arguments w  _%F _%B.

Definition volatilematch (n : nat) :=
  match n with
  | O => O
  | S p => p
  end.

Arguments volatilematch / n : simpl nomatch.
About volatilematch.
Eval simpl in fun n => volatilematch n.

Module Formatting.

Parameter A : Type.
Parameter f : forall (xxxxxxxxxxxxxx : A) (xxxxxxxxxxxxxx' : nat) (xxxxxxxxxxxxxx'' : nat) (xxxxxxxxxxxxxx''' : nat), xxxxxxxxxxxxxx' + xxxxxxxxxxxxxx' + xxxxxxxxxxxxxx'' = 0.
Print f.

End Formatting.

Can't find Coq: Start

After install, I can find set syntax: coq in the command palette but I can't find Coq: Start

set pwd as active file's folder, rather than active window's folder

i often find it more useful for the pwd to be the active file's folder, rather than the active window's folder, and i imagine this is also more intuitive behavior. something like pwd = os.path.dirname(sublime.active_window().active_view().file_name()) in line 46 of __init__.py?

Does not work if the current window is not opened as a folder

This is related to #15; if the current file is not opened as part of a folder (ie. it's just the file itself), then coq fails to start. I get this backtrace:

Traceback (most recent call last):
  File "/Applications/Sublime Text.app/Contents/MacOS/sublime_plugin.py", line 1088, in run_
    return self.run(edit)
  File "/Users/zhiayang/Library/Application Support/Sublime Text 3/Installed Packages/Coq.sublime-package/__init__.py", line 207, in run
  File "/Users/zhiayang/Library/Application Support/Sublime Text 3/Installed Packages/Coq.sublime-package/__init__.py", line 46, in start
IndexError: list index out of range

Using ST3 3.2.2, build 3211, the current up-to-date build on PackageControl.

undoing search / about / locate / compute undoes previous statement

consider the following. step through up to the "Search" line. then step backwards, then step forward, and step forward again. "simpl." does not run, because when we stepped backward from "Search" it undoes the "Proof" opening.

Theorem test : False.
Proof.
  Search (_ + _ = _).
  simpl.
Admitted.

i think the fix should be to add more comment keywords; Search, About, Locate, Compute should also be there?