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