src/Tools/VSCode/extension/README.md
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69343 395c4fb15ea2
child 70234 4e0834322981
permissions -rw-r--r--
more strict AFP properties;
wenzelm@64757
     1
# Isabelle Prover IDE support
wenzelm@64757
     2
wenzelm@66598
     3
This extension connects VSCode to the Isabelle Prover IDE infrastructure: it
wenzelm@68870
     4
requires a repository version of Isabelle.
wenzelm@66236
     5
wenzelm@66236
     6
The implementation is centered around the VSCode Language Server protocol, but
wenzelm@66237
     7
with many add-ons that are specific to VSCode and Isabelle/PIDE.
wenzelm@66236
     8
wenzelm@66236
     9
See also:
wenzelm@64605
    10
wenzelm@68870
    11
  * <https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
wenzelm@66237
    12
  * <https://github.com/Microsoft/language-server-protocol>
wenzelm@64757
    13
wenzelm@66237
    14
wenzelm@66237
    15
## Screenshot
wenzelm@66237
    16
wenzelm@66390
    17
![[Isabelle/VSCode]](https://isabelle.in.tum.de/repos/isabelle/raw-file/b565a39627bb/src/Tools/VSCode/extension/isabelle_vscode.png)
wenzelm@66227
    18
wenzelm@64605
    19
wenzelm@66236
    20
## Notable Features
wenzelm@66236
    21
wenzelm@66236
    22
  * Static syntax tables for Isabelle `.thy` and `.ML` files.
wenzelm@66236
    23
wenzelm@66236
    24
  * Implicit dependency management of sources, subject to changes of theory
wenzelm@66236
    25
  files within the editor, as well as external file-system events.
wenzelm@66218
    26
wenzelm@66236
    27
  * Implicit formal checking of theory files, using the *cursor position* of the
wenzelm@66236
    28
  active editor panel as indication for relevant spots.
wenzelm@66236
    29
wenzelm@66240
    30
  * Text overview lane with formal status of prover commands (unprocessed,
wenzelm@66240
    31
  running, error, warning).
wenzelm@66240
    32
wenzelm@66236
    33
  * Prover messages within the source text (errors/warnings and information
wenzelm@66236
    34
  messages).
wenzelm@66236
    35
wenzelm@66236
    36
  * Semantic text decorations: colors for free/bound variables, inferred types
wenzelm@66236
    37
  etc.
wenzelm@64757
    38
wenzelm@66236
    39
  * Visual indication of formal scopes and hyperlinks for formal entities.
wenzelm@66236
    40
wenzelm@66237
    41
  * Implicit proof state output via the VSCode message channel "Isabelle
wenzelm@66237
    42
  Output".
wenzelm@66236
    43
wenzelm@66236
    44
  * Explicit proof state output via separate GUI panel (command
wenzelm@66236
    45
  `isabelle.state`).
wenzelm@64948
    46
wenzelm@66236
    47
  * HTML preview via separate GUI panel (command `isabelle.preview`).
wenzelm@66236
    48
wenzelm@66237
    49
  * Rich completion information: Isabelle symbols (e.g. `\forall` or
wenzelm@66237
    50
  `\<forall>`), outer syntax keywords, formal entities, file-system paths,
wenzelm@66237
    51
  BibTeX entries etc.
wenzelm@66236
    52
wenzelm@66236
    53
  * Spell-checking of informal texts, including dictionary operations: via the
wenzelm@66236
    54
  regular completion dialog.
wenzelm@64948
    55
wenzelm@66227
    56
wenzelm@66236
    57
## Requirements
wenzelm@66236
    58
wenzelm@66240
    59
### Isabelle/VSCode Installation
wenzelm@66236
    60
wenzelm@68870
    61
  * Download a recent Isabelle development snapshot from <http://isabelle.in.tum.de/devel/release_snapshot>
wenzelm@66236
    62
wenzelm@66236
    63
  * Unpack and run the main Isabelle/jEdit application as usual, to ensure that
wenzelm@66236
    64
  the logic image is built properly and Isabelle works as expected.
wenzelm@66236
    65
wenzelm@66236
    66
  * Download and install VSCode from <https://code.visualstudio.com>
wenzelm@66236
    67
wenzelm@66236
    68
  * Open the VSCode *Extensions* view and install the following:
wenzelm@66236
    69
wenzelm@68870
    70
      + *Isabelle*.
wenzelm@66236
    71
wenzelm@66236
    72
      + *Prettify Symbols Mode* (important for display of Isabelle symbols).
wenzelm@66236
    73
wenzelm@66236
    74
      + *bibtexLanguage* (optional): it gives `.bib` a formal status, thus
wenzelm@66236
    75
        `@{cite}` antiquotations become active for completion and hyperlinks.
wenzelm@66236
    76
wenzelm@66236
    77
  * Open the dialog *Preferences / User settings* and provide the following
wenzelm@66236
    78
    entries in the second window, where local user additions are stored:
wenzelm@66236
    79
wenzelm@66236
    80
      + On all platforms: `isabelle.home` needs to point to the main Isabelle
wenzelm@66236
    81
      directory (`$ISABELLE_HOME`).
wenzelm@66236
    82
wenzelm@66236
    83
      + On Windows: use drive-letter and backslashes for `isabelle.home` above.
wenzelm@66237
    84
      When running from a bare repository clone (not a development snapshot),
wenzelm@66237
    85
      `isabelle.cygwin_home` needs to point to a suitable Cygwin installation.
wenzelm@66236
    86
wenzelm@66236
    87
    Examples:
wenzelm@64873
    88
wenzelm@66236
    89
      + Linux:
wenzelm@66236
    90
        ```
wenzelm@68870
    91
        "isabelle.home": "/home/makarius/Isabelle"
wenzelm@66236
    92
        ```
wenzelm@66236
    93
wenzelm@66236
    94
      + Mac OS X:
wenzelm@66236
    95
        ```
wenzelm@68870
    96
        "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
wenzelm@66236
    97
        ```
wenzelm@66236
    98
wenzelm@66236
    99
      + Windows:
wenzelm@66236
   100
        ```
wenzelm@68870
   101
        "isabelle.home": "C:\\Users\\makarius\\Isabelle"
wenzelm@66236
   102
        ```
wenzelm@66218
   103
wenzelm@66236
   104
  * Restart the VSCode application to ensure that all extensions are properly
wenzelm@66236
   105
  initialized and user settings are updated. Afterwards VSCode should know about
wenzelm@66236
   106
  `.thy` files (Isabelle theories) and `.ML` files (Isabelle/ML modules).
wenzelm@66236
   107
wenzelm@66240
   108
  The Isabelle extension is initialized when the first Isabelle file is opened.
wenzelm@66240
   109
  It requires a few seconds to start up: a small popup window eventually says
wenzelm@66240
   110
  *"Welcome to Isabelle ..."*. If that fails, there might be something wrong
wenzelm@66240
   111
  with `isabelle.home` from above, or the Isabelle distribution does not fit to
wenzelm@66240
   112
  the version of the VSCode extension from the Marketplace.
wenzelm@66236
   113
wenzelm@66236
   114
wenzelm@66236
   115
### Support for Isabelle symbols
wenzelm@66236
   116
wenzelm@66236
   117
Isabelle symbols like `\<forall>` are rendered using the extension *Prettify
wenzelm@66236
   118
Symbols Mode*, which needs to be installed separately.
wenzelm@66236
   119
wenzelm@66236
   120
In addition, the following user settings should be changed in the *Preferences /
wenzelm@66236
   121
User settings* dialog of VSCode:
wenzelm@66218
   122
wenzelm@66218
   123
```
wenzelm@66218
   124
"prettifySymbolsMode.substitutions": [
wenzelm@66218
   125
  {
wenzelm@66218
   126
    "language": "isabelle",
wenzelm@66218
   127
    "revealOn": "none",
wenzelm@66218
   128
    "adjustCursorMovement": true,
wenzelm@66218
   129
    "prettyCursor": "none",
wenzelm@66218
   130
    "substitutions": []
wenzelm@66218
   131
  },
wenzelm@66218
   132
  {
wenzelm@66218
   133
    "language": "isabelle-ml",
wenzelm@66218
   134
    "revealOn": "none",
wenzelm@66218
   135
    "adjustCursorMovement": true,
wenzelm@66218
   136
    "prettyCursor": "none",
wenzelm@66218
   137
    "substitutions": []
wenzelm@66218
   138
  }]
wenzelm@66218
   139
```
wenzelm@66218
   140
wenzelm@66236
   141
Actual symbol replacement tables are provided by the prover process on startup,
wenzelm@66236
   142
based on the usual `etc/symbols` specifications of the Isabelle installation.
wenzelm@66218
   143
wenzelm@66236
   144
wenzelm@66236
   145
### Further Preferences
wenzelm@66218
   146
wenzelm@66218
   147
  * Preferred Color Theme: `Light+ (default light)`
wenzelm@66218
   148
wenzelm@66236
   149
  * Alternative Color Theme: `Dark+ (default dark)` – with restrictions: some
wenzelm@66236
   150
  color combinations don't work out properly.
wenzelm@66218
   151
wenzelm@66218
   152
  * Recommended changes to default VSCode settings:
wenzelm@66218
   153
wenzelm@66218
   154
    ```
wenzelm@66223
   155
    "editor.acceptSuggestionOnEnter": "off",
wenzelm@66223
   156
    "editor.lineNumbers": "off",
wenzelm@66223
   157
    "editor.renderIndentGuides": false,
wenzelm@66236
   158
    "editor.rulers": [80, 100],
wenzelm@66223
   159
    "editor.wordBasedSuggestions": true,
wenzelm@66218
   160
    ```
wenzelm@66236
   161
wenzelm@66237
   162
## Known Limitations of Isabelle/VSCode
wenzelm@66236
   163
wenzelm@69343
   164
  * Lack of specific support for the Isabelle fonts: these need to be
wenzelm@66237
   165
  manually installed on the system and configured for VSCode (see also
wenzelm@66236
   166
  `$ISABELLE_FONTS` within the Isabelle environment).
wenzelm@66236
   167
wenzelm@66237
   168
    **Note:** As the Isabelle fonts continue to evolve, installed versions need
wenzelm@66236
   169
    to be updated according to each new Isabelle version.
wenzelm@66236
   170
wenzelm@66236
   171
  * Isabelle symbols are merely an optical illusion: it would be better to make
wenzelm@66236
   172
    them a first-class Unicode charset as in Isabelle/jEdit.
wenzelm@66236
   173
wenzelm@66236
   174
  * Isabelle symbol abbreviations like "-->" are not accepted by VSCode.
wenzelm@66236
   175
wenzelm@66237
   176
  * Lack of formal editor perspective in VSCode: only the cursor position is
wenzelm@66237
   177
  used (with some surrounding lines of text).
wenzelm@66236
   178
wenzelm@66236
   179
  * Lack of formal markup in prover messages and popups.
wenzelm@66236
   180
wenzelm@66237
   181
  * Lack of pretty-printing (logical line breaks) according to window and font
wenzelm@66236
   182
  dimensions.
wenzelm@66236
   183
wenzelm@66236
   184
  * Lack of GUI panels for Sledgehammer, Query operations etc.
wenzelm@66240
   185
wenzelm@66240
   186
  * Big theory files may cause problems to the VSCode rendering engine, since
wenzelm@66240
   187
  messages and text decorations are applied to the text as a whole (cf. the
wenzelm@66240
   188
  minimap view).