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