author | wenzelm |
Fri, 29 Jun 2018 20:32:24 +0200 | |
changeset 68546 | 34d732a83767 |
parent 67866 | 11e4060bcdca |
child 68870 | 53a75627aab7 |
permissions | -rw-r--r-- |
64757 | 1 |
# Isabelle Prover IDE support |
2 |
||
66598 | 3 |
This extension connects VSCode to the Isabelle Prover IDE infrastructure: it |
68546 | 4 |
requires Isabelle2018. |
66236 | 5 |
|
6 |
The implementation is centered around the VSCode Language Server protocol, but |
|
66237 | 7 |
with many add-ons that are specific to VSCode and Isabelle/PIDE. |
66236 | 8 |
|
9 |
See also: |
|
64605 | 10 |
|
68546 | 11 |
* <https://isabelle.in.tum.de/website-Isabelle2018> |
12 |
* <https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/Tools/VSCode> |
|
66237 | 13 |
* <https://github.com/Microsoft/language-server-protocol> |
64757 | 14 |
|
66237 | 15 |
|
16 |
## Screenshot |
|
17 |
||
66390
21514c6e5e43
prefer https for the sake of "npm run vscode:prepublish";
wenzelm
parents:
66240
diff
changeset
|
18 |
![[Isabelle/VSCode]](https://isabelle.in.tum.de/repos/isabelle/raw-file/b565a39627bb/src/Tools/VSCode/extension/isabelle_vscode.png) |
66227 | 19 |
|
64605 | 20 |
|
66236 | 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. |
|
66218 | 27 |
|
66236 | 28 |
* Implicit formal checking of theory files, using the *cursor position* of the |
29 |
active editor panel as indication for relevant spots. |
|
30 |
||
66240 | 31 |
* Text overview lane with formal status of prover commands (unprocessed, |
32 |
running, error, warning). |
|
33 |
||
66236 | 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. |
|
64757 | 39 |
|
66236 | 40 |
* Visual indication of formal scopes and hyperlinks for formal entities. |
41 |
||
66237 | 42 |
* Implicit proof state output via the VSCode message channel "Isabelle |
43 |
Output". |
|
66236 | 44 |
|
45 |
* Explicit proof state output via separate GUI panel (command |
|
46 |
`isabelle.state`). |
|
64948 | 47 |
|
66236 | 48 |
* HTML preview via separate GUI panel (command `isabelle.preview`). |
49 |
||
66237 | 50 |
* Rich completion information: Isabelle symbols (e.g. `\forall` or |
51 |
`\<forall>`), outer syntax keywords, formal entities, file-system paths, |
|
52 |
BibTeX entries etc. |
|
66236 | 53 |
|
54 |
* Spell-checking of informal texts, including dictionary operations: via the |
|
55 |
regular completion dialog. |
|
64948 | 56 |
|
66227 | 57 |
|
66236 | 58 |
## Requirements |
59 |
||
66240 | 60 |
### Isabelle/VSCode Installation |
66236 | 61 |
|
68546 | 62 |
* Download Isabelle2018 from <https://isabelle.in.tum.de/website-Isabelle2018> |
63 |
or any of its mirror sites. |
|
66236 | 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 |
||
68546 | 72 |
+ *Isabelle2018* (needs to fit to the underlying Isabelle release). |
66236 | 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. |
|
66237 | 86 |
When running from a bare repository clone (not a development snapshot), |
87 |
`isabelle.cygwin_home` needs to point to a suitable Cygwin installation. |
|
66236 | 88 |
|
89 |
Examples: |
|
64873 | 90 |
|
66236 | 91 |
+ Linux: |
92 |
``` |
|
68546 | 93 |
"isabelle.home": "/home/makarius/Isabelle2018" |
66236 | 94 |
``` |
95 |
||
96 |
+ Mac OS X: |
|
97 |
``` |
|
68546 | 98 |
"isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2018" |
66236 | 99 |
``` |
100 |
||
101 |
+ Windows: |
|
102 |
``` |
|
68546 | 103 |
"isabelle.home": "C:\\Users\\makarius\\Isabelle2018" |
66236 | 104 |
``` |
66218 | 105 |
|
66236 | 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 |
||
66240 | 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. |
|
66236 | 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: |
|
66218 | 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 |
||
66236 | 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. |
|
66218 | 145 |
|
66236 | 146 |
|
147 |
### Further Preferences |
|
66218 | 148 |
|
149 |
* Preferred Color Theme: `Light+ (default light)` |
|
150 |
||
66236 | 151 |
* Alternative Color Theme: `Dark+ (default dark)` – with restrictions: some |
152 |
color combinations don't work out properly. |
|
66218 | 153 |
|
154 |
* Recommended changes to default VSCode settings: |
|
155 |
||
156 |
``` |
|
66223 | 157 |
"editor.acceptSuggestionOnEnter": "off", |
158 |
"editor.lineNumbers": "off", |
|
159 |
"editor.renderIndentGuides": false, |
|
66236 | 160 |
"editor.rulers": [80, 100], |
66223 | 161 |
"editor.wordBasedSuggestions": true, |
66218 | 162 |
``` |
66236 | 163 |
|
66237 | 164 |
## Known Limitations of Isabelle/VSCode |
66236 | 165 |
|
166 |
* Lack of specific support for the `IsabelleText` fonts: these need to be |
|
66237 | 167 |
manually installed on the system and configured for VSCode (see also |
66236 | 168 |
`$ISABELLE_FONTS` within the Isabelle environment). |
169 |
||
66237 | 170 |
**Note:** As the Isabelle fonts continue to evolve, installed versions need |
66236 | 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 |
||
66237 | 178 |
* Lack of formal editor perspective in VSCode: only the cursor position is |
179 |
used (with some surrounding lines of text). |
|
66236 | 180 |
|
181 |
* Lack of formal markup in prover messages and popups. |
|
182 |
||
66237 | 183 |
* Lack of pretty-printing (logical line breaks) according to window and font |
66236 | 184 |
dimensions. |
185 |
||
186 |
* Lack of GUI panels for Sledgehammer, Query operations etc. |
|
66240 | 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). |