Skip to content

Commit fd94b29

Browse files
committed
fix README
1 parent 82ab1be commit fd94b29

File tree

1 file changed

+29
-15
lines changed

1 file changed

+29
-15
lines changed

README.md

Lines changed: 29 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,11 @@ useEffect(() => {
4242
})
4343
```
4444

45+
### Current hacks:
46+
47+
(Currently, this is all necessary for a functioning setup. However, we hope to remove some of these
48+
steps in the future and fix them properly.)
49+
4550
For some reason, the file (here `test.lean`) cannot be at the root of the file system, i.e., not `/test.lean` instead of `/project/test.lean`. (TODO: find out why)
4651

4752
The package uses the Lean 4 VSCode extension, which is intended to run in a nodejs runtime. Therefore, we need to install node polyfills.
@@ -85,21 +90,24 @@ export default {
8590
},
8691
[...]
8792
}
88-
``` "devDependencies": {
89-
"@chialab/esbuild-plugin-meta-url": "^0.18.2",
90-
"@codingame/esbuild-import-meta-url-plugin": "https://gitpkg.vercel.app/abentkamp/monacotest2/esbuild-import-meta-url-plugin?ec9666e",
91-
"@types/node": "^20.14.2",
92-
"@types/semver": "^7.5.8",
93-
"@types/vscode": "^1.89.0",
94-
"copyfiles": "^2.4.1",
95-
"cypress": "^13.13.0",
96-
"cypress-iframe": "^1.0.1",
97-
"ts-loader": "^9.5.1",
98-
"typescript": "^5.4.5",
99-
"wait-on": "^7.2.0",
100-
"webpack": "^5.93.0",
101-
"webpack-cli": "^5.1.4"
102-
},
93+
```
94+
95+
Moreover, the infoview javascript files need to be served. For this install `@leanprover/infoview`:
96+
97+
```
98+
npm install @leanprover/infoview
99+
```
100+
101+
and serve the files by adding the following to `vite.config.ts` :
102+
103+
```ts
104+
// vite.config.ts
105+
import { viteStaticCopy } from 'vite-plugin-static-copy'
106+
import { normalizePath } from 'vite'
107+
import path from 'node:path'
108+
109+
export default {
110+
103111
plugins: [
104112
viteStaticCopy({
105113
targets: [
@@ -109,6 +117,12 @@ export default {
109117
normalizePath(path.resolve(__dirname, './node_modules/lean4monaco/dist/webview/webview.js')),
110118
],
111119
dest: 'infoview'
120+
},
121+
{
122+
src: [
123+
normalizePath(path.resolve(__dirname, './node_modules/@leanprover/infoview/dist/codicon.ttf'))
124+
],
125+
dest: 'assets'
112126
}
113127
]
114128
})

0 commit comments

Comments
 (0)