diff --git a/lean4-infoview/package.json b/lean4-infoview/package.json index b2e5e329..77d01961 100644 --- a/lean4-infoview/package.json +++ b/lean4-infoview/package.json @@ -7,7 +7,7 @@ "watchTest": "npm run watch", "build": "rollup --config --environment NODE_ENV:production" }, - "browser": "dist/index", + "browser": "dist/index.production.min.js", "types": "dist/index", "files": [ "dist/*" diff --git a/lean4-infoview/rollup.config.js b/lean4-infoview/rollup.config.js index d1d88bdd..0664b844 100644 --- a/lean4-infoview/rollup.config.js +++ b/lean4-infoview/rollup.config.js @@ -12,6 +12,7 @@ const output = process.env.NODE_ENV && process.env.NODE_ENV === 'production' ? format: 'esm', compact: true, entryFileNames: '[name].production.min.js', + chunkFileNames: '[name]-[hash].production.min.js', plugins: [ terser() ] @@ -19,7 +20,8 @@ const output = process.env.NODE_ENV && process.env.NODE_ENV === 'production' ? dir: 'dist', sourcemap: 'inline', format: 'esm', - entryFileNames: '[name].development.js' + entryFileNames: '[name].development.js', + chunkFileNames: '[name]-[hash].development.js' } export default { diff --git a/vscode-lean4/.vscodeignore b/vscode-lean4/.vscodeignore index 627a7fef..83f13456 100644 --- a/vscode-lean4/.vscodeignore +++ b/vscode-lean4/.vscodeignore @@ -3,7 +3,11 @@ */** ../** -!dist +!dist/extension.js* +!dist/webview.js* +!dist/**/*.production.min.js +!dist/lean4-infoview/index.css +!dist/lean4-infoview/codicon.ttf !media !images !syntaxes diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts index b65f54ab..45a0c971 100644 --- a/vscode-lean4/src/config.ts +++ b/vscode-lean4/src/config.ts @@ -107,3 +107,14 @@ export function getLeanExecutableName(): string { } return 'lean' } + +/** + * The literal 'production' or 'development', depending on the build. + * Should be turned into a string literal by build tools. + */ +export const prodOrDev: string = process.env.NODE_ENV && process.env.NODE_ENV === 'production' + ? 'production' : 'development' + +/** The literal '.min' or empty, depending on the build. See {@link prodOrDev}. */ +export const minIfProd: string = process.env.NODE_ENV && process.env.NODE_ENV === 'production' + ? '.min' : '' diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts index 2d5096cc..8590ded5 100644 --- a/vscode-lean4/src/infoview.ts +++ b/vscode-lean4/src/infoview.ts @@ -8,7 +8,7 @@ import { import { EditorApi, InfoviewApi, LeanFileProgressParams, TextInsertKind, RpcConnectParams, RpcConnected, RpcKeepAliveParams } from '@lean4/infoview-api'; import { LeanClient } from './leanclient'; import { getInfoViewAllErrorsOnLine, getInfoViewAutoOpen, getInfoViewAutoOpenShowGoal, - getInfoViewFilterIndex, getInfoViewStyle, getInfoViewTacticStateFilters } from './config'; + getInfoViewFilterIndex, getInfoViewStyle, getInfoViewTacticStateFilters, minIfProd, prodOrDev } from './config'; import { Rpc } from './rpc'; import { LeanClientProvider } from './utils/clientProvider' import * as ls from 'vscode-languageserver-protocol' @@ -596,6 +596,7 @@ export class InfoProvider implements Disposable { } private initialHtml() { + const libPostfix = `.${prodOrDev}${minIfProd}.js` return ` @@ -611,10 +612,10 @@ export class InfoProvider implements Disposable { diff --git a/vscode-lean4/webpack.config.js b/vscode-lean4/webpack.config.js index af9a1282..d76cb998 100644 --- a/vscode-lean4/webpack.config.js +++ b/vscode-lean4/webpack.config.js @@ -5,7 +5,6 @@ const webpack = require('webpack'); const CopyPlugin = require('copy-webpack-plugin'); const prodOrDev = (env) => env.production ? 'production' : 'development'; -const minIfProd = (env) => env.production ? '.min' : ''; function getWebviewConfig(env) { let webview = { @@ -29,7 +28,7 @@ function getWebviewConfig(env) { resolve: { extensions: ['.tsx', '.ts', '.js'] }, - devtool: !env.production ? 'inline-source-map' : undefined, + devtool: env.production ? undefined : 'inline-source-map', experiments: { outputModule: true }, @@ -53,11 +52,11 @@ function getWebviewConfig(env) { from: path.resolve(__dirname, 'node_modules', '@lean4', 'infoview', 'dist'), to: path.resolve(__dirname, 'dist', 'lean4-infoview') }, { - from: path.resolve(__dirname, 'node_modules', '@esm-bundle', 'react', 'esm', `react.${prodOrDev(env)}${minIfProd(env)}.js`), - to: path.resolve(__dirname, 'dist', 'react.js') + from: path.resolve(__dirname, 'node_modules', '@esm-bundle', 'react', 'esm'), + to: path.resolve(__dirname, 'dist', 'react') }, { - from: path.resolve(__dirname, 'node_modules', '@esm-bundle', 'react-dom', 'esm', `react-dom.${prodOrDev(env)}${minIfProd(env)}.js`), - to: path.resolve(__dirname, 'dist', 'react-dom.js') + from: path.resolve(__dirname, 'node_modules', '@esm-bundle', 'react-dom', 'esm'), + to: path.resolve(__dirname, 'dist', 'react-dom') }] }) ] @@ -69,7 +68,7 @@ function getWebviewConfig(env) { function getExtensionConfig(env) { let config = { name: 'extension', - mode: env.production ? 'production' : 'development', + mode: prodOrDev(env), target: 'node', entry: './src/extension.ts', module: { @@ -87,7 +86,7 @@ function getExtensionConfig(env) { 'node-fetch': path.resolve(__dirname, 'node_modules/node-fetch/lib/index.js'), } }, - devtool: !env.production ? 'source-map' : undefined, + devtool: env.production ? undefined : 'source-map', output: { filename: 'extension.js', path: path.resolve(__dirname, 'dist'),