src/Tools/VSCode/extension/README.md
author wenzelm
Sat May 11 19:08:26 2019 +0200 (5 months ago)
changeset 70265 a8238fd25541
parent 70234 4e0834322981
permissions -rw-r--r--
back to post-release mode;
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@70265
     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@70265
    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@70265
    61
  * Download a recent Isabelle development snapshot from
wenzelm@70265
    62
    <https://isabelle.in.tum.de/devel/release_snapshot>
wenzelm@66236
    63
wenzelm@66236
    64
  * Unpack and run the main Isabelle/jEdit application as usual, to ensure that
wenzelm@66236
    65
  the logic image is built properly and Isabelle works as expected.
wenzelm@66236
    66
wenzelm@66236
    67
  * Download and install VSCode from <https://code.visualstudio.com>
wenzelm@66236
    68
wenzelm@66236
    69
  * Open the VSCode *Extensions* view and install the following:
wenzelm@66236
    70
wenzelm@70265
    71
      + *Isabelle* (needs to fit to the underlying Isabelle release).
wenzelm@66236
    72
wenzelm@66236
    73
      + *Prettify Symbols Mode* (important for display of Isabelle symbols).
wenzelm@66236
    74
wenzelm@66236
    75
      + *bibtexLanguage* (optional): it gives `.bib` a formal status, thus
wenzelm@66236
    76
        `@{cite}` antiquotations become active for completion and hyperlinks.
wenzelm@66236
    77
wenzelm@66236
    78
  * Open the dialog *Preferences / User settings* and provide the following
wenzelm@66236
    79
    entries in the second window, where local user additions are stored:
wenzelm@66236
    80
wenzelm@66236
    81
      + On all platforms: `isabelle.home` needs to point to the main Isabelle
wenzelm@66236
    82
      directory (`$ISABELLE_HOME`).
wenzelm@66236
    83
wenzelm@66236
    84
      + On Windows: use drive-letter and backslashes for `isabelle.home` above.
wenzelm@66237
    85
      When running from a bare repository clone (not a development snapshot),
wenzelm@66237
    86
      `isabelle.cygwin_home` needs to point to a suitable Cygwin installation.
wenzelm@66236
    87
wenzelm@66236
    88
    Examples:
wenzelm@64873
    89
wenzelm@66236
    90
      + Linux:
wenzelm@66236
    91
        ```
wenzelm@70265
    92
        "isabelle.home": "/home/makarius/Isabelle"
wenzelm@66236
    93
        ```
wenzelm@66236
    94
wenzelm@66236
    95
      + Mac OS X:
wenzelm@66236
    96
        ```
wenzelm@70265
    97
        "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle"
wenzelm@66236
    98
        ```
wenzelm@66236
    99
wenzelm@66236
   100
      + Windows:
wenzelm@66236
   101
        ```
wenzelm@70265
   102
        "isabelle.home": "C:\\Users\\makarius\\Isabelle"
wenzelm@66236
   103
        ```
wenzelm@66218
   104
wenzelm@66236
   105
  * Restart the VSCode application to ensure that all extensions are properly
wenzelm@66236
   106
  initialized and user settings are updated. Afterwards VSCode should know about
wenzelm@66236
   107
  `.thy` files (Isabelle theories) and `.ML` files (Isabelle/ML modules).
wenzelm@66236
   108
wenzelm@66240
   109
  The Isabelle extension is initialized when the first Isabelle file is opened.
wenzelm@66240
   110
  It requires a few seconds to start up: a small popup window eventually says
wenzelm@66240
   111
  *"Welcome to Isabelle ..."*. If that fails, there might be something wrong
wenzelm@66240
   112
  with `isabelle.home` from above, or the Isabelle distribution does not fit to
wenzelm@66240
   113
  the version of the VSCode extension from the Marketplace.
wenzelm@66236
   114
wenzelm@66236
   115
wenzelm@66236
   116
### Support for Isabelle symbols
wenzelm@66236
   117
wenzelm@66236
   118
Isabelle symbols like `\<forall>` are rendered using the extension *Prettify
wenzelm@66236
   119
Symbols Mode*, which needs to be installed separately.
wenzelm@66236
   120
wenzelm@66236
   121
In addition, the following user settings should be changed in the *Preferences /
wenzelm@66236
   122
User settings* dialog of VSCode:
wenzelm@66218
   123
wenzelm@66218
   124
```
wenzelm@66218
   125
"prettifySymbolsMode.substitutions": [
wenzelm@66218
   126
  {
wenzelm@66218
   127
    "language": "isabelle",
wenzelm@66218
   128
    "revealOn": "none",
wenzelm@66218
   129
    "adjustCursorMovement": true,
wenzelm@66218
   130
    "prettyCursor": "none",
wenzelm@66218
   131
    "substitutions": []
wenzelm@66218
   132
  },
wenzelm@66218
   133
  {
wenzelm@66218
   134
    "language": "isabelle-ml",
wenzelm@66218
   135
    "revealOn": "none",
wenzelm@66218
   136
    "adjustCursorMovement": true,
wenzelm@66218
   137
    "prettyCursor": "none",
wenzelm@66218
   138
    "substitutions": []
wenzelm@66218
   139
  }]
wenzelm@66218
   140
```
wenzelm@66218
   141
wenzelm@66236
   142
Actual symbol replacement tables are provided by the prover process on startup,
wenzelm@66236
   143
based on the usual `etc/symbols` specifications of the Isabelle installation.
wenzelm@66218
   144
wenzelm@66236
   145
wenzelm@66236
   146
### Further Preferences
wenzelm@66218
   147
wenzelm@66218
   148
  * Preferred Color Theme: `Light+ (default light)`
wenzelm@66218
   149
wenzelm@66236
   150
  * Alternative Color Theme: `Dark+ (default dark)` – with restrictions: some
wenzelm@66236
   151
  color combinations don't work out properly.
wenzelm@66218
   152
wenzelm@66218
   153
  * Recommended changes to default VSCode settings:
wenzelm@66218
   154
wenzelm@66218
   155
    ```
wenzelm@66223
   156
    "editor.acceptSuggestionOnEnter": "off",
wenzelm@66223
   157
    "editor.lineNumbers": "off",
wenzelm@66223
   158
    "editor.renderIndentGuides": false,
wenzelm@66236
   159
    "editor.rulers": [80, 100],
wenzelm@66223
   160
    "editor.wordBasedSuggestions": true,
wenzelm@66218
   161
    ```
wenzelm@66236
   162
wenzelm@66237
   163
## Known Limitations of Isabelle/VSCode
wenzelm@66236
   164
wenzelm@69343
   165
  * Lack of specific support for the Isabelle fonts: these need to be
wenzelm@66237
   166
  manually installed on the system and configured for VSCode (see also
wenzelm@66236
   167
  `$ISABELLE_FONTS` within the Isabelle environment).
wenzelm@66236
   168
wenzelm@66237
   169
    **Note:** As the Isabelle fonts continue to evolve, installed versions need
wenzelm@66236
   170
    to be updated according to each new Isabelle version.
wenzelm@66236
   171
wenzelm@66236
   172
  * Isabelle symbols are merely an optical illusion: it would be better to make
wenzelm@66236
   173
    them a first-class Unicode charset as in Isabelle/jEdit.
wenzelm@66236
   174
wenzelm@66236
   175
  * Isabelle symbol abbreviations like "-->" are not accepted by VSCode.
wenzelm@66236
   176
wenzelm@66237
   177
  * Lack of formal editor perspective in VSCode: only the cursor position is
wenzelm@66237
   178
  used (with some surrounding lines of text).
wenzelm@66236
   179
wenzelm@66236
   180
  * Lack of formal markup in prover messages and popups.
wenzelm@66236
   181
wenzelm@66237
   182
  * Lack of pretty-printing (logical line breaks) according to window and font
wenzelm@66236
   183
  dimensions.
wenzelm@66236
   184
wenzelm@66236
   185
  * Lack of GUI panels for Sledgehammer, Query operations etc.
wenzelm@66240
   186
wenzelm@66240
   187
  * Big theory files may cause problems to the VSCode rendering engine, since
wenzelm@66240
   188
  messages and text decorations are applied to the text as a whole (cf. the
wenzelm@66240
   189
  minimap view).