From d1d7071abec3c32054024b2753ed1326c2649881 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 24 Jul 2024 11:39:59 +0200 Subject: [PATCH] recover README --- README.md | 132 +++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 111 insertions(+), 21 deletions(-) diff --git a/README.md b/README.md index e1cdc89d..aeca5fbe 100644 --- a/README.md +++ b/README.md @@ -1,30 +1,120 @@ -# React + TypeScript + Vite +# Lean 4 Web -This template provides a minimal setup to get React working in Vite with HMR and some ESLint rules. +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. -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 -## Expanding the ESLint configuration +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. -If you are developing a production application, we recommend updating the configuration to enable type aware lint rules: +## Contribution -- Configure the top-level `parserOptions` property like this: +If you experience any problems, or have feature requests, please open an issue here! +PRs are welcome as well. -```js -export default { - // other rules... - parserOptions: { - ecmaVersion: 'latest', - sourceType: 'module', - project: ['./tsconfig.json', './tsconfig.node.json', './tsconfig.app.json'], - tsconfigRootDir: __dirname, - }, -} +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: ``` +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.) -- 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 +## 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.