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