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