prototype of new version

.eslintrc.cjs

@@ -0,0 +1,18 @@
+module.exports = {
+  root: true,
+  env: { browser: true, es2020: true },
+  extends: [
+    'eslint:recommended',
+    'plugin:@typescript-eslint/recommended',
+    'plugin:react-hooks/recommended',
+  ],
+  ignorePatterns: ['dist', '.eslintrc.cjs'],
+  parser: '@typescript-eslint/parser',
+  plugins: ['react-refresh'],
+  rules: {
+    'react-refresh/only-export-components': [
+      'warn',
+      { allowConstantExport: true },
+    ],
+  },
+}

.gitignore

@@ -1,7 +1,26 @@
+# Logs
+logs
+*.log
+npm-debug.log*
+yarn-debug.log*
+yarn-error.log*
+pnpm-debug.log*
+lerna-debug.log*
+
 node_modules
-client/dist
-server/build
-client/public/package_versions.json
 dist
-**/.DS_Store
+dist-ssr
+*.local
+
 **/.lake
+
+# Editor directories and files
+.vscode/*
+!.vscode/extensions.json
+.idea
+.DS_Store
+*.suo
+*.ntvs*
+*.njsproj
+*.sln
+*.sw?

.gitmodules

@@ -1,6 +1,3 @@
 [submodule "Projects/lean4web-tools"]
 	path = Projects/lean4web-tools
 	url = https://github.com/hhu-adam/lean4web-tools.git
-[submodule "client/monaco-lean4"]
-	path = client/monaco-lean4
-	url = [email protected]:hhu-adam/monaco-lean4.git

Projects/mathlib-demo/lake-manifest.json

@@ -1,10 +1,11 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "7110da53bf6da84198dba69ca90221c4798ade35",
+   "scope": "leanprover-community",
+   "rev": "ac82ca1064a77eb76d37ae2ab2d1cdeb942d57fe",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +14,8 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "scope": "leanprover-community",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "d68b34fabd37681e6732be752b7e90aaac7aa0e0",
+   "scope": "leanprover-community",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "b167323652ab59a5d1b91e906ca4172d1c0474b7",
+   "scope": "leanprover-community",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +64,8 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "5795dea5a47ba1d4735896548b96dd0bb38cf248",
+   "scope": "",
+   "rev": "df0b4dd7c1ca19a2861ca6ec1bd63851cb6037e9",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -67,7 +74,8 @@
   {"url": "https://github.com/hhu-adam/lean4web-tools.git",
    "type": "git",
    "subDir": null,
-   "rev": "8be7734dfa9a686d3a1329651e2a1a690e1123b6",
+   "scope": "",
+   "rev": "c69970315e29af067b8518995175f6195d4a8f6b",
    "name": "webeditor",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

Projects/mathlib-demo/lakefile.toml

@@ -0,0 +1,15 @@
+name = "mathlibLatest"
+defaultTargets = ["MathlibLatest"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "master"
+
+[[require]]
+name = "webeditor"
+git = "https://github.com/hhu-adam/lean4web-tools.git"
+rev = "main"
+
+[[lean_lib]]
+name = "MathlibLatest"

Projects/mathlib-demo/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc2
+leanprover/lean4:v4.10.0-rc2

README.md

@@ -1,120 +1,30 @@
-# Lean 4 Web
+# React + TypeScript + Vite
 
-This is a web version of Lean 4. The official lean playground is hosted at [live.lean-lang.org](https://live.lean-lang.org), while [lean.math.hhu.de](https://lean.math.hhu.de) hosts a development server testing newer features.
+This template provides a minimal setup to get React working in Vite with HMR and some ESLint rules.
 
+Currently, two official plugins are available:
 
+- [@vitejs/plugin-react](https://github.com/vitejs/vite-plugin-react/blob/main/packages/plugin-react/README.md) uses [Babel](https://babeljs.io/) for Fast Refresh
+- [@vitejs/plugin-react-swc](https://github.com/vitejs/vite-plugin-react-swc) uses [SWC](https://swc.rs/) for Fast Refresh
 
-In contrast to the [Lean 3 web editor](https://github.com/leanprover-community/lean-web-editor), in this web editor, the Lean server is
-running on a web server, and not in the browser.
+## Expanding the ESLint configuration
 
-## Contribution
+If you are developing a production application, we recommend updating the configuration to enable type aware lint rules:
 
-If you experience any problems, or have feature requests, please open an issue here!
-PRs are welcome as well.
+- Configure the top-level `parserOptions` property like this:
 
-To add new themes, please read [Adding Themes](client/public/themes/README.md).
-
-## Security
-Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server
-using [Bubblewrap](https://github.com/containers/bubblewrap).
-
-## Build Instructions
-
-We have set up the project on a Ubuntu Server 22.10.
-Here are the installation instructions:
-
-Install NPM (don't use `apt-get` since it will give you an outdated version of npm):
-```
-curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
-source ~/.bashrc
-nvm install node npm
-```
-
-Now, install `git` and clone this repository:
-```
-sudo apt-get install git
-git clone --recurse-submodules https://github.com/leanprover-community/lean4web.git
-```
-
-note that `--recurse-submodules` is needed to load the predefined projects in `Projects/`. (on an existing clone, you can call `git submodule init` and `git submodule update`)
-
-Install Bubblewrap:
+```js
+export default {
+  // other rules...
+  parserOptions: {
+    ecmaVersion: 'latest',
+    sourceType: 'module',
+    project: ['./tsconfig.json', './tsconfig.node.json', './tsconfig.app.json'],
+    tsconfigRootDir: __dirname,
+  },
+}
 ```
-sudo apt-get install bubblewrap
-```
-
-Navigate into the cloned repository, install, and
-compile:
-```
-cd lean4web
-npm install
-npm run build
-```
-
-Now the server can be started using
-```
-PORT=8080 npm run production
-```
-
-To set the locations of SSL certificates, use the following environment variables:
-```
-SSL_CRT_FILE=/path/to/crt_file.cer SSL_KEY_FILE=/path/to/private_ssl_key.pem PORT=8080 npm run production
-```
-
-### Cronjob
-
-Optionally, you can set up a cronjob to regularly update the mathlib version.
-To do so, run
-```
-crontab -e
-```
-and add the following lines, where all paths must be adjusted appropriately:
-```
-# Need to set PATH manually:
-SHELL=/usr/bin/bash
-PATH=/usr/local/sbin:/usr/local/bin:/sbin:/bin:/usr/sbin:/usr/bin:/home/USER/.elan/bin:/home/USER/.nvm/versions/node/v20.8.0/bin/
-
-# Update server (i.e. mathlib) of lean4web and delete mathlib cache
-*  */6 * * * cd /home/USER/lean4web && npm run build_server 2>&1 1>/dev/null | logger -t lean4web
-40 2   * * * rm -rf /home/USER/.cache/mathlib/
-```
-
-Note that with this setup, you will still have to manage the lean toolchains manually, as they will slowly fill up your space (~0.9GB per new toolchain): see `elan toolchain --help` for infos.
-
-In addition, we use Nginx and pm2 to manage our server.
-
-#### Managing toolchains
-
-Running and updating the server periodically might accumulate lean toolchains.
-
-To delete unused toolchains automatically, you can use the
-[elan-cleanup tool](https://github.com/JLimperg/elan-cleanup) and set up a
-cron-job with `crontab -e` and adding the following line, which runs once a month and
-deletes any unused toolchains:
-
-```
-30 2 1 * * /PATH/TO/elan-cleanup/build/bin/elan-cleanup | logger -t lean-cleanup
-```
-
-You can see installed lean toolchains with `elan toolchain list`
-and check the size of `~/.elan`.
-
-### Legal information
-For legal purposes, we need to display contact details. When setting up your own server,
-you will need to modify the following files:
-
-- `client/src/config/text.tsx`: Update contact information & server location. (set them to `null` if you don't need to display them in your country)
-- `client/public/index.html`: Update the `noscript` page with the correct contact details.
-
-## Development Instructions
-
-Install [npm](https://www.npmjs.com/) and clone this repository. Inside the repository, run:
-
-1. `npm install`, to install dependencies
-2. `npm run build_server`, to build contained lean projects under `Projects/` (or run `lake build` manually inside any lean project)
-3. `npm start`, to start the server.
-
-The project can be accessed via http://localhost:3000. (Internally, websocket requests to `ws://localhost:3000/`websockets will be forwarded to a Lean server running on port 8080.)
 
-## Running different projects
-You can run any lean project through the webeditor by cloning them to the `Projects/` folder. See [Adding Projects](Projects/README.md) for further instructions.
+- Replace `plugin:@typescript-eslint/recommended` to `plugin:@typescript-eslint/recommended-type-checked` or `plugin:@typescript-eslint/strict-type-checked`
+- Optionally add `plugin:@typescript-eslint/stylistic-type-checked`
+- Install [eslint-plugin-react](https://github.com/jsx-eslint/eslint-plugin-react) and add `plugin:react/recommended` & `plugin:react/jsx-runtime` to the `extends` list