chore: separate package.json for client and server (#94)

* bump lean4monaco

* npm audit fix

* separate client and server

* fix eslint

* fix tests

* fix tsc build

* add windows test

* fix test setup

Author: joneugster

Projects/MathlibDemo/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "63710499c7ac0bd4ab1977494d82e3017ac59edf",
+   "rev": "55aa437fb40b168305405301f173cf0cb2adfe94",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
+   "rev": "e84e3e16aea6b72cc5d311ca1bb25caad417e162",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890",
+   "rev": "f207d9fcf0cef00ba79962a33ef156061914d9c7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
+   "rev": "2e58165a9dcdca9837b666528f974299ee1a51cc",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.84",
+   "inputRev": "v0.0.92",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c",
+   "rev": "c3361708f266893de5d1769192b60d4b1831f2bb",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72",
+   "rev": "221e8088e3a066b8676dc471ff10638cf1c10835",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2e16f91af2a97975e5d2fac906494cd6c17ba255",
+   "rev": "87f6314ff2cc922489cd73cd0fbc2252f39aa153",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
+   "rev": "3de531c1135f5e3a01f3ac04830996fda476b28e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": "v4.29.0-rc6",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "MathlibDemo",

Projects/MathlibDemo/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.27.0-rc1
+leanprover/lean4:v4.29.0-rc6

index.html client/index.htmlindex.html renamed to client/index.html

@@ -20,6 +20,6 @@
         <!-- </p> -->
       </noscript>
     </div>
-    <script type="module" src="client/src/index.tsx"></script>
+    <script type="module" src="src/index.tsx"></script>
   </body>
 </html>

client/package.json

@@ -0,0 +1,43 @@
+{
+  "name": "leanweb-client",
+  "private": true,
+  "type": "module",
+  "scripts": {
+    "dev": "NODE_ENV=development vite --host",
+    "build": "tsc -b && NODE_ENV=production vite build"
+  },
+  "dependencies": {
+    "@emotion/react": "^11.14.0",
+    "@emotion/styled": "^11.14.1",
+    "@fortawesome/free-solid-svg-icons": "^7.1.0",
+    "@fortawesome/react-fontawesome": "^3.1.1",
+    "@mui/material": "^7.3.5",
+    "@tailwindcss/vite": "^4.1.18",
+    "@tanstack/query-core": "^5.90.14",
+    "@uiw/react-codemirror": "^4.25.3",
+    "file-saver": "^2.0.5",
+    "jotai-location": "^0.6.2",
+    "jotai-react": "^0.0.0",
+    "jotai-tanstack-query": "^0.11.0",
+    "jotai": "^2.16.1",
+    "lean4monaco": "^1.1.8",
+    "lz-string": "^1.5.0",
+    "react-dom": "^19.2.0",
+    "react-split": "^2.0.14",
+    "react": "^19.2.0",
+    "tailwindcss": "^4.1.18",
+    "vscode-ws-jsonrpc": "^3.5.0"
+  },
+  "devDependencies": {
+    "@codingame/esbuild-import-meta-url-plugin": "^1.0.3",
+    "@types/file-saver": "^2.0.7",
+    "@types/react-dom": "^19.2.3",
+    "@types/react": "^19.2.7",
+    "@vitejs/plugin-react-swc": "^4.2.2",
+    "typescript": "^5.9.3",
+    "vite-plugin-node-polyfills": "0.24.0",
+    "vite-plugin-static-copy": "^3.1.4",
+    "vite-plugin-svgr": "^4.5.0",
+    "vite": "^7.2.4"
+  }
+}

tsconfig.json client/tsconfig.jsontsconfig.json renamed to client/tsconfig.json

@@ -1,6 +1,6 @@
 {
   "compilerOptions": {
-    "outDir": "./client/dist/",
+    "outDir": "dist",
     "target": "ES2023",
     "useDefineForClassFields": true,
     "lib": ["ES2023", "DOM", "DOM.Iterable"],
@@ -24,6 +24,6 @@
     /* Performance */
     "skipLibCheck": true
   },
-  "include": ["client/src", "eslint.config.js"],
-  "exclude": ["server", "node_modules"]
+  "include": ["src"],
+  "exclude": ["node_modules"]
 }

vite.config.ts client/vite.config.tsvite.config.ts renamed to client/vite.config.ts

@@ -1,5 +1,3 @@
-import path from "node:path";
-
 import importMetaUrlPlugin from "@codingame/esbuild-import-meta-url-plugin";
 import tailwindcss from "@tailwindcss/vite";
 import react from "@vitejs/plugin-react-swc";
@@ -16,12 +14,11 @@ export default defineConfig({
       // @ts-ignore           // TODO
       plugins: [importMetaUrlPlugin],
     },
-    exclude: ["Projects"],
+    // exclude: ["Projects"],
   },
   build: {
-    // Relative to the root
     // Note: This has to match the path in `server/index.mjs` and in `tsconfig.json`
-    outDir: "client/dist",
+    outDir: "dist",
   },
   plugins: [
     react(),
@@ -44,36 +41,19 @@ export default defineConfig({
       targets: [
         {
           src: [
-            normalizePath(
-              path.resolve(
-                __dirname,
-                "./node_modules/@leanprover/infoview/dist/*",
-              ),
-            ),
-            normalizePath(
-              path.resolve(
-                __dirname,
-                "./node_modules/lean4monaco/dist/webview/webview.js",
-              ),
-            ),
+            "../node_modules/@leanprover/infoview/dist/*",
+            "../node_modules/lean4monaco/dist/webview/webview.js",
           ],
           dest: "infoview",
         },
         {
-          src: [
-            normalizePath(
-              path.resolve(
-                __dirname,
-                "./node_modules/@leanprover/infoview/dist/codicon.ttf",
-              ),
-            ),
-          ],
+          src: ["../node_modules/@leanprover/infoview/dist/codicon.ttf"],
           dest: "assets",
         },
       ],
     }),
   ],
-  publicDir: "client/public/",
+  publicDir: "public",
   base: "/", // setting this to `/leanweb/` means the server is now accessible at `localhost:3000/leanweb`
   server: {
     port: 3000,
@@ -91,8 +71,6 @@ export default defineConfig({
     },
   },
   resolve: {
-    alias: {
-      path: "path-browserify",
-    },
+    alias: {},
   },
 });

cypress.config.ts

@@ -16,4 +16,5 @@ export default defineConfig({
       });
     },
   },
+  allowCypressEnv: false,
 });

eslint.config.js eslint.config.mjseslint.config.js renamed to eslint.config.mjs

@@ -14,7 +14,7 @@ export default [
     ignores: ["dist", "node_modules"],
   },
   {
-    files: ["client/src/**/*.{ts,tsx}"],
+    files: ["client/src/**/*.{ts,tsx}", "server/**/*.{ts,tsx,mjs,cjs,js}"],
     ...js.configs.recommended,
     languageOptions: {
       parser: tsParser,
@@ -52,8 +52,13 @@ export default [
       ],
       "simple-import-sort/imports": "warn",
       "simple-import-sort/exports": "warn",
-
-      "@typescript-eslint/no-unused-vars": "off",
+      "@typescript-eslint/no-unused-vars": [
+        "warn",
+        {
+          varsIgnorePattern: "^_",
+          argsIgnorePattern: "^_",
+        },
+      ],
     },
   },