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