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

Abella

by JimmyZJX ST3

No description provided

Details

Installs

  • Total 1K
  • Win 1K
  • Mac 163
  • Linux 100
Jun 13 Jun 12 Jun 11 Jun 10 Jun 9 Jun 8 Jun 7 Jun 6 Jun 5 Jun 4 Jun 3 Jun 2 Jun 1 May 31 May 30 May 29 May 28 May 27 May 26 May 25 May 24 May 23 May 22 May 21 May 20 May 19 May 18 May 17 May 16 May 15 May 14 May 13 May 12 May 11 May 10 May 9 May 8 May 7 May 6 May 5 May 4 May 3 May 2 May 1 Apr 30
Windows 0 0 0 0 2 0 0 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 2 0 0 0 0 0 0 1
Mac 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 1 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0
Linux 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 0 0 0 0 0 0 1 0 0 0 0 0 0
01234Jun 13Jun 10Jun 7Jun 4Jun 1May 29May 26May 23May 20May 17May 14May 11May 8May 5May 2Jun 13 Linux: 0 Mac: 0 Windows: 0Jun 12 Linux: 0 Mac: 0 Windows: 0Jun 11 Linux: 0 Mac: 0 Windows: 0Jun 10 Linux: 0 Mac: 0 Windows: 0Jun 9 Linux: 0 Mac: 0 Windows: 2Jun 8 Linux: 0 Mac: 0 Windows: 0Jun 7 Linux: 0 Mac: 0 Windows: 0Jun 6 Linux: 0 Mac: 0 Windows: 0Jun 5 Linux: 0 Mac: 0 Windows: 1Jun 4 Linux: 0 Mac: 0 Windows: 0Jun 3 Linux: 0 Mac: 0 Windows: 0Jun 2 Linux: 0 Mac: 0 Windows: 0Jun 1 Linux: 0 Mac: 0 Windows: 0May 31 Linux: 0 Mac: 0 Windows: 0May 30 Linux: 0 Mac: 0 Windows: 0May 29 Linux: 0 Mac: 0 Windows: 0May 28 Linux: 0 Mac: 0 Windows: 1May 27 Linux: 0 Mac: 0 Windows: 0May 26 Linux: 0 Mac: 0 Windows: 0May 25 Linux: 0 Mac: 0 Windows: 0May 24 Linux: 0 Mac: 0 Windows: 0May 23 Linux: 0 Mac: 0 Windows: 0May 22 Linux: 0 Mac: 0 Windows: 0May 21 Linux: 0 Mac: 0 Windows: 0May 20 Linux: 0 Mac: 0 Windows: 0May 19 Linux: 0 Mac: 0 Windows: 0May 18 Linux: 0 Mac: 1 Windows: 0May 17 Linux: 0 Mac: 0 Windows: 0May 16 Linux: 0 Mac: 0 Windows: 1May 15 Linux: 0 Mac: 0 Windows: 0May 14 Linux: 0 Mac: 0 Windows: 0May 13 Linux: 0 Mac: 0 Windows: 0May 12 Linux: 0 Mac: 0 Windows: 0May 11 Linux: 0 Mac: 0 Windows: 0May 10 Linux: 0 Mac: 0 Windows: 0May 9 Linux: 0 Mac: 0 Windows: 0May 8 Linux: 0 Mac: 0 Windows: 0May 7 Linux: 0 Mac: 1 Windows: 2May 6 Linux: 1 Mac: 0 Windows: 0May 5 Linux: 0 Mac: 0 Windows: 0May 4 Linux: 0 Mac: 0 Windows: 0May 3 Linux: 0 Mac: 0 Windows: 0May 2 Linux: 0 Mac: 0 Windows: 0May 1 Linux: 0 Mac: 0 Windows: 0Apr 30 Linux: 0 Mac: 0 Windows: 1Jun 13 Linux: 0 Mac: 0 Windows: 0Jun 12 Linux: 0 Mac: 0 Windows: 0Jun 11 Linux: 0 Mac: 0 Windows: 0Jun 10 Linux: 0 Mac: 0 Windows: 0Jun 9 Linux: 0 Mac: 0 Windows: 2Jun 8 Linux: 0 Mac: 0 Windows: 0Jun 7 Linux: 0 Mac: 0 Windows: 0Jun 6 Linux: 0 Mac: 0 Windows: 0Jun 5 Linux: 0 Mac: 0 Windows: 1Jun 4 Linux: 0 Mac: 0 Windows: 0Jun 3 Linux: 0 Mac: 0 Windows: 0Jun 2 Linux: 0 Mac: 0 Windows: 0Jun 1 Linux: 0 Mac: 0 Windows: 0May 31 Linux: 0 Mac: 0 Windows: 0May 30 Linux: 0 Mac: 0 Windows: 0May 29 Linux: 0 Mac: 0 Windows: 0May 28 Linux: 0 Mac: 0 Windows: 1May 27 Linux: 0 Mac: 0 Windows: 0May 26 Linux: 0 Mac: 0 Windows: 0May 25 Linux: 0 Mac: 0 Windows: 0May 24 Linux: 0 Mac: 0 Windows: 0May 23 Linux: 0 Mac: 0 Windows: 0May 22 Linux: 0 Mac: 0 Windows: 0May 21 Linux: 0 Mac: 0 Windows: 0May 20 Linux: 0 Mac: 0 Windows: 0May 19 Linux: 0 Mac: 0 Windows: 0May 18 Linux: 0 Mac: 1 Windows: 0May 17 Linux: 0 Mac: 0 Windows: 0May 16 Linux: 0 Mac: 0 Windows: 1May 15 Linux: 0 Mac: 0 Windows: 0May 14 Linux: 0 Mac: 0 Windows: 0May 13 Linux: 0 Mac: 0 Windows: 0May 12 Linux: 0 Mac: 0 Windows: 0May 11 Linux: 0 Mac: 0 Windows: 0May 10 Linux: 0 Mac: 0 Windows: 0May 9 Linux: 0 Mac: 0 Windows: 0May 8 Linux: 0 Mac: 0 Windows: 0May 7 Linux: 0 Mac: 1 Windows: 2May 6 Linux: 1 Mac: 0 Windows: 0May 5 Linux: 0 Mac: 0 Windows: 0May 4 Linux: 0 Mac: 0 Windows: 0May 3 Linux: 0 Mac: 0 Windows: 0May 2 Linux: 0 Mac: 0 Windows: 0May 1 Linux: 0 Mac: 0 Windows: 0Apr 30 Linux: 0 Mac: 0 Windows: 1Jun 13 Linux: 0 Mac: 0 Windows: 0Jun 12 Linux: 0 Mac: 0 Windows: 0Jun 11 Linux: 0 Mac: 0 Windows: 0Jun 10 Linux: 0 Mac: 0 Windows: 0Jun 9 Linux: 0 Mac: 0 Windows: 2Jun 8 Linux: 0 Mac: 0 Windows: 0Jun 7 Linux: 0 Mac: 0 Windows: 0Jun 6 Linux: 0 Mac: 0 Windows: 0Jun 5 Linux: 0 Mac: 0 Windows: 1Jun 4 Linux: 0 Mac: 0 Windows: 0Jun 3 Linux: 0 Mac: 0 Windows: 0Jun 2 Linux: 0 Mac: 0 Windows: 0Jun 1 Linux: 0 Mac: 0 Windows: 0May 31 Linux: 0 Mac: 0 Windows: 0May 30 Linux: 0 Mac: 0 Windows: 0May 29 Linux: 0 Mac: 0 Windows: 0May 28 Linux: 0 Mac: 0 Windows: 1May 27 Linux: 0 Mac: 0 Windows: 0May 26 Linux: 0 Mac: 0 Windows: 0May 25 Linux: 0 Mac: 0 Windows: 0May 24 Linux: 0 Mac: 0 Windows: 0May 23 Linux: 0 Mac: 0 Windows: 0May 22 Linux: 0 Mac: 0 Windows: 0May 21 Linux: 0 Mac: 0 Windows: 0May 20 Linux: 0 Mac: 0 Windows: 0May 19 Linux: 0 Mac: 0 Windows: 0May 18 Linux: 0 Mac: 1 Windows: 0May 17 Linux: 0 Mac: 0 Windows: 0May 16 Linux: 0 Mac: 0 Windows: 1May 15 Linux: 0 Mac: 0 Windows: 0May 14 Linux: 0 Mac: 0 Windows: 0May 13 Linux: 0 Mac: 0 Windows: 0May 12 Linux: 0 Mac: 0 Windows: 0May 11 Linux: 0 Mac: 0 Windows: 0May 10 Linux: 0 Mac: 0 Windows: 0May 9 Linux: 0 Mac: 0 Windows: 0May 8 Linux: 0 Mac: 0 Windows: 0May 7 Linux: 0 Mac: 1 Windows: 2May 6 Linux: 1 Mac: 0 Windows: 0May 5 Linux: 0 Mac: 0 Windows: 0May 4 Linux: 0 Mac: 0 Windows: 0May 3 Linux: 0 Mac: 0 Windows: 0May 2 Linux: 0 Mac: 0 Windows: 0May 1 Linux: 0 Mac: 0 Windows: 0Apr 30 Linux: 0 Mac: 0 Windows: 1

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+Down | Navigate to the end | | Ctrl+Shift+Enter | Kill Abella and reset the state | | Ctrl+';' | Lookup and show Theorem | | Alt+S | Execute a “search” command, and update the proof script if succeed | | Ctrl+B | Compile the current file (this is the standard ST “build” command) |

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 “ -> ” |

Notice that on OSX, the ctrl key is replaced by cmd (super).

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. The preference file can be found at [Preferences - Package Settings - 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",
},