chore: dispatch to prod/dev build

leanprover · Mar 18, 2022 · a60fe31 · a60fe31
1 parent 214ad2f
commit a60fe31
Show file tree

Hide file tree

Showing 6 changed files with 33 additions and 16 deletions.
diff --git 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
@@ -12,14 +12,16 @@ 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()
         ]
     } : {
         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
@@ -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
@@ -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
@@ -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 `
             <!DOCTYPE html>
             <html>
@@ -611,10 +612,10 @@ export class InfoProvider implements Disposable {
                 <script type="importmap">
                     {
                         "imports": {
-                            "@lean4/infoview": "${this.getLocalPath('dist/lean4-infoview/index.js')}",
-                            "react": "${this.getLocalPath('dist/react.js')}",
-                            "react-dom": "${this.getLocalPath('dist/react-dom.js')}",
-                            "react-popper": "${this.getLocalPath('dist/lean4-infoview/react-popper.js')}"
+                            "@lean4/infoview": "${this.getLocalPath(`dist/lean4-infoview/index${libPostfix}`)}",
+                            "react": "${this.getLocalPath(`dist/react/react${libPostfix}`)}",
+                            "react-dom": "${this.getLocalPath(`dist/react-dom/react-dom${libPostfix}`)}",
+                            "react-popper": "${this.getLocalPath(`dist/lean4-infoview/react-popper${libPostfix}`)}"
                         }
                     }
                 </script>

diff --git 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'),