chore: enable infoview debugging (#732)

This PR ensures that we can set breakpoints in the InfoView again.
Specifically:
- We fix a deadlock in the `watch` task which meant changes in the
infoview would not propagate to the extension build.
- We ensure that all stages use development rather than production
builds of the infoview and the infoview loader.
- We use standalone sourcemap files instead of inline sourcemaps.
- We add a bunch of hacks to make sure both VSCode and Chrome DevTools
have access to these files.
- The terser plugin we use was stripping inline source maps. This PR
ensures that this doesn't happen. (Though we are not using them
anymore.)

Also:
- Bump `es-module-shims` and `rehype-mathjax`. Pin `mathjax-full` to the
latest working version that `rehype-mathjax` is compatible with.

---------

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-authored-by: Wojciech Nawrocki <wjnawrocki@protonmail.com>

Author: 3 people

.vscode/launch.json

@@ -10,7 +10,7 @@
             "args": ["--extensionDevelopmentPath=${workspaceRoot}/vscode-lean4"],
             "stopOnEntry": false,
             "sourceMaps": true,
-            "outFiles": ["${workspaceRoot}/vscode-lean4/dist/**/*.js"],
+            "outFiles": ["${workspaceRoot}/*/dist/**/*.js"],
             "preLaunchTask": "watch",
             "debugWebviews": true,
             "rendererDebugOptions": {

.vscode/tasks.json

@@ -76,7 +76,7 @@
         {
             "label": "build",
             "type": "npm",
-            "script": "build",
+            "script": "build:dev",
             "problemMatcher": {
                 "owner": "typescript",
                 "source": "ts",

lean4-infoview-api/package.json

@@ -9,7 +9,8 @@
     "scripts": {
         "watch": "tsc --watch",
         "watchTest": "tsc --watch",
-        "build": "tsc"
+        "build": "tsc",
+        "build:dev": "tsc"
     },
     "main": "dist/index",
     "types": "dist/index",

lean4-infoview/package.json

@@ -9,17 +9,20 @@
     "scripts": {
         "watch": "rollup --config --environment NODE_ENV:development --watch",
         "build": "rollup --config --environment NODE_ENV:production",
+        "build:dev": "rollup --config --environment NODE_ENV:development",
         "watchTest": "npm run watch",
         "test": "tsc -p test/tsconfig.json"
     },
     "exports": {
         ".": {
-            "default": "./dist/index.production.min.js",
-            "types": "./dist/index.d.ts"
+            "types": "./dist/index.d.ts",
+            "development": "./dist/index.development.js",
+            "default": "./dist/index.production.min.js"
         },
         "./loader": {
-            "default": "./dist/loader.production.min.js",
-            "types": "./dist/loader.d.ts"
+            "types": "./dist/loader.d.ts",
+            "development": "./dist/loader.development.js",
+            "default": "./dist/loader.production.min.js"
         },
         "./package.json": "./package.json"
     },
@@ -30,11 +33,11 @@
     "license": "Apache-2.0",
     "devDependencies": {
         "@floating-ui/react": "^0.26.25",
-        "@rollup/plugin-commonjs": "^28.0.0",
+        "@rollup/plugin-commonjs": "^29.0.2",
         "@rollup/plugin-json": "^6.1.0",
-        "@rollup/plugin-node-resolve": "^15.1.0",
+        "@rollup/plugin-node-resolve": "^16.0.3",
         "@rollup/plugin-replace": "^6.0.1",
-        "@rollup/plugin-terser": "^0.4.4",
+        "@rollup/plugin-terser": "^1.0.0",
         "@rollup/plugin-typescript": "^12.1.0",
         "@rollup/plugin-url": "^8.0.1",
         "@types/react": "^18.2.15",
@@ -47,7 +50,8 @@
         "react-markdown": "^9.0.1",
         "react-syntax-highlighter": "^15.5.0",
         "remark-math": "^6.0.0",
-        "rehype-mathjax": "^6.0.0",
+        "rehype-mathjax": "^7.1.0",
+        "mathjax-full": "~3.2.2",
         "rollup": "^4.24.0",
         "rollup-plugin-css-only": "^4.3.0",
         "typescript": "^5.4.5"
@@ -57,7 +61,7 @@
         "@vscode/codicons": "^0.0.40",
         "@vscode-elements/react-elements": "^0.5.0",
         "es-module-lexer": "^1.5.4",
-        "es-module-shims": "^1.7.3",
+        "es-module-shims": "^2.8.0",
         "react-fast-compare": "^3.2.2",
         "tachyons": "^4.12.0",
         "vscode-languageserver-protocol": "^3.17.3"

lean4-infoview/rollup.config.js

@@ -5,8 +5,34 @@ import replace from '@rollup/plugin-replace'
 import terser from '@rollup/plugin-terser'
 import typescript from '@rollup/plugin-typescript'
 import url from '@rollup/plugin-url'
+import fs from 'fs'
+import path from 'path'
 import css from 'rollup-plugin-css-only'
 
+/**
+ * A minimal Rollup plugin that loads existing source maps for `.js` files.
+ * When Rollup imports an already-compiled `.js` file (e.g. from `lean4-infoview-api/dist`),
+ * it does not read the accompanying `.js.map` by default.
+ * This plugin checks for a sibling `.map` file and, if found,
+ * returns its contents from the `load` hook so that Rollup chains the maps together.
+ * This allows the final bundle's source map to point to the original `.ts` sources
+ * rather than the intermediate `.js` files.
+ *
+ * @returns {import('rollup').Plugin} */
+const inputSourcemaps = () => ({
+    name: 'input-sourcemaps',
+    async load(id) {
+        if (!id.endsWith('.js')) return null
+        try {
+            const code = await fs.promises.readFile(id, 'utf8')
+            const mapJson = await fs.promises.readFile(id + '.map', 'utf8')
+            return { code, map: JSON.parse(mapJson) }
+        } catch {
+            return null
+        }
+    },
+})
+
 /** @type {import('rollup').OutputOptions} */
 const output =
     process.env.NODE_ENV && process.env.NODE_ENV === 'production'
@@ -21,42 +47,61 @@ const output =
           }
         : {
               dir: 'dist',
-              sourcemap: 'inline',
+              sourcemap: true,
+              /* By default, `sourceMappingURL` in the infoview bundle (`dist/index.development.js`)
+               * points to the source map as a relative path.
+               * When we debug the webview,
+               * the infoview bundle is fetched from VSCode's builtin `vscode-resource` server,
+               * and Chrome DevTools tries to fetch the source map that way as well.
+               * This fails,
+               * despite `WebviewOptions.localResourceRoots` supposedly including the entire workspace by default.
+               * Using a `file://` URI instead allows DevTools to fetch the source map,
+               * as well as all the source files it refers to. */
+              sourcemapBaseUrl: 'file://' + path.resolve('dist'),
+              /* Source maps refer to relative paths by default,
+               * but these paths get broken when lean4-infoview/dist is copied into vscode-lean4/dist.
+               * Make them absolute instead. */
+              sourcemapPathTransform: (relativeSourcePath, sourcemapPath) =>
+                  path.resolve(path.dirname(sourcemapPath), relativeSourcePath),
               format: 'esm',
               entryFileNames: '[name].development.js',
               chunkFileNames: '[name]-[hash].development.js',
           }
 
 /** @type {import('rollup').InputPluginOption} */
 const plugins = [
+    inputSourcemaps(),
     url({
         include: ['**/*.ttf'],
         fileName: '[name][extname]',
     }),
     typescript({
         tsconfig: './tsconfig.json',
         outputToFilesystem: false,
-        // https://stackoverflow.com/a/63235210
-        sourceMap: false,
     }),
     nodeResolve({
         browser: true,
     }),
     replace({
         'process.env.NODE_ENV': JSON.stringify(process.env.NODE_ENV),
-        preventAssignment: true, // TODO delete when `true` becomes the default
+        preventAssignment: true,
     }),
     commonjs(),
     json(),
 ]
 
 /**
- * Note that besides building the infoview single-page application, we build a loader and a bunch
- * of esm-shims. This is a way of compiling our dependencies into single-file ES modules which can
- * be shared as imports between the infoview app and dynamically loaded widget modules. Although
- * projects such * as jspm.io do exist, they tend to chunk modules into a bunch of files which are
- * not easy to * bundle, and requiring them dynamically would make the infoview depend on an internet
- * connection. See also `README.md`.
+ * Besides building the infoview single-page application,
+ * we build a loader and a bunch of esm-shims.
+ * This is a way of compiling our runtime dependencies into single-file ES modules
+ * which can be shared as imports between the infoview app and dynamically loaded widget modules.
+ * Due to limitations in Rollup,
+ * we must use an array of configs rather than a single config to do this.
+ * Although projects do exist (e.g. jspm.io)
+ * that could in principle produce the esm-shims for us,
+ * they tend to chunk modules into many files rather than producing a single file.
+ * Requiring them dynamically would make the infoview depend on an internet connection.
+ * See also `README.md`.
  *
  * @type {import('rollup').RollupOptions[]}
  */

lean4-infoview/src/loader.ts

@@ -27,5 +27,5 @@ export function loadRenderInfoview(
     importShim.addImportMap({ imports })
     importShim('@leanprover/infoview')
         .then((mod: any) => next(mod.renderInfoview(...args)))
-        .catch(ex => console.error(`Error importing '@leanprover/infoview': ${JSON.stringify(ex)}`))
+        .catch(ex => console.error(`Error importing '@leanprover/infoview': ${ex}`))
 }

lean4-unicode-input-component/package.json

@@ -9,7 +9,8 @@
     "scripts": {
         "watch": "tsc --watch",
         "watchTest": "tsc --watch",
-        "build": "tsc"
+        "build": "tsc",
+        "build:dev": "tsc"
     },
     "main": "dist/index",
     "types": "dist/index",

lean4-unicode-input/package.json

@@ -9,7 +9,8 @@
     "scripts": {
         "watch": "tsc --watch",
         "watchTest": "tsc --watch",
-        "build": "tsc"
+        "build": "tsc",
+        "build:dev": "tsc"
     },
     "main": "dist/index",
     "types": "dist/index",