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

Abella

by JimmyZJX ST3

No description provided

Details

Installs

  • Total 211
  • Win 166
  • Mac 27
  • Linux 18
Jan 25 Jan 24 Jan 23 Jan 22 Jan 21 Jan 20 Jan 19 Jan 18 Jan 17 Jan 16 Jan 15 Jan 14 Jan 13 Jan 12 Jan 11 Jan 10 Jan 9 Jan 8 Jan 7 Jan 6 Jan 5 Jan 4 Jan 3 Jan 2 Jan 1 Dec 31 Dec 30 Dec 29 Dec 28 Dec 27 Dec 26 Dec 25 Dec 24 Dec 23 Dec 22 Dec 21 Dec 20 Dec 19 Dec 18 Dec 17 Dec 16 Dec 15 Dec 14 Dec 13 Dec 12
Windows 0 0 1 3 2 4 1 2 0 0 1 1 1 0 0 0 0 0 0 0 0 0 1 0 0 0 0 6 2 0 1 2 0 2 1 0 0 0 0 1 1 0 0 1 0
Mac 0 0 1 0 0 0 0 0 0 0 0 1 0 1 1 0 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 2 0 0 0 0 0
Linux 0 0 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 1 0

Readme

Source
raw.​githubusercontent.​com

Abella for Sublime Text 3

Support for the Abella theorem prover in Sublime Text 3.

The develop of this plugin is mainly based on a Coq plugin for ST.

Installation

The recommended way to install Sublime Abella 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:JimmyZJX/SublimeAbella.git Abella

Usage

You need to open an Abella script file (*.thm) in ST3, and the following default key bindings should work: | | | | —————- | —————————————————————— | | Ctrl+Enter | Start Abella (if necessary) and navigate to cursor. | | Ctrl+Down | Navigate to the next statement. | | Ctrl+Up | Undo last statement | | Ctrl+Right | Navigate to cursor (basically equivalent to Ctrl+Enter) | | Ctrl+Left | Reload Abella, and go to cursor | | Ctrl+Shift+Enter | Kill Abella and reset the state | | Ctrl+';' | Show Theorem | | Alt+S | Execute a “search” command, and update the proof script if succeed |

And there are also shortcuts that help writing proofs: | | | | ——— | ———————————————— | | Ctrl+7 | (7 stands for “&”, and) insert text “ /\ ” | | Ctrl+'\' | ('\' stands for “ | ”, or) insert text “ \/ ” | | Ctrl+'.' | ('.' stands for “>”, arrow) insert text “ -> ” |

Auto-Next

When Abella plugin is started, inserting a '.' that ends just the next tactic automatically triggers a navigation to that tactic (same effect as Ctrl+Enter/Down).

Executable

The abella executable should be in PATH by default.

If you want to change the location, edit your user setting abella.exec and point to the currect file. The default value is abella, and you may change it to /path/to/abella.

Highlighting

In order to get nice background highlighting for the proven parts of the file, add the following snippet to your color scheme file.

(If you are not sure what I'm talking about, install the plugin PackageResourceViewer, execute the command PackageResourceViewer: Extract Package and select Color Scheme - Default, then click Preferences-Browse Packages, find and edit Color Scheme - Default/Monokai.sublime-color-scheme)

For tmTheme syntax:

dark themes

<dict>
  <key>name</key>
  <string>Proven with Abella</string>
  <key>scope</key>
  <string>meta.abella.proven</string>
  <key>settings</key>
  <dict>
    <key>background</key>
    <string>#365A28</string>
    <key>foreground</key>
    <string>#51873C</string>
  </dict>
</dict>

light themes

<dict>
  <key>name</key>
  <string>Proven with Abella</string>
  <key>scope</key>
  <string>meta.abella.proven</string>
  <key>settings</key>
  <dict>
    <key>background</key>
    <string>#002800</string>
  </dict>
</dict>

For sublime-color-scheme syntax:

dark themes

{
    "name": "Proven with Abella",
    "scope": "meta.abella.proven",
    "background": "#365A28",
    "foreground": "#51873C"
},

light themes

{
    "name": "Proven with Abella",
    "scope": "meta.abella.proven",
    "background": "#002800",
},