import editor

client/src/components/Level.tsx

@@ -12,6 +12,7 @@ import InputZone from './InputZone';
 import Message from './Message';
 import TacticState from './TacticState';
 import * as rpc from 'vscode-ws-jsonrpc';
+import Editor from 'lean4web/client/src/Editor'
 
 interface LevelProps {
   rpcConnection: null|rpc.MessageConnection;
@@ -103,8 +104,10 @@ function Level({ rpcConnection, nbLevels, level, setCurLevel, setLevelTitle, set
         <LeftPanel spells={tacticDocs} inventory={lemmaDocs} />
       </Grid>
       <Grid xs={4}>
-        <InputZone index={index} history={history} messageOpen={messageOpen} setMessageOpen={setMessageOpen} completed={completed} sendTactic={sendTactic} nbLevels={nbLevels} loadNextLevel={loadNextLevel}
-          errors={errors} lastTactic={lastTactic} undo={undo} finishGame={finishGame} />
+        <Editor setRestart={() => {}}
+          value={""} onDidChangeContent={() => {}}/>
+        {/* <InputZone index={index} history={history} messageOpen={messageOpen} setMessageOpen={setMessageOpen} completed={completed} sendTactic={sendTactic} nbLevels={nbLevels} loadNextLevel={loadNextLevel}
+          errors={errors} lastTactic={lastTactic} undo={undo} finishGame={finishGame} /> */}
         <Message isOpen={messageOpen} content={message} close={closeMessage} />
       </Grid>
       <Grid xs={4}>

package.json

@@ -10,6 +10,8 @@
     "@mui/material": "^5.10.9",
     "better-react-mathjax": "^2.0.2",
     "express": "^4.18.2",
+    "lean4web": "git+https://github.com/hhu-adam/lean4web.git",
+    "path-browserify": "^1.0.1",
     "react": "^18.2.0",
     "react-dom": "^18.2.0",
     "react-markdown": "^8.0.3",

server/leanserver/GameServer/FileWorker.lean

@@ -269,7 +269,7 @@ section Initialization
         if path.fileName != "lakefile.lean" && (← System.FilePath.pathExists lakePath) then
           let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx).toArray hOut
           srcSearchPath ← initSrcSearchPath (← getBuildDir) pkgSearchPath
-      let env ← importModules [{module := `Init}, {module := `Lib}] opts 0
+      let env ← importModules [{module := `Init}] opts 0
       pure (env, msgLog)
     catch e =>  -- should be from `lake print-paths`
       let msgs := MessageLog.empty.add { fileName := "<ignored>", pos := ⟨0, 0⟩, data := e.toString }

tsconfig.json

@@ -1,10 +1,14 @@
 {
   "compilerOptions": {
     "outDir": "./client/dist/",
-    "module": "es6",
+    "module": "esnext",
     "target": "es5",
     "allowJs": true,
+    "resolveJsonModule": true,
+    "esModuleInterop": true,
     "moduleResolution": "node",
     "jsx": "react",
+    "downlevelIteration": true,
+    "experimentalDecorators": true
   }
-}
+}

webpack.config.js

@@ -1,4 +1,5 @@
 const path = require("path");
+const webpack = require('webpack');
 const ReactRefreshWebpackPlugin = require('@pmmmwh/react-refresh-webpack-plugin');
 const WebpackShellPluginNext = require('webpack-shell-plugin-next');
 
@@ -31,8 +32,12 @@ module.exports = env => {
         },
         {
           test: /\.tsx?$/,
-          use: 'ts-loader',
-          exclude: /node_modules/,
+          use: [{
+            loader: 'ts-loader',
+            options: { allowTsInNodeModules: true }
+          }],
+          exclude: /node_modules(?!\/(lean4web|lean4))/,
+          // Allow .ts imports from node_modules/lean4web and node_modules/lean4
         },
         {
           test: /\.css$/,
@@ -40,7 +45,13 @@ module.exports = env => {
         }
       ]
     },
-    resolve: { extensions: ["*", ".js", ".jsx", ".tsx", ".ts"] },
+    resolve: {
+      extensions: ["*", ".js", ".jsx", ".tsx", ".ts"],
+      fallback: {
+        "http": require.resolve("stream-http") ,
+        "path": require.resolve("path-browserify")
+      },
+    },
     output: {
       path: path.resolve(__dirname, "client/dist/"),
       filename: "bundle.js",
@@ -60,14 +71,27 @@ module.exports = env => {
     plugins: [
       !isDevelopment && new WebpackShellPluginNext({
         onBuildEnd:{
-          // It's hard to set up webpack to copy the index.html correctly,
-          // so we copy it explicitly after every build:
-          scripts: ['cp client/public/index.html client/dist/'],
+          scripts: [
+            // It's hard to set up webpack to copy the index.html correctly,
+            // so we copy it explicitly after every build:
+            'cp client/public/index.html client/dist/',
+            // Similarly, I haven't been able to load `onigasm.wasm` properly:
+            'cp client/public/onigasm.wasm client/dist/',],
           blocking: false,
           parallel: true
         }
       }),
-      isDevelopment && new ReactRefreshWebpackPlugin()
+      isDevelopment && new ReactRefreshWebpackPlugin(),
+      new webpack.ContextReplacementPlugin(
+        /\/@leanprover\/infoview\//,
+        (data) => {
+          // Webpack is not happy about the dynamically loaded widget code in the function
+          // `dynamicallyLoadComponent` in `infoview/userWidget.tsx`. If we want to support
+          // dynamically loaded widget code, we need to make sure that the files are available.
+          delete data.dependencies[0].critical;
+          return data;
+        },
+      ),
     ].filter(Boolean),
   };
 }