64757
|
1 |
# Isabelle Prover IDE support
|
|
2 |
|
66236
|
3 |
This extension connects VSCode to the Isabelle Prover IDE infrastructure. It
|
|
4 |
requires a recent development version of Isabelle from 2017 – one that happens
|
|
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:
|
64605
|
11 |
|
66218
|
12 |
* <http://isabelle.in.tum.de/devel/release_snapshot>
|
|
13 |
* <http://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode>
|
64757
|
14 |
|
66230
|
15 |
![[Isabelle/VSCode screenshot]](http://isabelle.in.tum.de/repos/isabelle/raw-file/9fe05edaa351/src/Tools/VSCode/extension/isabelle_vscode.png)
|
66227
|
16 |
|
64605
|
17 |
|
66236
|
18 |
## Notable Features
|
|
19 |
|
|
20 |
* Static syntax tables for Isabelle `.thy` and `.ML` files.
|
|
21 |
|
|
22 |
* Implicit dependency management of sources, subject to changes of theory
|
|
23 |
files within the editor, as well as external file-system events.
|
66218
|
24 |
|
66236
|
25 |
* Implicit formal checking of theory files, using the *cursor position* of the
|
|
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.
|
64757
|
33 |
|
66236
|
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`).
|
64948
|
40 |
|
66236
|
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.
|
64948
|
49 |
|
66227
|
50 |
|
66236
|
51 |
## Requirements
|
|
52 |
|
|
53 |
### Isabelle Installation
|
|
54 |
|
|
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:
|
64873
|
84 |
|
66236
|
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 |
```
|
66218
|
99 |
|
66236
|
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:
|
66218
|
118 |
|
|
119 |
```
|
|
120 |
"prettifySymbolsMode.substitutions": [
|
|
121 |
{
|
|
122 |
"language": "isabelle",
|
|
123 |
"revealOn": "none",
|
|
124 |
"adjustCursorMovement": true,
|
|
125 |
"prettyCursor": "none",
|
|
126 |
"substitutions": []
|
|
127 |
},
|
|
128 |
{
|
|
129 |
"language": "isabelle-ml",
|
|
130 |
"revealOn": "none",
|
|
131 |
"adjustCursorMovement": true,
|
|
132 |
"prettyCursor": "none",
|
|
133 |
"substitutions": []
|
|
134 |
}]
|
|
135 |
```
|
|
136 |
|
66236
|
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.
|
66218
|
139 |
|
66236
|
140 |
|
|
141 |
### Further Preferences
|
66218
|
142 |
|
|
143 |
* Preferred Color Theme: `Light+ (default light)`
|
|
144 |
|
66236
|
145 |
* Alternative Color Theme: `Dark+ (default dark)` – with restrictions: some
|
|
146 |
color combinations don't work out properly.
|
66218
|
147 |
|
|
148 |
* Recommended changes to default VSCode settings:
|
|
149 |
|
|
150 |
```
|
66223
|
151 |
"editor.acceptSuggestionOnEnter": "off",
|
|
152 |
"editor.lineNumbers": "off",
|
|
153 |
"editor.renderIndentGuides": false,
|
66236
|
154 |
"editor.rulers": [80, 100],
|
66223
|
155 |
"editor.wordBasedSuggestions": true,
|
66218
|
156 |
```
|
66236
|
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.
|