Merge remote-tracking branch 'origin/main'

Author: joneugster

.github/workflows/test.yml

@@ -23,5 +23,4 @@ jobs:
           lake --version
       - run: npm install
       - run: npm run build
-      - run: npm run build_server
       - run: npm run test

README.md

@@ -2,8 +2,8 @@
 
 Provides browser support for running Lean in a Monaco editor.
 
-This package is based on the VSCode extension
-[Lean 4](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4) and the
+This package uses the [VSCode extension
+"Lean 4"](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4) and the
 [Lean Infoview](https://www.npmjs.com/package/@leanprover/infoview).
 
 ## Usage
@@ -47,8 +47,10 @@ For some reason, the file (here `test.lean`) cannot be at the root of the file s
 The package uses the Lean 4 VSCode extension, which is intended to run in a nodejs runtime. Therefore, we need to install node polyfills.
 Here is how this can be done if your project uses Vite:
 ```
-npm install vite-plugin-node-polyfills memfs 
+npm install [email protected] --save-exact
+npm install memfs 
 ```
+(We use version 0.17.0 due to this bug: https://github.com/davidmyersdev/vite-plugin-node-polyfills/issues/81)
 
 ```ts
 // vite.config.ts
@@ -97,7 +99,10 @@ export default {
     viteStaticCopy({
       targets: [
         {
-          src: normalizePath(path.resolve(__dirname, './node_modules/@leanprover/infoview/dist/*.production.min.js')),
+          src: [
+            normalizePath(path.resolve(__dirname, './node_modules/@leanprover/infoview/dist/*.production.min.js')),
+            normalizePath(path.resolve(__dirname, './node_modules/lean4monaco/webview/webview.js')),
+          ],
           dest: 'infoview'
         }
       ]
@@ -112,4 +117,4 @@ export default {
 The error I typically got is:
 ```
 this._configurationService.onDidChangeConfiguration is not a function
-```
+```

cypress/e2e/spec.cy.ts

@@ -20,24 +20,19 @@ describe('Editor Test', () => {
       .should(($p) => {
         expect(getComputedStyle($p.get(0)).getPropertyValue('--vscode-editor-background')).to.equal("#ffffff")
       })
-    cy.wait(4000)
     cy.get('[data-cy="theme-dark"]').click()
-    cy.wait(4000)
     cy.contains('#check Nat')
       .should(($p) => {
         expect(getComputedStyle($p.get(0)).getPropertyValue('--vscode-editor-background')).to.equal("#1e1e1e")
       })
   })
   it('inputs unicode', () => {
-
     cy.visit('http://localhost:5173/')
     cy.get('[data-cy="leader-backslash"]').click()
     cy.contains('#check Nat').click("left")
     cy.get('body').type('\\alpha')
     cy.contains('α')
-    cy.wait(4000)
     cy.get('[data-cy="leader-comma"]').click()
-    cy.wait(4000)
     cy.contains('#check Nat').click("left")
     cy.get('body').type(',beta')
     cy.contains('β')