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