Skip to content

Commit c0519ca

Browse files
Geoc2022Geoc2022
committed
Update from template
1 parent e6e5808 commit c0519ca

202 files changed

Lines changed: 39897 additions & 11 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/test.yml‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
name: Test
2+
run-name: Test the project
3+
on:
4+
workflow_dispatch:
5+
push:
6+
branches:
7+
- main
8+
pull_request:
9+
branches:
10+
- main
11+
jobs:
12+
test:
13+
runs-on: ubuntu-latest
14+
steps:
15+
- uses: actions/checkout@v4
16+
- uses: actions/setup-node@v3
17+
- uses: leanprover/lean-action@v1
18+
with:
19+
build: true
20+
test: true
21+
lint: false
22+
use-github-cache: false
23+
use-mathlib-cache: false
24+
check-reservoir-eligibility: false
25+
lake-package-directory: "server"
26+
27+
- run: elan default stable
28+
29+
- name: Build the project
30+
run: |
31+
npm install
32+
npm run build
33+
npm run build:test
34+
35+
- name: Run Cypress tests (Development mode)
36+
run: npm run test
37+
38+
- name: Install Bubblewrap
39+
run: sudo apt-get install bubblewrap
40+
41+
- name: Configure AppArmor for Bubblewrap (https://etbe.coker.com.au/2024/04/24/ubuntu-24-04-bubblewrap/)
42+
run: |
43+
sudo tee /etc/apparmor.d/bwrap > /dev/null << 'EOF'
44+
abi <abi/4.0>,
45+
include <tunables/global>
46+
47+
profile bwrap /usr/bin/bwrap flags=(unconfined) {
48+
userns,
49+
50+
# Site-specific additions and overrides. See local/README for details.
51+
include if exists <local/bwrap>
52+
}
53+
EOF
54+
sudo systemctl reload apparmor
55+
56+
- name: Run Cypress tests (Production mode)
57+
run: npm run test:prod

‎.gitignore‎

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,11 @@
1-
build/
2-
lake-packages/
3-
.lake/
1+
node_modules
2+
client/dist
3+
relay/dist
4+
games/
5+
server/.lake
46
**/.DS_Store
7+
logs/
8+
relay/prev_cpu_metric
9+
test.ecosystem.config.cjs
10+
prod.ecosystem.config.cjs
11+
cypress/screenshots

‎.vscode/ltex.dictionary.en-US.txt‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
GameSkeleton
2+
HiddenTactic
3+
subgoals
4+
KaTex
5+
gameserver
6+
lakefile
7+
Zulip

‎LICENSE‎

Lines changed: 671 additions & 4 deletions
Large diffs are not rendered by default.

‎NOTES.md‎

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
2+
# Install Lean
3+
wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile
4+
5+
# Install NPM
6+
```
7+
curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
8+
source ~/.bashrc
9+
nvm install node npm
10+
11+
npm install -g http-server
12+
```
13+
14+
# Clone NNG interface
15+
16+
```
17+
git clone https://github.com/hhu-adam/NNG4.git
18+
```
19+
20+
21+
22+
# Install PM2
23+
24+
```
25+
sudo npm i -g pm2
26+
27+
pm2 start ecosystem.config.js
28+
pm2 save
29+
pm2 startup
30+
pm2 install pm2-logrotate
31+
32+
```
33+
34+
35+
# Nginx installieren
36+
```
37+
sudo apt update
38+
sudo apt upgrade
39+
sudo apt install nginx nginx-extras
40+
```
41+
42+
Konfigurieren als reverse proxy:
43+
```
44+
sudo unlink /etc/nginx/sites-enabled/default
45+
cd /etc/nginx/sites-available
46+
sudo vim reverse-proxy.conf
47+
```
48+
49+
```
50+
51+
# Anonymize IP addresses
52+
map $remote_addr $remote_addr_anon {
53+
~(?P<ip>\d+\.\d+\.\d+)\. $ip.0;
54+
~(?P<ip>[^:]+:[^:]+): $ip::;
55+
127.0.0.1 $remote_addr;
56+
::1 $remote_addr;
57+
default 0.0.0.0;
58+
}
59+
60+
log_format main '$remote_addr_anon - $remote_user [$time_local] "$request" '
61+
'$status $body_bytes_sent "$http_referer" '
62+
'"$http_user_agent" "$http_x_forwarded_for"';
63+
64+
server {
65+
server_name lean.math.hhu.de;
66+
location / {
67+
proxy_pass http://localhost:8001;
68+
proxy_set_header Host $host;
69+
proxy_set_header X-Real-IP $remote_addr;
70+
proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;
71+
72+
proxy_http_version 1.1;
73+
proxy_set_header Upgrade $http_upgrade;
74+
proxy_set_header Connection "upgrade";
75+
}
76+
client_max_body_size 0;
77+
78+
access_log /var/log/nginx/access.log main;
79+
error_log /dev/null crit;
80+
81+
listen 443 ssl;
82+
ssl_certificate /home/adam/adam_math_hhu_de_cert.cer;
83+
ssl_certificate_key /etc/ssl/private/private.pem;
84+
}
85+
86+
server {
87+
server_name adam.math.hhu.de;
88+
location / {
89+
proxy_pass http://localhost:8002;
90+
proxy_set_header Host $host;
91+
proxy_set_header X-Real-IP $remote_addr;
92+
proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;
93+
proxy_http_version 1.1;
94+
proxy_set_header Upgrade $http_upgrade;
95+
proxy_set_header Connection "upgrade";
96+
97+
}
98+
client_max_body_size 0;
99+
100+
listen 443 ssl;
101+
ssl_certificate /home/adam/adam_math_hhu_de_cert.cer;
102+
ssl_certificate_key /etc/ssl/private/private.pem;
103+
104+
access_log /var/log/nginx/access.log main;
105+
error_log /dev/null crit;
106+
}
107+
108+
server {
109+
server_name adam-dev.math.hhu.de;
110+
location / {
111+
proxy_pass http://localhost:8003;
112+
proxy_set_header Host $host;
113+
proxy_set_header X-Real-IP $remote_addr;
114+
proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;
115+
proxy_http_version 1.1;
116+
proxy_set_header Upgrade $http_upgrade;
117+
proxy_set_header Connection "upgrade";
118+
119+
}
120+
client_max_body_size 0;
121+
122+
listen 443 ssl;
123+
ssl_certificate /home/adam/adam_math_hhu_de_cert.cer;
124+
ssl_certificate_key /etc/ssl/private/private.pem;
125+
126+
access_log /var/log/nginx/access.log main;
127+
error_log /dev/null crit;
128+
}
129+
130+
# Redirect HTTP to HTTPS
131+
server {
132+
listen 80 default_server;
133+
server_name _;
134+
return 301 https://$host$request_uri;
135+
}
136+
```
137+
138+
Activate config:
139+
```
140+
sudo ln -s /etc/nginx/sites-available/reverse-proxy.conf /etc/nginx/sites-enabled/reverse-proxy.conf
141+
sudo nginx -t
142+
sudo nginx -s reload
143+
```
144+
145+
146+
## Install bubblewrap (bwrap)
147+
```
148+
sudo apt-get install bubblewrap
149+
```

‎NOTES_SUBDOMAIN.md‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
## Certificate for multiple subdomains:
2+
3+
Make a copy of the `openssl.cnf` file:
4+
```
5+
cp /etc/ssl/openssl.cnf ~/
6+
```
7+
8+
Edit the file:
9+
```
10+
vim ~/openssl.cnf
11+
```
12+
13+
Uncomment following line in the `[req]` section:
14+
```
15+
req_extensions = v3_req
16+
```
17+
18+
In the `[v3_req]` section, add the following line:
19+
```
20+
subjectAltName = @alt_names
21+
```
22+
23+
Create a new section `[ alt_names ]` at the bottom of the config file. Add SAN or DNS or Alt names like this.
24+
25+
```
26+
[ alt_names ]
27+
DNS.1 = lean.math.uni-duesseldorf.de
28+
```
29+
30+
Note: Do not add the domain name used in the common name field again.
31+
32+
Save and quit.
33+
34+
Create a private key
35+
```
36+
sudo openssl genpkey -algorithm RSA -pkeyopt rsa_keygen_bits:4096 -out /etc/ssl/private/private.pem
37+
```
38+
39+
Generate the CSR:
40+
```
41+
sudo openssl req -new -key /etc/ssl/private/private.pem -out ~/public.csr -config ~/openssl.cnf
42+
```
43+
44+
```
45+
Country Name (2 letter code) [AU]:DE
46+
State or Province Name (full name) [Some-State]:Nordrhein-Westfalen
47+
Locality Name (eg, city) []:Duesseldorf
48+
Organization Name (eg, company) [Internet Widgits Pty Ltd]:Heinrich-Heine-Universitaet Duesseldorf
49+
Organizational Unit Name (eg, section) []:ZIM
50+
Common Name (e.g. server FQDN or YOUR name) []:adam.math.uni-duesseldorf.de // Die Domain, die oben ausgelassen wurde
51+
Email Address []:alexander.bentkamp@hhu.de //(Ihre Mailadresse)
52+
53+
A challenge password []: // leer lassen
54+
An optional company name []: leer lassen
55+
```
56+
57+
Check that the certificate contains the Common Name and all Subject Alternative Names:
58+
```
59+
openssl req -in public.csr -noout -text
60+
```
61+
62+
Then follow the instructions here: https://wiki.hhu.de/display/HHU/Serverzertifikat+beantragen

‎README.md‎

Lines changed: 63 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,65 @@
1-
# Algebra Game
1+
# Lean 4 Game
22

3-
This is a game about basic abstract algebra based on the [Lean4 Game Template](https://github.com/leanprover-community/lean4game/). It is currently a work in progress. You can see the progress on [Issues](https://github.com/Geoc2022/AlgebraGame/issues).
3+
This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
44

5-
Info on how to run this game can be found here:
6-
* [Running a game locally](https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md)
5+
## Creating a Game
6+
7+
Please follow the tutorial [Creating a Game](doc/create_game.md). In particular, the following steps might be of interest:
8+
9+
* Step 6: [How to Run Games Locally](doc/running_locally.md)
10+
* Step 8: [How to Update an existing Game](doc/update_game.md)
11+
* Step 10: [How to Publish a Game](doc/publish_game.md)
12+
* [Troubleshooting](doc/troubleshoot.md)
13+
14+
## Documentation
15+
16+
The documentation is very much work in progress but the linked documentation here
17+
should be up-to-date:
18+
19+
### Game creation API
20+
21+
- [Creating a Game](doc/create_game.md): **the main document to consult**.
22+
- [More about Hints](doc/hints.md): describes the `Hint` and `Branch` tactic.
23+
24+
### Frontend API
25+
26+
* [How to Run Games Locally](doc/running_locally.md): play a game on your computer
27+
* [How to Update an existing Game](doc/update_game.md): update to a new lean version
28+
* [How to Publish a Game](doc/publish_game.md): load your game to adam.math.hhu.de for others to play
29+
30+
### Backend
31+
32+
not fully written yet.
33+
34+
* [Server](doc/DOCUMENTATION.md): describes the server part (i.e. the content of `server/` und `relay/`).
35+
36+
## Contributing
37+
38+
Contributions to `lean4game` are always welcome!
39+
40+
### Translation
41+
42+
The interface can be translated to various languages. For adding a translation, one needs to do the following:
43+
44+
1. In `client/src/config.json`, add your new language. The "iso" key is the ISO language code, i.e. it should be accepted by "i18next" and "GNU gettext"; the "flag" key is once accepted by [react-country-flag](https://www.npmjs.com/package/react-country-flag).
45+
2. Run `npm run translate`. This should create a new file `client/public/locales/{language}/translation.json`. (alternatively you can copy-paste `client/public/locales/en/translation.json`)
46+
3. Add all translations.
47+
4. Commit the changes you made to `config.json` together with the new `translation.json`.
48+
49+
For translating games, see [Translating a game](doc/translate.md).
50+
51+
## Security
52+
53+
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 with bubblewrap.
54+
55+
## Contact
56+
57+
In case of technical problems with ```adam.math.hhu.de``` please contact us via <a href="mailto:matvey.lorkish@hhu.de?subject=Lean4Game: <Your%20Question>">e-mail</a>.
58+
59+
## Credits
60+
61+
The project has primarily been developed by Alexander Bentkamp and Jon Eugster.
62+
63+
It is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
64+
(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
65+
by Kevin Buzzard and Mohammad Pedramfar, and on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).

‎TODO-skipped-commits.txt‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
2+
d3a55a4dd36be3c47fff450fcc759193393eb33b
3+
1431ff8b496a0f1563fb46c9124b2e6bcf50d421
4+
470a184cac47c933b94fe0b84607d596cd9ed45a
5+
af5426856e9233f43a181c35b214918e43ad327c
6+
ded9c3817027ae5a2a71cd928830373cc6b07b66
7+
c5df85ce665c665679fcb3772b2f481047791be6
8+
d82ef8af8f2f474b6f2f6a9dd9181b24095e3a54

0 commit comments

Comments
 (0)