You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: README.md
+3-135Lines changed: 3 additions & 135 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -14,140 +14,8 @@ running on a web server, and not in the browser.
14
14
If you experience any problems, or have feature requests, please open an issue here!
15
15
PRs are welcome as well.
16
16
17
-
## Security
18
-
Providing the use access to a Lean instance running on the server is a severe security risk.
19
-
That is why we start the Lean server using [Bubblewrap](https://github.com/containers/bubblewrap).
20
-
21
-
If bubblewrap is not installed, the server will start without a container and produce a warning.
22
-
You can also opt-out of using bubblewrap by setting `NODE_ENV=development`.
23
-
24
17
## Documentation
25
18
26
-
### URL arguments
27
-
28
-
The website parses arguments of the form `https://myserver.com/#arg1=value1&arg2=value2`.
29
-
The recognised arguments are:
30
-
31
-
-`code=`: plain text code.
32
-
*(overwrites `codez`; note this argument does accept unescaped code, but the browser will always display certain characters escaped, like `%20` for a space)*
33
-
-`codez=`: compressed code using [LZ-string](https://www.npmjs.com/package/lz-string).
34
-
-`url=`: a URL where the content is loaded from.
35
-
*(overwrites `code` and `codez`)*.
36
-
-`project=`: the Lean project used by the server to evaluate the code. This has to be the name
37
-
of one of the projects defined in the server's config.
38
-
39
-
The server will automatically only write one of `code`, `codez`, and `url` based on the following
40
-
logic:
41
-
42
-
1. if the code matches the one from the loaded URL, use `url`
43
-
2. if the preferences say no comression, use `code`
44
-
3. otherwise use `codez` or `code` depending on which results in a shorter URL.
45
-
46
-
## Build Instructions
47
-
48
-
We have set up the project on a Ubuntu Server 22.10.
49
-
Here are the installation instructions:
50
-
51
-
Install NPM (don't use `apt-get` since it will give you an outdated version of npm):
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`)
65
-
66
-
Install Bubblewrap:
67
-
```
68
-
sudo apt-get install bubblewrap
69
-
```
70
-
71
-
Navigate into the cloned repository, install, and
72
-
compile:
73
-
```
74
-
cd lean4web
75
-
npm install
76
-
npm run build
77
-
```
78
-
79
-
Now the server can be started using
80
-
```
81
-
PORT=8080 npm run production
82
-
```
83
-
84
-
To set the locations of SSL certificates, use the following environment variables:
85
-
```
86
-
SSL_CRT_FILE=/path/to/crt_file.cer SSL_KEY_FILE=/path/to/private_ssl_key.pem PORT=8080 npm run production
87
-
```
88
-
89
-
### Cronjob
90
-
91
-
Optionally, you can set up a cronjob to regularly update the mathlib version.
92
-
To do so, run
93
-
```
94
-
crontab -e
95
-
```
96
-
and add the following lines, where all paths must be adjusted appropriately:
# Update server (i.e. mathlib) of lean4web and delete mathlib cache
103
-
* */6 * * * cd /home/USER/lean4web && npm run build:server 2>&1 1>/dev/null | logger -t lean4web
104
-
40 2 * * * rm -rf /home/USER/.cache/mathlib/
105
-
```
106
-
107
-
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.
108
-
109
-
In addition, we use Nginx and pm2 to manage our server.
110
-
111
-
#### Managing toolchains
112
-
113
-
Running and updating the server periodically might accumulate Lean toolchains.
114
-
115
-
To delete unused toolchains automatically, you can use the
116
-
[elan-cleanup tool](https://github.com/JLimperg/elan-cleanup) and set up a
117
-
cron-job with `crontab -e` and adding the following line, which runs once a month and
You can see installed lean toolchains with `elan toolchain list`
125
-
and check the size of `~/.elan`.
126
-
127
-
### Legal information
128
-
129
-
Depending on the GDPR and laws applying to your server, you will need to provide the following
130
-
information:
131
-
132
-
-`client/config/config.tsx`, `serverCountry`: where your server is located.
133
-
-`client/config/config.tsx`, `contactDetails`: used in privacy policy & impressum
134
-
-`client/config/config.tsx`, `impressum`: further legal notes
135
-
136
-
if `contactDetails` or `impressum` are not `null`, you will see an item `Impressum` in
137
-
the dropdown menu containing that information.
138
-
139
-
Further, you might need to add the impressum manually to `index.html`
140
-
for people with javascript disabled!
141
-
142
-
## Development Instructions
143
-
144
-
Install [npm](https://www.npmjs.com/) and clone this repository. Inside the repository, run:
145
-
146
-
1.`npm install`, to install dependencies
147
-
2.`npm run build:server`, to build contained lean projects under `Projects/` (or run `lake build` manually inside any lean project)
148
-
3.`npm start`, to start the server.
149
-
150
-
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.)
151
-
152
-
## Running different projects
153
-
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.
19
+
-[User Manual](./doc/Usage.md): Specification of `lean4web` features for the end user.
20
+
-[Installation](./doc/Installation.md): Instructions to install your own instance of `lean4web` on your own server
21
+
-[Development](./doc/Development.md): Instructions to contribute to `lean4web` itself
Install [npm](https://www.npmjs.com/) and clone this repository. Inside the repository, run:
10
+
11
+
1.`npm install`, to install dependencies
12
+
2.`npm run build:server`, to build contained lean projects under `Projects/` (or run `lake build` manually inside any lean project)
13
+
3.`npm start`, to start the server.
14
+
15
+
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.)
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`)
33
+
34
+
Install Bubblewrap:
35
+
```
36
+
sudo apt-get install bubblewrap
37
+
```
38
+
39
+
Navigate into the cloned repository, install, and
40
+
compile:
41
+
```
42
+
cd lean4web
43
+
npm install
44
+
npm run build
45
+
```
46
+
47
+
Now the server can be started using
48
+
```
49
+
PORT=8080 npm run production
50
+
```
51
+
52
+
To set the locations of SSL certificates, use the following environment variables:
53
+
```
54
+
SSL_CRT_FILE=/path/to/crt_file.cer SSL_KEY_FILE=/path/to/private_ssl_key.pem PORT=8080 npm run production
55
+
```
56
+
57
+
### Cronjob
58
+
59
+
Optionally, you can set up a cronjob to regularly update the mathlib version.
60
+
To do so, run
61
+
```
62
+
crontab -e
63
+
```
64
+
and add the following lines, where all paths must be adjusted appropriately:
# Update server (i.e. mathlib) of lean4web and delete mathlib cache
71
+
* */6 * * * cd /home/USER/lean4web && npm run build:server 2>&1 1>/dev/null | logger -t lean4web
72
+
40 2 * * * rm -rf /home/USER/.cache/mathlib/
73
+
```
74
+
75
+
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.
76
+
77
+
In addition, we use Nginx and pm2 to manage our server.
78
+
79
+
#### Managing toolchains
80
+
81
+
Running and updating the server periodically might accumulate Lean toolchains.
82
+
83
+
To delete unused toolchains automatically, you can use the
84
+
[elan-cleanup tool](https://github.com/JLimperg/elan-cleanup) and set up a
85
+
cron-job with `crontab -e` and adding the following line, which runs once a month and
You can see installed lean toolchains with `elan toolchain list`
93
+
and check the size of `~/.elan`.
94
+
95
+
### Legal information
96
+
97
+
Depending on the GDPR and laws applying to your server, you will need to provide the following
98
+
information:
99
+
100
+
-`client/config/config.tsx`, `serverCountry`: where your server is located.
101
+
-`client/config/config.tsx`, `contactDetails`: used in privacy policy & impressum
102
+
-`client/config/config.tsx`, `impressum`: further legal notes
103
+
104
+
if `contactDetails` or `impressum` are not `null`, you will see an item `Impressum` in
105
+
the dropdown menu containing that information.
106
+
107
+
Further, you might need to add the impressum manually to `index.html`
108
+
for people with javascript disabled!
109
+
110
+
### Running different projects
111
+
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.
The website parses arguments of the form `https://myserver.com/#arg1=value1&arg2=value2`.
11
+
The recognised arguments are:
12
+
13
+
-`code=`: plain text code.
14
+
*(overwrites `codez`; note this argument does accept unescaped code, but the browser will always display certain characters escaped, like `%20` for a space)*
15
+
-`codez=`: compressed code using [LZ-string](https://www.npmjs.com/package/lz-string).
16
+
-`url=`: a URL where the content is loaded from.
17
+
*(overwrites `code` and `codez`)*.
18
+
-`project=`: the Lean project used by the server to evaluate the code. This has to be the name
19
+
of one of the projects defined in the server's config.
20
+
21
+
The server will automatically only write one of `code`, `codez`, and `url` based on the following
22
+
logic:
23
+
24
+
1. if the code matches the one from the loaded URL, use `url`
25
+
2. if the preferences say no comression, use `code`
26
+
3. otherwise use `codez` or `code` depending on which results in a shorter URL.
0 commit comments