equal
deleted
inserted
replaced
1 # Isabelle Prover IDE support |
1 # Isabelle Prover IDE support |
2 |
2 |
3 This extension connects VSCode to the Isabelle Prover IDE infrastructure: it |
3 This extension connects VSCode to the Isabelle Prover IDE infrastructure: it |
4 requires a repository version of Isabelle. |
4 requires Isabelle2019. |
5 |
5 |
6 The implementation is centered around the VSCode Language Server protocol, but |
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. |
7 with many add-ons that are specific to VSCode and Isabelle/PIDE. |
8 |
8 |
9 See also: |
9 See also: |
10 |
10 |
11 * <https://isabelle.in.tum.de/repos/isabelle/file/tip/src/Tools/VSCode> |
11 * <https://isabelle.in.tum.de/website-Isabelle2019> |
|
12 * <https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2019/src/Tools/VSCode> |
12 * <https://github.com/Microsoft/language-server-protocol> |
13 * <https://github.com/Microsoft/language-server-protocol> |
13 |
14 |
14 |
15 |
15 ## Screenshot |
16 ## Screenshot |
16 |
17 |
56 |
57 |
57 ## Requirements |
58 ## Requirements |
58 |
59 |
59 ### Isabelle/VSCode Installation |
60 ### Isabelle/VSCode Installation |
60 |
61 |
61 * Download a recent Isabelle development snapshot from <http://isabelle.in.tum.de/devel/release_snapshot> |
62 * Download Isabelle2019 from <https://isabelle.in.tum.de/website-Isabelle2019> |
|
63 or any of its mirror sites. |
62 |
64 |
63 * Unpack and run the main Isabelle/jEdit application as usual, to ensure that |
65 * 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. |
66 the logic image is built properly and Isabelle works as expected. |
65 |
67 |
66 * Download and install VSCode from <https://code.visualstudio.com> |
68 * Download and install VSCode from <https://code.visualstudio.com> |
67 |
69 |
68 * Open the VSCode *Extensions* view and install the following: |
70 * Open the VSCode *Extensions* view and install the following: |
69 |
71 |
70 + *Isabelle*. |
72 + *Isabelle2019* (needs to fit to the underlying Isabelle release). |
71 |
73 |
72 + *Prettify Symbols Mode* (important for display of Isabelle symbols). |
74 + *Prettify Symbols Mode* (important for display of Isabelle symbols). |
73 |
75 |
74 + *bibtexLanguage* (optional): it gives `.bib` a formal status, thus |
76 + *bibtexLanguage* (optional): it gives `.bib` a formal status, thus |
75 `@{cite}` antiquotations become active for completion and hyperlinks. |
77 `@{cite}` antiquotations become active for completion and hyperlinks. |
86 |
88 |
87 Examples: |
89 Examples: |
88 |
90 |
89 + Linux: |
91 + Linux: |
90 ``` |
92 ``` |
91 "isabelle.home": "/home/makarius/Isabelle" |
93 "isabelle.home": "/home/makarius/Isabelle2019" |
92 ``` |
94 ``` |
93 |
95 |
94 + Mac OS X: |
96 + Mac OS X: |
95 ``` |
97 ``` |
96 "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle" |
98 "isabelle.home": "/Users/makarius/Isabelle.app/Isabelle2019" |
97 ``` |
99 ``` |
98 |
100 |
99 + Windows: |
101 + Windows: |
100 ``` |
102 ``` |
101 "isabelle.home": "C:\\Users\\makarius\\Isabelle" |
103 "isabelle.home": "C:\\Users\\makarius\\Isabelle2019" |
102 ``` |
104 ``` |
103 |
105 |
104 * Restart the VSCode application to ensure that all extensions are properly |
106 * Restart the VSCode application to ensure that all extensions are properly |
105 initialized and user settings are updated. Afterwards VSCode should know about |
107 initialized and user settings are updated. Afterwards VSCode should know about |
106 `.thy` files (Isabelle theories) and `.ML` files (Isabelle/ML modules). |
108 `.thy` files (Isabelle theories) and `.ML` files (Isabelle/ML modules). |