Compare commits
334 Commits
mobile-opt
...
main
| Author | SHA1 | Date |
|---|---|---|
|
|
61ed224788 | 1 year ago |
|
|
39137f6d0b | 1 year ago |
|
|
cd5870347b | 1 year ago |
|
|
50bf73a0c5 | 1 year ago |
|
|
39d7af9d3e | 1 year ago |
|
|
49062cc3d5 | 1 year ago |
|
|
f75389e93f | 1 year ago |
|
|
92665b7521 | 1 year ago |
|
|
1845644e86 | 1 year ago |
|
|
341a9ae14b | 1 year ago |
|
|
0895821baa | 1 year ago |
|
|
5b0715629a | 1 year ago |
|
|
39e08194f6 | 1 year ago |
|
|
451dc262b2 | 1 year ago |
|
|
52898d93e7 | 2 years ago |
|
|
5f30572741 | 2 years ago |
|
|
76f2414bd5 | 2 years ago |
|
|
f1f9325c54 | 2 years ago |
|
|
bd3375ada7 | 2 years ago |
|
|
64f34acd7a | 2 years ago |
|
|
ae38ad977a | 2 years ago |
|
|
a191c47b8e | 2 years ago |
|
|
0e58e81875 | 2 years ago |
|
|
f0aa6b58ed | 2 years ago |
|
|
045b1ea3fb | 2 years ago |
|
|
dc6f7b2822 | 2 years ago |
|
|
db5ac7ed15 | 2 years ago |
|
|
6a0e739301 | 2 years ago |
|
|
ed96cf9534 | 2 years ago |
|
|
64670d1579 | 2 years ago |
|
|
25141b9613 | 2 years ago |
|
|
ab9d0d0679 | 2 years ago |
|
|
6dca770dbf | 2 years ago |
|
|
2022fa9a44 | 2 years ago |
|
|
b77afebe0a | 2 years ago |
|
|
4ac38ef7dd | 2 years ago |
|
|
6a8abf41bd | 2 years ago |
|
|
1466a41169 | 2 years ago |
|
|
3cdb9a026b | 2 years ago |
|
|
ebd7268421 | 2 years ago |
|
|
af15982804 | 2 years ago |
|
|
5a404a9a58 | 2 years ago |
|
|
cebea6a6aa | 2 years ago |
|
|
36499c0257 | 2 years ago |
|
|
8c5e47dd7b | 2 years ago |
|
|
a46840d327 | 2 years ago |
|
|
f518efc81c | 2 years ago |
|
|
9b93e3817d | 2 years ago |
|
|
54c1e0dcaf | 2 years ago |
|
|
2c1e69611b | 2 years ago |
|
|
2c22c445b1 | 2 years ago |
|
|
b6b31a06ac | 2 years ago |
|
|
255839fea7 | 2 years ago |
|
|
b961030db2 | 2 years ago |
|
|
c20d807d5c | 2 years ago |
|
|
23c8099401 | 2 years ago |
|
|
6bd9e95db9 | 2 years ago |
|
|
1febc51791 | 2 years ago |
|
|
d53b57a764 | 2 years ago |
|
|
020b4f7803 | 2 years ago |
|
|
0ae099414c | 2 years ago |
|
|
b091ec579b | 2 years ago |
|
|
2a14f48f45 | 2 years ago |
|
|
4ed0753bb0 | 2 years ago |
|
|
6b5fc80896 | 2 years ago |
|
|
e56c7a0670 | 2 years ago |
|
|
5b710da197 | 2 years ago |
|
|
b275bbb94f | 2 years ago |
|
|
29eb90e6c8 | 2 years ago |
|
|
4e9ac54cde | 2 years ago |
|
|
18f21fa324 | 2 years ago |
|
|
d034148bec | 2 years ago |
|
|
feaf6dae0c | 2 years ago |
|
|
6059ff1da7 | 2 years ago |
|
|
6f95f41d14 | 2 years ago |
|
|
335209b094 | 2 years ago |
|
|
de1ff4fadc | 2 years ago |
|
|
db66cb1fcc | 2 years ago |
|
|
66aa8e688e | 2 years ago |
|
|
a523bab1d6 | 2 years ago |
|
|
499bb00d4f | 2 years ago |
|
|
67b03d9ccf | 2 years ago |
|
|
a15dd0a1bd | 2 years ago |
|
|
d456621875 | 2 years ago |
|
|
74059bd5af | 2 years ago |
|
|
ce71bc81c6 | 2 years ago |
|
|
7cedfc5038 | 2 years ago |
|
|
a8d3169ebb | 2 years ago |
|
|
9b05a27888 | 2 years ago |
|
|
3124d90cd6 | 2 years ago |
|
|
5a768c25b7 | 2 years ago |
|
|
39be34e83a | 2 years ago |
|
|
dd7a2d1bc1 | 2 years ago |
|
|
684a1bc72b | 2 years ago |
|
|
10391b616c | 2 years ago |
|
|
aaa6c3b576 | 2 years ago |
|
|
d60dc3fcb2 | 2 years ago |
|
|
1a54edffd4 | 2 years ago |
|
|
ad1add5264 | 2 years ago |
|
|
a26022e3fc | 2 years ago |
|
|
7c44d49b2a | 2 years ago |
|
|
a111814973 | 2 years ago |
|
|
a7784ef66b | 2 years ago |
|
|
389e120117 | 2 years ago |
|
|
ee9fd18a56 | 2 years ago |
|
|
8b29f88407 | 2 years ago |
|
|
ebda6cc162 | 2 years ago |
|
|
7e9514fe96 | 2 years ago |
|
|
038dbe71b8 | 2 years ago |
|
|
19d2ea363a | 2 years ago |
|
|
3ac8fdace7 | 2 years ago |
|
|
8d0493acb5 | 2 years ago |
|
|
27c661f08f | 2 years ago |
|
|
b37f050da5 | 2 years ago |
|
|
09c81ea43f | 2 years ago |
|
|
ff12b34295 | 2 years ago |
|
|
45bc0468df | 2 years ago |
|
|
c24efb1377 | 2 years ago |
|
|
830bffaf11 | 2 years ago |
|
|
a9447a70d4 | 2 years ago |
|
|
eaa4eecad2 | 2 years ago |
|
|
1828e73b30 | 2 years ago |
|
|
ce9f5c7840 | 2 years ago |
|
|
64d7879c32 | 2 years ago |
|
|
cb711205a2 | 2 years ago |
|
|
f42829422d | 2 years ago |
|
|
ee6741232f | 2 years ago |
|
|
fa4ae5672d | 2 years ago |
|
|
9bc0a3de46 | 2 years ago |
|
|
6cdbfbd9cb | 2 years ago |
|
|
f55581a5f2 | 2 years ago |
|
|
381930e547 | 2 years ago |
|
|
e07570181c | 2 years ago |
|
|
87689e1c3a | 2 years ago |
|
|
47297e4194 | 2 years ago |
|
|
f3f077741d | 2 years ago |
|
|
edf1085310 | 2 years ago |
|
|
68f84a3426 | 2 years ago |
|
|
217f86ce5e | 2 years ago |
|
|
dd60093dfc | 2 years ago |
|
|
85347a54d9 | 2 years ago |
|
|
3b4afd6e0e | 2 years ago |
|
|
2c12872a6e | 2 years ago |
|
|
ad819bf7ff | 2 years ago |
|
|
c0f366abba | 2 years ago |
|
|
f72ebdf050 | 2 years ago |
|
|
af8463ca5d | 2 years ago |
|
|
d0a444205a | 2 years ago |
|
|
1796c76a84 | 2 years ago |
|
|
a75a4a81ac | 2 years ago |
|
|
45d84103c1 | 2 years ago |
|
|
92e9ed38b2 | 2 years ago |
|
|
d689c7ec86 | 2 years ago |
|
|
16c979a6c2 | 2 years ago |
|
|
2b85386373 | 2 years ago |
|
|
8008b68fd6 | 2 years ago |
|
|
2649f985fa | 2 years ago |
|
|
698a88c545 | 2 years ago |
|
|
3775ad98c8 | 2 years ago |
|
|
780514e45a | 2 years ago |
|
|
19f2ceface | 2 years ago |
|
|
800d1f3308 | 2 years ago |
|
|
c0acde14e2 | 2 years ago |
|
|
976d1c6901 | 2 years ago |
|
|
5bb6c559bc | 2 years ago |
|
|
11ee6c1535 | 2 years ago |
|
|
3998fb2fc9 | 2 years ago |
|
|
538f74004c | 2 years ago |
|
|
6aebb8993f | 2 years ago |
|
|
6472ef5b31 | 2 years ago |
|
|
72ffab5b46 | 2 years ago |
|
|
3b660c5185 | 2 years ago |
|
|
ebb8c98145 | 2 years ago |
|
|
4abf05b77e | 2 years ago |
|
|
df423aaace | 2 years ago |
|
|
a67dcb306f | 2 years ago |
|
|
37582e04d4 | 2 years ago |
|
|
9d4a6df139 | 2 years ago |
|
|
26202e5f36 | 2 years ago |
|
|
ed017fa605 | 2 years ago |
|
|
36bc52c960 | 2 years ago |
|
|
e085f2f106 | 2 years ago |
|
|
e975c455fe | 2 years ago |
|
|
c006be5a9f | 2 years ago |
|
|
49379a0930 | 2 years ago |
|
|
03076b0161 | 2 years ago |
|
|
bfb60ffedd | 2 years ago |
|
|
ca576542ba | 2 years ago |
|
|
fd5e507541 | 2 years ago |
|
|
c103eeacfa | 2 years ago |
|
|
e277a48749 | 2 years ago |
|
|
16ff701518 | 2 years ago |
|
|
20ca385e14 | 2 years ago |
|
|
5a38543e3b | 2 years ago |
|
|
a4a6f2e725 | 2 years ago |
|
|
cc89e78e4c | 2 years ago |
|
|
c533a635c2 | 2 years ago |
|
|
ab98eaa3ba | 2 years ago |
|
|
7114a8c4cb | 2 years ago |
|
|
b7eb15184d | 2 years ago |
|
|
892c70165a | 2 years ago |
|
|
8929813e48 | 2 years ago |
|
|
5d88cd6739 | 2 years ago |
|
|
d16956da9b | 2 years ago |
|
|
e15e5af126 | 2 years ago |
|
|
8c93b3c5b3 | 2 years ago |
|
|
cd1d212a3c | 2 years ago |
|
|
406c2799b1 | 3 years ago |
|
|
e579071a3b | 3 years ago |
|
|
8cdac88b5a | 3 years ago |
|
|
7882958f54 | 3 years ago |
|
|
c9f97b3285 | 3 years ago |
|
|
614b762b6c | 3 years ago |
|
|
c4f4dbdc6b | 3 years ago |
|
|
5a78118bb6 | 3 years ago |
|
|
a6775d5495 | 3 years ago |
|
|
03a370464b | 3 years ago |
|
|
eaa214ec37 | 3 years ago |
|
|
d7f1f70d41 | 3 years ago |
|
|
2d0f69d337 | 3 years ago |
|
|
1ab50710f5 | 3 years ago |
|
|
e76e287763 | 3 years ago |
|
|
5fd49abb90 | 3 years ago |
|
|
4b7d540a80 | 3 years ago |
|
|
aec196deff | 3 years ago |
|
|
ae636a03ed | 3 years ago |
|
|
deec431620 | 3 years ago |
|
|
5aa0764844 | 3 years ago |
|
|
93c55dc9f7 | 3 years ago |
|
|
aab7441323 | 3 years ago |
|
|
2ba36b91d5 | 3 years ago |
|
|
a2726ae287 | 3 years ago |
|
|
8c39fb6664 | 3 years ago |
|
|
5f52e23f29 | 3 years ago |
|
|
b067dea6e7 | 3 years ago |
|
|
4edf67f0d6 | 3 years ago |
|
|
004f81835f | 3 years ago |
|
|
527f58e3a4 | 3 years ago |
|
|
b239a5d3dc | 3 years ago |
|
|
63cf5e8b72 | 3 years ago |
|
|
25f166f57f | 3 years ago |
|
|
c89e2e4020 | 3 years ago |
|
|
f6738faf46 | 3 years ago |
|
|
cb7224934c | 3 years ago |
|
|
13d54ff0ff | 3 years ago |
|
|
72e4011c62 | 3 years ago |
|
|
4f5256fa88 | 3 years ago |
|
|
c2b9175fe5 | 3 years ago |
|
|
a1a6862b5a | 3 years ago |
|
|
0a057913be | 3 years ago |
|
|
bedb2ad5ec | 3 years ago |
|
|
e02e73c1c0 | 3 years ago |
|
|
c82a88867f | 3 years ago |
|
|
8b43aed596 | 3 years ago |
|
|
8c84d3fae7 | 3 years ago |
|
|
d5697d052e | 3 years ago |
|
|
0e652256f8 | 3 years ago |
|
|
9492c1011a | 3 years ago |
|
|
54bab2a016 | 3 years ago |
|
|
3f8b180b04 | 3 years ago |
|
|
23b1074aa2 | 3 years ago |
|
|
0964a06f2f | 3 years ago |
|
|
b17c8fc4cb | 3 years ago |
|
|
0c4ae92856 | 3 years ago |
|
|
088711b5d1 | 3 years ago |
|
|
4c93b3a091 | 3 years ago |
|
|
aa00e359c4 | 3 years ago |
|
|
f6a2632d80 | 3 years ago |
|
|
f2190d648f | 3 years ago |
|
|
d7fd8709cb | 3 years ago |
|
|
7a03c4fe0d | 3 years ago |
|
|
333c9498f1 | 3 years ago |
|
|
121b36b542 | 3 years ago |
|
|
6bced7575b | 3 years ago |
|
|
d18b48db2f | 3 years ago |
|
|
97dc648452 | 3 years ago |
|
|
472e2c66df | 3 years ago |
|
|
622e9d3897 | 3 years ago |
|
|
7f91ae7da8 | 3 years ago |
|
|
28a7c65db2 | 3 years ago |
|
|
56525c6234 | 3 years ago |
|
|
44f7b6703e | 3 years ago |
|
|
8851cd8b1f | 3 years ago |
|
|
bae360874c | 3 years ago |
|
|
07b6525c58 | 3 years ago |
|
|
8e8026aa38 | 3 years ago |
|
|
a3a421f504 | 3 years ago |
|
|
084e25c0dc | 3 years ago |
|
|
6580afb622 | 3 years ago |
|
|
0c0a7ab400 | 3 years ago |
|
|
dfb2f10219 | 3 years ago |
|
|
a57a5af111 | 3 years ago |
|
|
946a7fa673 | 3 years ago |
|
|
244c373192 | 3 years ago |
|
|
374afa318a | 3 years ago |
|
|
d0636b1d85 | 3 years ago |
|
|
2e121363b3 | 3 years ago |
|
|
590d68ccfb | 3 years ago |
|
|
f6727e5c9f | 3 years ago |
|
|
241ef4b67a | 3 years ago |
|
|
ea4250f38d | 3 years ago |
|
|
1d2420331d | 3 years ago |
|
|
2213862998 | 3 years ago |
|
|
81073b24b8 | 3 years ago |
|
|
33068f1183 | 3 years ago |
|
|
8ab37d4344 | 3 years ago |
|
|
9d9902cce1 | 3 years ago |
|
|
f53316c591 | 3 years ago |
|
|
427ce43e95 | 3 years ago |
|
|
15d79244d4 | 3 years ago |
|
|
f13027f75c | 3 years ago |
|
|
5fcdee4f71 | 3 years ago |
|
|
7ad23dab24 | 3 years ago |
|
|
89e19cc019 | 3 years ago |
|
|
4db5260ed8 | 3 years ago |
|
|
d19046aebd | 3 years ago |
|
|
6e0fcb1d50 | 3 years ago |
|
|
04c70ba522 | 3 years ago |
|
|
1b3993ad3e | 3 years ago |
|
|
45a95bbdc4 | 3 years ago |
|
|
7c9f3d7a0a | 3 years ago |
|
|
823000d5d4 | 3 years ago |
|
|
c706b66af1 | 3 years ago |
|
|
933394bb6f | 3 years ago |
|
|
e09c016c4c | 3 years ago |
|
|
06d9656e88 | 3 years ago |
|
|
b30164dec4 | 3 years ago |
|
|
ea685f0b19 | 3 years ago |
|
|
d71b895550 | 3 years ago |
|
|
21070af13c | 3 years ago |
|
|
2b9f791655 | 3 years ago |
|
|
51ca5354dc | 3 years ago |
|
|
ebcde9d588 | 3 years ago |
|
|
335e7e6883 | 3 years ago |
@ -0,0 +1,8 @@
|
|||||||
|
node_modules
|
||||||
|
client/dist
|
||||||
|
games/
|
||||||
|
server/.lake
|
||||||
|
**/.DS_Store
|
||||||
|
logs/
|
||||||
|
relay/prev_cpu_metric
|
||||||
|
test.ecosystem.config.cjs
|
||||||
@ -1,11 +1,23 @@
|
|||||||
name: Build
|
name: Build
|
||||||
run-name: Build the project
|
run-name: Build the project
|
||||||
on: [push]
|
on:
|
||||||
|
workflow_dispatch:
|
||||||
|
push:
|
||||||
jobs:
|
jobs:
|
||||||
build:
|
build:
|
||||||
runs-on: ubuntu-latest
|
runs-on: ubuntu-latest
|
||||||
steps:
|
steps:
|
||||||
- uses: actions/checkout@v3
|
- name: install elan
|
||||||
|
run: |
|
||||||
|
set -o pipefail
|
||||||
|
curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
|
||||||
|
./elan-init -y
|
||||||
|
echo "$HOME/.elan/bin" >> $GITHUB_PATH
|
||||||
|
- uses: actions/checkout@v4
|
||||||
- uses: actions/setup-node@v3
|
- uses: actions/setup-node@v3
|
||||||
|
- name: print lean and lake versions
|
||||||
|
run: |
|
||||||
|
lean --version
|
||||||
|
lake --version
|
||||||
- run: npm install
|
- run: npm install
|
||||||
- run: npm run build
|
- run: npm run build
|
||||||
|
|||||||
@ -1,6 +1,8 @@
|
|||||||
node_modules
|
node_modules
|
||||||
client/dist
|
client/dist
|
||||||
server/build
|
games/
|
||||||
server/lakefile.olean
|
server/.lake
|
||||||
**/lake-packages/
|
|
||||||
**/.DS_Store
|
**/.DS_Store
|
||||||
|
logs/
|
||||||
|
relay/prev_cpu_metric
|
||||||
|
test.ecosystem.config.cjs
|
||||||
|
|||||||
@ -0,0 +1,7 @@
|
|||||||
|
GameSkeleton
|
||||||
|
HiddenTactic
|
||||||
|
subgoals
|
||||||
|
KaTex
|
||||||
|
gameserver
|
||||||
|
lakefile
|
||||||
|
Zulip
|
||||||
@ -0,0 +1,29 @@
|
|||||||
|
FROM node:23-bookworm
|
||||||
|
|
||||||
|
RUN apt update && apt upgrade -y
|
||||||
|
RUN apt install -y bubblewrap
|
||||||
|
|
||||||
|
WORKDIR /app
|
||||||
|
|
||||||
|
# Install elan
|
||||||
|
RUN curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz && \
|
||||||
|
./elan-init -y
|
||||||
|
|
||||||
|
ENV PATH="/root/.elan/bin:${PATH}"
|
||||||
|
|
||||||
|
# Copy package files
|
||||||
|
COPY package.json package-lock.json ./
|
||||||
|
|
||||||
|
# Install dependencies
|
||||||
|
RUN npm install
|
||||||
|
|
||||||
|
# Copy project files
|
||||||
|
COPY . .
|
||||||
|
|
||||||
|
# Build the project
|
||||||
|
RUN npm run build
|
||||||
|
|
||||||
|
EXPOSE 8080
|
||||||
|
|
||||||
|
# Set the entrypoint
|
||||||
|
CMD ["npm", "run", "production"]
|
||||||
@ -1,36 +1,93 @@
|
|||||||
# Lean 4 Game
|
# lean4game fork
|
||||||
|
|
||||||
This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
|
Questo è un fork di **lean4game** con supporto per essere self-hostato con Docker.
|
||||||
|
|
||||||
The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
|
## Deployment con Docker Compose
|
||||||
(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
|
|
||||||
of Kevin Buzzard and Mohammad Pedramfar.
|
|
||||||
The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
|
|
||||||
|
|
||||||
## Creating a Game
|
Dopo aver clonato questa repo, per prima cosa serve creare [un token di API per GitHub](https://github.com/settings/developers) per permettere a lean4game di importare da solo i vari "game". Possiamo mettere questo token ed il nostro nome utente in un file `.env` come segue
|
||||||
|
|
||||||
|
```
|
||||||
|
export LEAN4GAME_GITHUB_USER='...'
|
||||||
|
export LEAN4GAME_GITHUB_TOKEN='...'
|
||||||
|
```
|
||||||
|
|
||||||
|
poi per lanciare tutto con docker compose basta eseguire
|
||||||
|
|
||||||
|
```bash
|
||||||
|
$ source .env
|
||||||
|
$ docker compose up -d
|
||||||
|
```
|
||||||
|
|
||||||
|
Questo comando lancierà lean4game su `http://locahost:8080`.
|
||||||
|
|
||||||
|
### Aggiungere Giochi
|
||||||
|
|
||||||
|
Per scaricare nuovi giochi basta fare una chiamata al seguente url
|
||||||
|
|
||||||
|
- `https://{host}/import/trigger/{org}/{repo}`
|
||||||
|
|
||||||
|
Ad esempio per scaricare <https://github.com/leanprover-community/nng4> basta andare all'indirizzo `https://{host}/import/trigger/leanprover-community/nng4` per aggiungere _Natural Number Game_.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
# Lean 4 Game
|
||||||
|
|
||||||
Please follow the tutorial [Creating a Game](doc/create_game.md).
|
This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
|
||||||
In particular step 5 thereof explains [How to Run Games Locally](doc/running_locally.md).
|
|
||||||
|
|
||||||
### Publishing a Game
|
## Creating a Game
|
||||||
|
|
||||||
We encourage anybody to have games hosted on our [Lean Game Server](https://adam.math.hhu.de) for anybody to play. For that you simply need to contact us with the link to your game repo. We are also happy to add work-in-progress games and games in any language.
|
Please follow the tutorial [Creating a Game](doc/create_game.md). In particular, the following steps might be of interest:
|
||||||
|
|
||||||
For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).
|
* Step 5: [How to Run Games Locally](doc/running_locally.md)
|
||||||
|
* Step 7: [How to Update an existing Game](doc/update_game.md)
|
||||||
|
* Step 9: [How to Publishing a Game](doc/publish_game.md)
|
||||||
|
* [Troubleshooting](doc/troubleshoot.md)
|
||||||
|
|
||||||
## Documentation
|
## Documentation
|
||||||
|
|
||||||
The documentation for the game engine itself is still missing, but there is [Creating a Game](doc/create_game.md) explaining the API to create a game.
|
The documentation is very much work in progress but the linked documentation here
|
||||||
|
should be up-to-date:
|
||||||
|
|
||||||
|
### Game creation API
|
||||||
|
|
||||||
|
- [Creating a Game](doc/create_game.md): **the main document to consult**.
|
||||||
|
- [More about Hints](doc/hints.md): describes the `Hint` and `Branch` tactic.
|
||||||
|
|
||||||
|
### Frontend API
|
||||||
|
|
||||||
Some documentation:
|
* [How to Run Games Locally](doc/running_locally.md): play a game on your computer
|
||||||
|
* [How to Update an existing Game](doc/update_game.md): update to a new lean version
|
||||||
|
* [How to Publishing a Game](doc/publish_game.md): load your game to adam.math.hhu.de for others to play
|
||||||
|
|
||||||
- [NPM Scripts](doc/npm_scripts.md)
|
### Backend
|
||||||
- [Old documentation](doc/DOCUMENTATION.md)
|
|
||||||
|
not fully written yet.
|
||||||
|
|
||||||
|
* [Server](doc/DOCUMENTATION.md): describes the server part (i.e. the content of `server/` und `relay/`).
|
||||||
|
|
||||||
## Contributing
|
## Contributing
|
||||||
|
|
||||||
Contributions to `lean4game` are always welcome!
|
Contributions to `lean4game` are always welcome!
|
||||||
|
|
||||||
|
### Translation
|
||||||
|
|
||||||
|
The interface can be translated to various languages. For adding a translation, one needs to do the following:
|
||||||
|
|
||||||
|
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).
|
||||||
|
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`)
|
||||||
|
3. Add all translations.
|
||||||
|
4. Commit the changes you made to `config.json` together with the new `translation.json`.
|
||||||
|
|
||||||
|
For translating games, see [Translating a game](doc/translate.md).
|
||||||
|
|
||||||
## Security
|
## 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 with bubblewrap.
|
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.
|
||||||
|
|
||||||
|
## Credits
|
||||||
|
|
||||||
|
The project has primarily been developed by Alexander Bentkamp and Jon Eugster.
|
||||||
|
|
||||||
|
It is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
|
||||||
|
(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
|
||||||
|
by Kevin Buzzard and Mohammad Pedramfar, and on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
|
||||||
|
|||||||
@ -0,0 +1,152 @@
|
|||||||
|
const lean4gameConfig = require("./src/config.json")
|
||||||
|
|
||||||
|
const typescriptTransform = require('i18next-scanner-typescript');
|
||||||
|
|
||||||
|
const fs = require('fs');
|
||||||
|
const chalk = require('chalk');
|
||||||
|
const eol = require('eol');
|
||||||
|
const path = require('path');
|
||||||
|
const VirtualFile = require('vinyl');
|
||||||
|
|
||||||
|
function flush(done) {
|
||||||
|
const { parser } = this;
|
||||||
|
const { options } = parser;
|
||||||
|
|
||||||
|
// Flush to resource store
|
||||||
|
const resStore = parser.get({ sort: options.sort });
|
||||||
|
const { jsonIndent } = options.resource;
|
||||||
|
const lineEnding = String(options.resource.lineEnding).toLowerCase();
|
||||||
|
|
||||||
|
Object.keys(resStore).forEach((lng) => {
|
||||||
|
const namespaces = resStore[lng];
|
||||||
|
|
||||||
|
Object.keys(namespaces).forEach((ns) => {
|
||||||
|
const resPath = parser.formatResourceSavePath(lng, ns);
|
||||||
|
let resContent;
|
||||||
|
try {
|
||||||
|
resContent = JSON.parse(
|
||||||
|
fs.readFileSync(
|
||||||
|
fs.realpathSync(path.join('public', 'locales', resPath))
|
||||||
|
).toString('utf-8')
|
||||||
|
);
|
||||||
|
} catch (e) {
|
||||||
|
console.log("no previous translation found!")
|
||||||
|
resContent = {};
|
||||||
|
}
|
||||||
|
const obj = { ...namespaces[ns], ...resContent };
|
||||||
|
let text = JSON.stringify(obj, null, jsonIndent) + '\n';
|
||||||
|
|
||||||
|
if (lineEnding === 'auto') {
|
||||||
|
text = eol.auto(text);
|
||||||
|
} else if (lineEnding === '\r\n' || lineEnding === 'crlf') {
|
||||||
|
text = eol.crlf(text);
|
||||||
|
} else if (lineEnding === '\n' || lineEnding === 'lf') {
|
||||||
|
text = eol.lf(text);
|
||||||
|
} else if (lineEnding === '\r' || lineEnding === 'cr') {
|
||||||
|
text = eol.cr(text);
|
||||||
|
} else { // Defaults to LF
|
||||||
|
text = eol.lf(text);
|
||||||
|
}
|
||||||
|
|
||||||
|
let contents = null;
|
||||||
|
|
||||||
|
try {
|
||||||
|
// "Buffer.from(string[, encoding])" is added in Node.js v5.10.0
|
||||||
|
contents = Buffer.from(text);
|
||||||
|
} catch (e) {
|
||||||
|
// Fallback to "new Buffer(string[, encoding])" which is deprecated since Node.js v6.0.0
|
||||||
|
contents = new Buffer(text);
|
||||||
|
}
|
||||||
|
|
||||||
|
this.push(new VirtualFile({
|
||||||
|
path: resPath,
|
||||||
|
contents: contents
|
||||||
|
}));
|
||||||
|
});
|
||||||
|
});
|
||||||
|
|
||||||
|
done();
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
module.exports = {
|
||||||
|
input: [
|
||||||
|
'client/src/**/*.{tsx,ts}',
|
||||||
|
// Use ! to filter out files or directories
|
||||||
|
'!client/i18n/**',
|
||||||
|
'!**/node_modules/**',
|
||||||
|
],
|
||||||
|
options: {
|
||||||
|
debug: true,
|
||||||
|
removeUnusedKeys: true,
|
||||||
|
func: {
|
||||||
|
list: ['i18next.t', 'i18n.t', 't'],
|
||||||
|
extensions: ['.js', '.jsx'] // not .ts or .tsx since we use i18next-scanner-typescript!
|
||||||
|
},
|
||||||
|
trans: {
|
||||||
|
component: 'Trans',
|
||||||
|
i18nKey: 'i18nKey',
|
||||||
|
defaultsKey: 'defaults',
|
||||||
|
extensions: ['.js', '.jsx'], // not .ts or .tsx since we use i18next-scanner-typescript!
|
||||||
|
fallbackKey: (ns, value) => {return value},
|
||||||
|
|
||||||
|
// https://react.i18next.com/latest/trans-component#usage-with-simple-html-elements-like-less-than-br-greater-than-and-others-v10.4.0
|
||||||
|
supportBasicHtmlNodes: true, // Enables keeping the name of simple nodes (e.g. <br/>) in translations instead of indexed keys.
|
||||||
|
keepBasicHtmlNodesFor: ['br', 'strong', 'i', 'p'], // Which nodes are allowed to be kept in translations during defaultValue generation of <Trans>.
|
||||||
|
|
||||||
|
// // https://github.com/acornjs/acorn/tree/master/acorn#interface
|
||||||
|
// acorn: {
|
||||||
|
// ecmaVersion: 2020,
|
||||||
|
// sourceType: 'module', // defaults to 'module'
|
||||||
|
// }
|
||||||
|
},
|
||||||
|
lngs: lean4gameConfig.languages.map(e => e.iso),
|
||||||
|
ns: [],
|
||||||
|
defaultLng: 'en',
|
||||||
|
defaultNs: 'translation',
|
||||||
|
defaultValue: (lng, ns, key) => {
|
||||||
|
if (lng === 'en') {
|
||||||
|
return key; // Use key as value for base language
|
||||||
|
}
|
||||||
|
return ''; // Return empty string for other languages
|
||||||
|
},
|
||||||
|
resource: {
|
||||||
|
loadPath: './client/public/locales/{{lng}}/{{ns}}.json',
|
||||||
|
savePath: './client/public/locales/{{lng}}/{{ns}}.json',
|
||||||
|
jsonIndent: 2,
|
||||||
|
lineEnding: '\n'
|
||||||
|
},
|
||||||
|
nsSeparator: false, // namespace separator
|
||||||
|
keySeparator: false, // key separator
|
||||||
|
plurals: false,
|
||||||
|
interpolation: {
|
||||||
|
prefix: '{{',
|
||||||
|
suffix: '}}'
|
||||||
|
},
|
||||||
|
metadata: {},
|
||||||
|
allowDynamicKeys: false,
|
||||||
|
},
|
||||||
|
|
||||||
|
transform: typescriptTransform(
|
||||||
|
// options
|
||||||
|
{
|
||||||
|
// default value for extensions
|
||||||
|
extensions: [".ts", ".tsx"],
|
||||||
|
// optional ts configuration
|
||||||
|
tsOptions: {
|
||||||
|
target: "es2017",
|
||||||
|
},
|
||||||
|
},
|
||||||
|
|
||||||
|
function(outputText, file, enc, done) {
|
||||||
|
'use strict';
|
||||||
|
const parser = this.parser;
|
||||||
|
|
||||||
|
parser.parseTransFromString(outputText);
|
||||||
|
parser.parseFuncFromString(outputText);
|
||||||
|
|
||||||
|
done();
|
||||||
|
}
|
||||||
|
),
|
||||||
|
|
||||||
|
};
|
||||||
@ -0,0 +1,99 @@
|
|||||||
|
{
|
||||||
|
"Tactics": "Taktiken",
|
||||||
|
"Lean Game Server": "Lean-Lern-Spiel-Server",
|
||||||
|
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>Die Spielregeln bestimmen ob es erlaubt ist, Levels zu überspringen und ob das Spiel überprüft welche Taktiken und Theoreme freigeschaltet sind und nur diese im Beweis akzeptiert.</p><1>Bemerkung: \"Freigeschaltete\" Taktiken (und Theoreme) werden durch zwei Faktoren bestimmt: The Menge der Taktiken die minimal notwending sind um den Level zu lösen und dazu die Menge aller Taktiken, die in einem anderen Level freigeschaltet wurden. Das bedeutet wenn <1>simp</1> in einem Level freigeschaltet wird, kann diese Taktik danach in jeglichen Levels verwendet werden.",
|
||||||
|
"Game Rules": "Spielregeln",
|
||||||
|
"levels": "Level",
|
||||||
|
"tactics": "Taktiken",
|
||||||
|
"regular": "regulär",
|
||||||
|
"relaxed": "relaxed",
|
||||||
|
"none": "keine",
|
||||||
|
"Rules": "Regeln",
|
||||||
|
"Intro": "Prolog",
|
||||||
|
"Game Introduction": "Prolog",
|
||||||
|
"World selection": "Übersicht",
|
||||||
|
"Start": "Start",
|
||||||
|
"Inventory": "Inventar",
|
||||||
|
"next level": "nächstes Level",
|
||||||
|
"Next": "Weiter",
|
||||||
|
"back to world selection": "Zurück zur Übersicht",
|
||||||
|
"Leave World": "Welt verlassen",
|
||||||
|
"previous level": "voheriges Level",
|
||||||
|
"Previous": "Zurück",
|
||||||
|
"Editor mode is enforced!": "Editor kann nicht verlassen werden!",
|
||||||
|
"Editor mode": "Editor",
|
||||||
|
"Typewriter mode": "Schreibmaschine",
|
||||||
|
"information, Impressum, privacy policy": "Informationen, Impressum, Privacy Policy",
|
||||||
|
"Preferences": "Einstellungen",
|
||||||
|
"Game Info & Credits": "Spielinfo & Credits",
|
||||||
|
"Game Info": "Spielinfo",
|
||||||
|
"Clear Progress": "Spielstand löschen",
|
||||||
|
"Erase": "Löschen",
|
||||||
|
"Download Progress": "Spielstand herunterladen",
|
||||||
|
"Download": "Herunterladen",
|
||||||
|
"Load Progress from JSON": "Spielstand aus JSON laden",
|
||||||
|
"Upload": "Laden",
|
||||||
|
"Home": "Home",
|
||||||
|
"back to games selection": "Zurück zur Spielauswahl",
|
||||||
|
"close inventory": "Inventar schließen",
|
||||||
|
"show inventory": "Inventar öffnen",
|
||||||
|
"World": "Welt",
|
||||||
|
"Show more help!": "Mehr Hilfe",
|
||||||
|
"Goal": "Beweisziel",
|
||||||
|
"Current Goal": "Aktuelles Beweisziel",
|
||||||
|
"Objects": "Objekte",
|
||||||
|
"Assumptions": "Annahmen",
|
||||||
|
"Further Goals": "Weitere Ziele",
|
||||||
|
"No Goals": "Keine Beweisziele",
|
||||||
|
"Loading goal…": "Beweisziel wird geladen…",
|
||||||
|
"Click somewhere in the Lean file to enable the infoview.": "Ein Klick in den Lean-Code aktiviert den Infoview.",
|
||||||
|
"Waiting for Lean server to start…": "Warte auf den Lean-Server …",
|
||||||
|
"Level completed! 🎉": "Level gelöst! 🎉",
|
||||||
|
"Level completed with warnings 🎭": "Level mit Warnungen abgeschlossen 🎭",
|
||||||
|
"Active Goal": "Aktuelles Ziel",
|
||||||
|
"Crashed! Go to editor mode and fix your proof! Last server response:": "Abgestürzt! Wechsle in den Editor-Modus, um deinen Beweis zu repariaeren. Letzte Meldung vom Server:",
|
||||||
|
"Line": "Zeile",
|
||||||
|
"Character": "Charakter",
|
||||||
|
"Loading messages…": "Lade Meldungen …",
|
||||||
|
"Execute": "Ausführen",
|
||||||
|
"Definitions": "Definitionen",
|
||||||
|
"Theorems": "Theoreme",
|
||||||
|
"Not unlocked yet": "Noch nicht verfügbar",
|
||||||
|
"Not available in this level": "In diesem Level nicht verfügbar",
|
||||||
|
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Eine Sammlung von Lernspielen für den Beweisassistenten <1>Lean</1> <i>(Lean 4)</i> und dessen mathematische Bibliothek <5>mathlib</5>",
|
||||||
|
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "Kein Spiel geladen. Öffne <1>http://localhost:3000/#/g/local/FOLDER</1> um ein Spiel direkt aus einem lokalen Ordner zu laden.",
|
||||||
|
"Prerequisites": "Voraussetzungen",
|
||||||
|
"Worlds": "Welten",
|
||||||
|
"Levels": "Level",
|
||||||
|
"Language": "Sprache",
|
||||||
|
"Development notes": "Entwicklungsstand",
|
||||||
|
"Adding new games": "Neue Spiele hinzufügen",
|
||||||
|
"Funding": "Finanzierung",
|
||||||
|
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>Soll der Spielstand unwiderruflich gelöscht werden?</p><p>(Dies löscht sämtliche Beweise und das gesammelte Inventar. Spielstände anderer Spiele werden nicht gelöscht.)</p>",
|
||||||
|
"Delete Progress?": "Spielstand löschen?",
|
||||||
|
"Delete": "Löschen",
|
||||||
|
"Download & Delete": "Herunterladen & löschen",
|
||||||
|
"Cancel": "Abbrechen",
|
||||||
|
"Layout": "Seitenlayout",
|
||||||
|
"Always visible": "Immer sichtbar",
|
||||||
|
"Save my settings (in the browser store)": "Einstellungen im Browser speichern.",
|
||||||
|
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>Wähle eine JSON-Datei mit einem Spielstand, um diesen zu laden.</p><1><0>Achtung:</0> Deraktuelle Spielstand wird dabei überschrieben! Wenn du noch einmal zum aktuellen Spielstand zurückkehren möchtest, solltest du zunächst den <2>aktuellen Spielstand herunterladen</2>!</1>",
|
||||||
|
"Upload Saved Progress": "Spielstand hochladen",
|
||||||
|
"Load selected file": "Ausgewählte Datei hochladen",
|
||||||
|
"Mobile": "Mobil",
|
||||||
|
"Auto": "Auto",
|
||||||
|
"Desktop": "Desktop",
|
||||||
|
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>Für alle, die selbst Spiel entwickeln möchten, gibt es ein <1>GameSkeleton Github Repo</1> als Vorlage und die Anleitung <3>How to Create a Game</3>.</0><1>Die <1>Anleitung</1> erklärt auch, wie ein solches Spiel mittels einer passenden URL auf den Sever geladen und gespiel werden kann. Fragen dazu beantworten wir gern.</1><p>Als Kacheln sichtbar ist auf dieser Seite nur eine kuratierte Auswahl an existierenden Spielen. Wir erweitern diese Auswahl auf Anfrage sehr gerne.</p>",
|
||||||
|
"Level": "Level",
|
||||||
|
"Introduction": "Prolog",
|
||||||
|
"Retry proof from here": "Ab hier neu ansetzen",
|
||||||
|
"Retry": "Noch einmal",
|
||||||
|
"Failed command": "Gescheiterter Befehl",
|
||||||
|
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "Diese Server läuft auf universitäter Infrastruktur mit begrenzten Kapazitäten. Wir schätzen, dass die Belastungsgrenze bei rund 70 gleichzeitig laufenden Spielen besteht.",
|
||||||
|
"<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "Der Spieleserver und die alle Spiele befinden sich in fortlaufender Entwicklung. Wir bitten darum, Fehler und Ungereimtheiten als <1>GitHub Issue</1> zu melden.",
|
||||||
|
"This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "Die Lean-Spiele-Software und dieser Spiele-Server werden als Teils der Projekts <1>ADAM: Anticipating the Digital Age of Mathematics</1> an der Heinrich-Heine-Universität Düsseldorf entwickelt.",
|
||||||
|
"Server capacity": "Server-Auslastung",
|
||||||
|
"RAM": "RAM",
|
||||||
|
" used": "",
|
||||||
|
"CPU": "CPU"
|
||||||
|
}
|
||||||
@ -0,0 +1,99 @@
|
|||||||
|
{
|
||||||
|
"Tactics": "Tactics",
|
||||||
|
"Lean Game Server": "Lean Game Server",
|
||||||
|
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>",
|
||||||
|
"Game Rules": "Game Rules",
|
||||||
|
"levels": "levels",
|
||||||
|
"tactics": "tactics",
|
||||||
|
"regular": "regular",
|
||||||
|
"relaxed": "relaxed",
|
||||||
|
"none": "none",
|
||||||
|
"Rules": "Rules",
|
||||||
|
"Intro": "Intro",
|
||||||
|
"Game Introduction": "Game Introduction",
|
||||||
|
"World selection": "World selection",
|
||||||
|
"Start": "Start",
|
||||||
|
"Inventory": "Inventory",
|
||||||
|
"next level": "next level",
|
||||||
|
"Next": "Next",
|
||||||
|
"back to world selection": "back to world selection",
|
||||||
|
"Leave World": "Leave World",
|
||||||
|
"previous level": "previous level",
|
||||||
|
"Previous": "Previous",
|
||||||
|
"Editor mode is enforced!": "Editor mode is enforced!",
|
||||||
|
"Editor mode": "Editor mode",
|
||||||
|
"Typewriter mode": "Typewriter mode",
|
||||||
|
"information, Impressum, privacy policy": "information, Impressum, privacy policy",
|
||||||
|
"Preferences": "Preferences",
|
||||||
|
"Game Info & Credits": "Game Info & Credits",
|
||||||
|
"Game Info": "Game Info",
|
||||||
|
"Clear Progress": "Clear Progress",
|
||||||
|
"Erase": "Erase",
|
||||||
|
"Download Progress": "Download Progress",
|
||||||
|
"Download": "Download",
|
||||||
|
"Load Progress from JSON": "Load Progress from JSON",
|
||||||
|
"Upload": "Upload",
|
||||||
|
"Home": "Home",
|
||||||
|
"back to games selection": "back to games selection",
|
||||||
|
"close inventory": "close inventory",
|
||||||
|
"show inventory": "show inventory",
|
||||||
|
"World": "World",
|
||||||
|
"Show more help!": "Show more help!",
|
||||||
|
"Goal": "Goal",
|
||||||
|
"Current Goal": "Current Goal",
|
||||||
|
"Objects": "Objects",
|
||||||
|
"Assumptions": "Assumptions",
|
||||||
|
"Further Goals": "Further Goals",
|
||||||
|
"No Goals": "No Goals",
|
||||||
|
"Loading goal…": "Loading goal…",
|
||||||
|
"Click somewhere in the Lean file to enable the infoview.": "Click somewhere in the Lean file to enable the infoview.",
|
||||||
|
"Waiting for Lean server to start…": "Waiting for Lean server to start…",
|
||||||
|
"Level completed! 🎉": "Level completed! 🎉",
|
||||||
|
"Level completed with warnings 🎭": "Level completed with warnings 🎭",
|
||||||
|
"Active Goal": "Active Goal",
|
||||||
|
"Crashed! Go to editor mode and fix your proof! Last server response:": "Crashed! Go to editor mode and fix your proof! Last server response:",
|
||||||
|
"Line": "Line",
|
||||||
|
"Character": "Character",
|
||||||
|
"Loading messages…": "Loading messages…",
|
||||||
|
"Execute": "Execute",
|
||||||
|
"Definitions": "Definitions",
|
||||||
|
"Theorems": "Theorems",
|
||||||
|
"Not unlocked yet": "Not unlocked yet",
|
||||||
|
"Not available in this level": "Not available in this level",
|
||||||
|
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>",
|
||||||
|
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.",
|
||||||
|
"Prerequisites": "Prerequisites",
|
||||||
|
"Worlds": "Worlds",
|
||||||
|
"Levels": "Levels",
|
||||||
|
"Language": "Language",
|
||||||
|
"Server capacity": "Server capacity",
|
||||||
|
"RAM": "RAM",
|
||||||
|
"CPU": "CPU",
|
||||||
|
"Development notes": "Development notes",
|
||||||
|
"Adding new games": "Adding new games",
|
||||||
|
"Funding": "Funding",
|
||||||
|
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>",
|
||||||
|
"Delete Progress?": "Delete Progress?",
|
||||||
|
"Delete": "Delete",
|
||||||
|
"Download & Delete": "Download & Delete",
|
||||||
|
"Cancel": "Cancel",
|
||||||
|
"Layout": "Layout",
|
||||||
|
"Always visible": "Always visible",
|
||||||
|
"Save my settings (in the browser store)": "Save my settings (in the browser store)",
|
||||||
|
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>",
|
||||||
|
"Upload Saved Progress": "Upload Saved Progress",
|
||||||
|
"Load selected file": "Load selected file",
|
||||||
|
"Mobile": "Mobile",
|
||||||
|
"Auto": "Auto",
|
||||||
|
"Desktop": "Desktop",
|
||||||
|
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>",
|
||||||
|
"Level": "Level",
|
||||||
|
"Introduction": "Introduction",
|
||||||
|
"Retry proof from here": "Retry proof from here",
|
||||||
|
"Retry": "Retry",
|
||||||
|
"Failed command": "Failed command",
|
||||||
|
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>",
|
||||||
|
"<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>",
|
||||||
|
"This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.",
|
||||||
|
" used": " used"
|
||||||
|
}
|
||||||
@ -0,0 +1,99 @@
|
|||||||
|
{
|
||||||
|
"Intro": "Introducción",
|
||||||
|
"Game Introduction": "Introducción del juego",
|
||||||
|
"World selection": "Seleccionar mundo",
|
||||||
|
"Start": "Empezar",
|
||||||
|
"Inventory": "Inventario",
|
||||||
|
"next level": "siguiente nivel",
|
||||||
|
"Next": "Siguiente",
|
||||||
|
"back to world selection": "volver a la selección de mundos",
|
||||||
|
"Leave World": "Abandonar mundo",
|
||||||
|
"previous level": "nivel anterior",
|
||||||
|
"Previous": "Anterior",
|
||||||
|
"Editor mode is enforced!": "¡El modo editor es obligatorio!",
|
||||||
|
"Editor mode": "Modo editor",
|
||||||
|
"Typewriter mode": "Modo línea a línea",
|
||||||
|
"information, Impressum, privacy policy": "información, Impressum, política de privacidad",
|
||||||
|
"Preferences": "Preferencias",
|
||||||
|
"Game Info & Credits": "Información del juego y reconocimientos",
|
||||||
|
"Game Info": "Información del juego",
|
||||||
|
"Clear Progress": "Limpiar el progreso",
|
||||||
|
"Erase": "Borrar",
|
||||||
|
"Download Progress": "Descargar progreso",
|
||||||
|
"Download": "Descargar",
|
||||||
|
"Load Progress from JSON": "Cargar progreso desde JSON",
|
||||||
|
"Upload": "Subir",
|
||||||
|
"Home": "Inicio",
|
||||||
|
"back to games selection": "volver a la selección de juegos",
|
||||||
|
"close inventory": "cerrar inventario",
|
||||||
|
"show inventory": "mostrar inventario",
|
||||||
|
"World": "Mundo",
|
||||||
|
"Show more help!": "¡Mostrar más ayuda!",
|
||||||
|
"Goal": "Objetivo",
|
||||||
|
"Objects": "Objetos",
|
||||||
|
"Assumptions": "Hipótesis",
|
||||||
|
"Current Goal": "Objetivo actual",
|
||||||
|
"Further Goals": "Objetivos pendientes",
|
||||||
|
"No Goals": "Sin objetivos",
|
||||||
|
"Loading goal…": "Cargando objetivo…",
|
||||||
|
"Click somewhere in the Lean file to enable the infoview.": "Pulsa en algún lugar del archivo Lean para habilitar la vista de información.",
|
||||||
|
"Waiting for Lean server to start…": "Esperando a que el servidor Lean se inicie…",
|
||||||
|
"Level completed! 🎉": "Nivel completado 🎉",
|
||||||
|
"Level completed with warnings 🎭": "Nivel completado con advertencias 🎭",
|
||||||
|
"Failed command": "Comando fallido",
|
||||||
|
"Retry proof from here": "Reintentar la prueba desde aquí",
|
||||||
|
"Retry": "Reintentar",
|
||||||
|
"Active Goal": "Objetivo activo",
|
||||||
|
"Crashed! Go to editor mode and fix your proof! Last server response:": "¡Error! Vaya al modo editor y corrija su prueba. Última respuesta del servidor:",
|
||||||
|
"Line": "Línea",
|
||||||
|
"Character": "Carácter",
|
||||||
|
"Loading messages…": "Cargando mensajes…",
|
||||||
|
"Execute": "Ejecutar",
|
||||||
|
"Tactics": "Tácticas",
|
||||||
|
"Definitions": "Definiciones",
|
||||||
|
"Theorems": "Teoremas",
|
||||||
|
"Not unlocked yet": "No desbloqueado aún",
|
||||||
|
"Not available in this level": "No disponible en este nivel",
|
||||||
|
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Un repositorio de juegos para aprender el asistente de demostración <1>Lean</1>, <i>(Lean 4)</i> y su biblioteca matemática <5>mathlib</5> ",
|
||||||
|
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "No se ha cargado ningún juego. Use <1>http://localhost:3000/#/g/local/FOLDER</1> para abrir un juego directamente desde una carpeta local",
|
||||||
|
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>Si está considerando escribir su propio juego, use el <1>GameSkeleton Github Repo</1> como plantilla y lea <3>How to Create a Game</3>.</0><1>Puede cargar directamente los juegos en el servidor y jugarlo usando la URL adecuada. Las <1>instrucciones anteriores</1> también explican los detalles sobre cómo cargar su juego en el servidor. Le animamos a ponerse en contacto con nosotros si tiene preguntas.</1><p>Los juegos incluidos en esta página son añadidos manualmente. Por favor, contactenos y añadiremos el suyo encantados.</p>",
|
||||||
|
"Prerequisites": "Requisitos previos",
|
||||||
|
"Worlds": "Mundos",
|
||||||
|
"Levels": "Niveles",
|
||||||
|
"Language": "Idioma",
|
||||||
|
"Lean Game Server": "Servidor de Juegos de Lean",
|
||||||
|
"Development notes": "Notas de desarrollo",
|
||||||
|
"Adding new games": "Añadir nuevos juegos",
|
||||||
|
"Funding": "Financiación",
|
||||||
|
"Level": "Nivel",
|
||||||
|
"Introduction": "Introducción",
|
||||||
|
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>¿Desea eliminar su progreso guardado definitivamente?</p><p>(Esto elimina sus pruebas y su inventario recopilado. Los progresos guardados de otros juegos no se eliminan.)</p>",
|
||||||
|
"Delete Progress?": "¿Borrar Progreso?",
|
||||||
|
"Delete": "Borrar",
|
||||||
|
"Download & Delete": "Descargar y Borrar",
|
||||||
|
"Cancel": "Cancelar",
|
||||||
|
"Mobile": "Móvil",
|
||||||
|
"Auto": "Automático",
|
||||||
|
"Desktop": "Escritorio",
|
||||||
|
"Layout": "Diseño",
|
||||||
|
"Always visible": "Siempre visible",
|
||||||
|
"Save my settings (in the browser store)": "Guardar mis ajustes (en el almacenamiento del navegador)",
|
||||||
|
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>Las reglas del juego determinan si se permite saltarse niveles y si el juego realiza comprobaciones para permitir únicamente tácticas y teoremas desbloqueados en las pruebas.</p><1>Nota: las tácticas (o teoremas) \"Desbloqueadas\" está determinadas por dos cosas: el conjunto mínimo de tácticas necesarias para resolver un nivel, más cualquier táctica que hayas desbloqueado en otro nivel. Esto significa que si desbloqueas <1>simp</1> en un nivel, puedes usarlo a partir de entonces en cualquier nivel.</1><p>Las opciones son:</p>",
|
||||||
|
"Game Rules": "Reglas del juego",
|
||||||
|
"levels": "niveles",
|
||||||
|
"tactics": "tácticas",
|
||||||
|
"regular": "normal",
|
||||||
|
"relaxed": "relajado",
|
||||||
|
"none": "ninguno",
|
||||||
|
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>Seleccione un archivo JSON con el progreso del juego guardado para cargar su progreso.</p><1><0>Advertencia:</0> Esto borrará su progreso actual en el juego. Considere <2>descargar su progreso actual</2> antes</1>",
|
||||||
|
"Upload Saved Progress": "Subir progreso guardado",
|
||||||
|
"Load selected file": "Cargar archivo seleccionado",
|
||||||
|
"Rules": "Reglas",
|
||||||
|
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "<p>Como este servidor corre en máquinas de nuestra universidad, tiene una capacidad limitada. Nuestra estimación actual es de unos 70 juegos simultaneos.</p>.",
|
||||||
|
"<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "<1>Muchos aspectos de los juegos y la infrastructura están aún en desarrollo. No dude en abrir una <1>GitHub Issue</1> sobre cualquier problema que experimente.</1>",
|
||||||
|
"This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "Este servidor se ha desarrollado como parte del proyecto <1>ADAM: Anticipating the Digital Age of Mathematics</1> en la Heinrich-Heine-Universität de Düsseldorf.",
|
||||||
|
"Server capacity": "",
|
||||||
|
"RAM": "",
|
||||||
|
" used": "",
|
||||||
|
"CPU": ""
|
||||||
|
}
|
||||||
@ -0,0 +1,8 @@
|
|||||||
|
/ko-level1.tmx
|
||||||
|
/ko-level2.tmx
|
||||||
|
/ko-omegat.tmx
|
||||||
|
/**/*.bak
|
||||||
|
/omegat/last_entry.properties
|
||||||
|
/omegat/files_order.txt
|
||||||
|
/omegat/project_stats.txt
|
||||||
|
/tm/*.tmx
|
||||||
@ -0,0 +1,15 @@
|
|||||||
|
# 린 4 게임
|
||||||
|
|
||||||
|
[English (영어)](./README.md) | 한국어
|
||||||
|
|
||||||
|
## 기여하기
|
||||||
|
|
||||||
|
`lean4game`의 한국어 번역에 기여하는 활동은 언제든지 환영합니다!
|
||||||
|
|
||||||
|
### 한국어 번역
|
||||||
|
|
||||||
|
저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
|
||||||
|
|
||||||
|
[bc]: https://github.com/chabulhwi
|
||||||
|
[omt]: https://omegat.org/
|
||||||
|
[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
|
||||||
@ -0,0 +1,18 @@
|
|||||||
|
# Lean 4 Game
|
||||||
|
|
||||||
|
English | [한국어[Korean]](./README.ko.md)
|
||||||
|
|
||||||
|
## Contributing
|
||||||
|
|
||||||
|
Contributions to the Korean translation of `lean4game` are always welcome!
|
||||||
|
|
||||||
|
### Korean Translation
|
||||||
|
|
||||||
|
I ([Bulhwi Cha][bc]) use [OmegaT][omt] to translate English documentation into
|
||||||
|
Korean. The OmegaT project is in this directory, that is,
|
||||||
|
`client/public/locales/ko`. You need to install the [Okapi filters plugin for
|
||||||
|
OmegaT][okapi] to make OmegaT parse JSON files.
|
||||||
|
|
||||||
|
[bc]: https://github.com/chabulhwi
|
||||||
|
[omt]: https://omegat.org/
|
||||||
|
[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
|
||||||
@ -0,0 +1,167 @@
|
|||||||
|
# Glossary in tab-separated format -*- coding: utf-8 -*-
|
||||||
|
St. Anselm 안셀무스
|
||||||
|
ontological 존재론적
|
||||||
|
argument 논증
|
||||||
|
argument 인수
|
||||||
|
Lean 린
|
||||||
|
Lean community 린 커뮤니티
|
||||||
|
God 신
|
||||||
|
Alvin Plantinga 앨빈 플랜팅아
|
||||||
|
exist 존재하다
|
||||||
|
existence 존재
|
||||||
|
the understanding 지성
|
||||||
|
reality 현실
|
||||||
|
assumption 가정
|
||||||
|
reductio 귀류법
|
||||||
|
great 큰
|
||||||
|
premise 전제
|
||||||
|
being 존재자
|
||||||
|
conceive 생각하다
|
||||||
|
definition 정의
|
||||||
|
true 참
|
||||||
|
true 참인
|
||||||
|
false 거짓
|
||||||
|
false 거짓인
|
||||||
|
formulate 정식화하다
|
||||||
|
formulation 정식화
|
||||||
|
formalize 형식화하다
|
||||||
|
formalization 형식화
|
||||||
|
property 속성
|
||||||
|
redundant 불필요한
|
||||||
|
sentence 문장
|
||||||
|
state 진술하다
|
||||||
|
statement 진술
|
||||||
|
proposition 명제
|
||||||
|
negation 부정
|
||||||
|
axiom 공리
|
||||||
|
theorem 정리
|
||||||
|
theory 이론
|
||||||
|
conclude 결론하다
|
||||||
|
prove 증명하다
|
||||||
|
SEP 스탠퍼드 철학 백과사전
|
||||||
|
Eric Wieser 에릭 비저
|
||||||
|
Alistair Tucker 앨리스터 터커
|
||||||
|
philosophy 철학
|
||||||
|
Owl of Sogang 서강올빼미
|
||||||
|
type theory 유형론
|
||||||
|
universe level 유형 세계 변수
|
||||||
|
type 유형
|
||||||
|
type 입력하다
|
||||||
|
type check 유형을 확인하다
|
||||||
|
type check 유형이 확인되다
|
||||||
|
type check 유형 확인이 잘되다
|
||||||
|
type class 유형 클래스
|
||||||
|
instance 사례
|
||||||
|
category mistake 범주 실수
|
||||||
|
class 클래스
|
||||||
|
example 보기
|
||||||
|
example 예
|
||||||
|
inductive type 귀납형
|
||||||
|
define 정의하다
|
||||||
|
constructor 구성자
|
||||||
|
Apache License, Version 2.0 아파치 라이선스, 버전 2.0
|
||||||
|
under the terms of 의 조건에 따라
|
||||||
|
OmegaT 오메가T
|
||||||
|
symbolic link 심벌릭 링크
|
||||||
|
directory 디렉터리
|
||||||
|
root directory 최상위 디렉터리
|
||||||
|
documentation 문서
|
||||||
|
English 영어
|
||||||
|
Korean 한국어
|
||||||
|
chapter 장
|
||||||
|
quiz 퀴즈
|
||||||
|
question 문제
|
||||||
|
command 명령어
|
||||||
|
error 오류
|
||||||
|
code 코드
|
||||||
|
evaluate 계산하다
|
||||||
|
keyword 핵심어
|
||||||
|
declare 선언하다
|
||||||
|
constant 상수
|
||||||
|
reference 참고 문헌
|
||||||
|
universe-polymorphic 세계 다형적
|
||||||
|
parametrically polymorphic 매개 변수 다형적
|
||||||
|
function 함수
|
||||||
|
identifier 식별자
|
||||||
|
definitionally equal 정의상 같은
|
||||||
|
natural number 자연수
|
||||||
|
input 입력값
|
||||||
|
return 반환하다
|
||||||
|
non-zero 영이 아닌
|
||||||
|
zero 영
|
||||||
|
alpha-equivalent 알파 동등한
|
||||||
|
less-than-or-equal-to sign 작거나 같음 부호
|
||||||
|
dependent function 의존 함수
|
||||||
|
dependent function type 의존 함수형
|
||||||
|
dependent product 의존곱
|
||||||
|
dependent product type 의존곱형
|
||||||
|
underscore 밑줄
|
||||||
|
implicit 암시적
|
||||||
|
explicit 명시적
|
||||||
|
sigma type 시그마
|
||||||
|
propositional logic 명제 논리
|
||||||
|
term 항
|
||||||
|
contemporary 동시대
|
||||||
|
term 용어
|
||||||
|
truth-value 진릿값
|
||||||
|
bearer 담지자
|
||||||
|
propositional attitudes 명제적 태도
|
||||||
|
believe 믿다
|
||||||
|
doubt 의심하다
|
||||||
|
South Korea 한국
|
||||||
|
school mathematics 학교 수학
|
||||||
|
sentence 문장
|
||||||
|
high school mathematics 고등학교 수학
|
||||||
|
teacher 교사
|
||||||
|
Stanford Encyclopedia of Philosophy 스탠퍼드 철학 백과사전
|
||||||
|
ordered triple 순서세짝
|
||||||
|
conjecture 추측
|
||||||
|
Goldbach's conjecture 골드바흐의 추측
|
||||||
|
interactive theorem prover 상호 작용 정리 증명기
|
||||||
|
truth 참
|
||||||
|
falsity 거짓
|
||||||
|
rule of inference 추론 규칙
|
||||||
|
introduction rule 도입 규칙
|
||||||
|
elimination rule 제거 규칙
|
||||||
|
ex falso quodlibet 엑스 팔소 세퀴투르 쿠오들리베트
|
||||||
|
principle of explosion 폭발 원리
|
||||||
|
propositional connective 명제 연결사
|
||||||
|
symbol 기호
|
||||||
|
refutation by contradiction 모순에 따른 부인
|
||||||
|
contradiction 모순
|
||||||
|
conjunction 연언
|
||||||
|
disjunction 선언(選言)
|
||||||
|
implication 함의
|
||||||
|
material implication 내용적 함의
|
||||||
|
conditional 조건문
|
||||||
|
modus ponens 긍정 논법[모더스 포넨스]
|
||||||
|
necessary condition 필요조건
|
||||||
|
conversion 역
|
||||||
|
inversion 이(裏)
|
||||||
|
contraposition 대우(對偶)
|
||||||
|
equivalence 동등
|
||||||
|
biconditional 쌍조건문
|
||||||
|
abbreviation 준말
|
||||||
|
if and only if …일 때 그리고 그럴 때만
|
||||||
|
editor 편집기
|
||||||
|
shortcut 단축키
|
||||||
|
Theorem Proving in Lean 4 린 4로 하는 정리 증명
|
||||||
|
exercise 연습 문제
|
||||||
|
repository 저장소
|
||||||
|
Jeremy Avigad 제러미 아비가드
|
||||||
|
Leonardo de Moura 레오나르두 지 모라
|
||||||
|
Soonho Kong 공순호
|
||||||
|
Sebastian Ullrich 제바스티안 울리히
|
||||||
|
file 파일
|
||||||
|
Markdown 마크다운
|
||||||
|
quiz 퀴즈
|
||||||
|
translation 번역
|
||||||
|
contribute 기여하다
|
||||||
|
progress 진도
|
||||||
|
capacity 이용량
|
||||||
|
GitHub 깃허브
|
||||||
|
repo 저장소
|
||||||
|
game rule 게임 규칙
|
||||||
|
unlocked 잠금 해제가 된
|
||||||
|
unlock 잠금 해제를 하다
|
||||||
|
Markdown 마크다운
|
||||||
@ -0,0 +1,33 @@
|
|||||||
|
<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
|
||||||
|
<omegat>
|
||||||
|
<project version="1.0">
|
||||||
|
<source_dir>__DEFAULT__</source_dir>
|
||||||
|
<source_dir_excludes>
|
||||||
|
<mask>**/.svn/**</mask>
|
||||||
|
<mask>**/CVS/**</mask>
|
||||||
|
<mask>**/.cvs/**</mask>
|
||||||
|
<mask>**/.git/**</mask>
|
||||||
|
<mask>**/.hg/**</mask>
|
||||||
|
<mask>**/.repositories/**</mask>
|
||||||
|
<mask>**/desktop.ini</mask>
|
||||||
|
<mask>**/Thumbs.db</mask>
|
||||||
|
<mask>**/.DS_Store</mask>
|
||||||
|
<mask>**/~$*</mask>
|
||||||
|
</source_dir_excludes>
|
||||||
|
<target_dir>__DEFAULT__</target_dir>
|
||||||
|
<tm_dir>__DEFAULT__</tm_dir>
|
||||||
|
<glossary_dir>__DEFAULT__</glossary_dir>
|
||||||
|
<glossary_file>__DEFAULT__</glossary_file>
|
||||||
|
<dictionary_dir>__DEFAULT__</dictionary_dir>
|
||||||
|
<export_tm_dir>__DEFAULT__</export_tm_dir>
|
||||||
|
<export_tm_levels>omegat level1 level2</export_tm_levels>
|
||||||
|
<source_lang>en</source_lang>
|
||||||
|
<target_lang>ko</target_lang>
|
||||||
|
<source_tok>org.omegat.tokenizer.LuceneEnglishTokenizer</source_tok>
|
||||||
|
<target_tok>org.omegat.tokenizer.HunspellTokenizer</target_tok>
|
||||||
|
<sentence_seg>true</sentence_seg>
|
||||||
|
<support_default_translations>true</support_default_translations>
|
||||||
|
<remove_tags>false</remove_tags>
|
||||||
|
<external_command></external_command>
|
||||||
|
</project>
|
||||||
|
</omegat>
|
||||||
File diff suppressed because it is too large
Load Diff
@ -0,0 +1 @@
|
|||||||
|
../README.md
|
||||||
@ -0,0 +1 @@
|
|||||||
|
../../en/translation.json
|
||||||
@ -0,0 +1,15 @@
|
|||||||
|
# 린 4 게임
|
||||||
|
|
||||||
|
[English (영어)](./README.md) | 한국어
|
||||||
|
|
||||||
|
## 기여하기
|
||||||
|
|
||||||
|
`lean4game`의 한국어 번역에 기여하는 활동은 언제든지 환영합니다!
|
||||||
|
|
||||||
|
### 한국어 번역
|
||||||
|
|
||||||
|
저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
|
||||||
|
|
||||||
|
[bc]: https://github.com/chabulhwi
|
||||||
|
[omt]: https://omegat.org/
|
||||||
|
[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
|
||||||
@ -0,0 +1,99 @@
|
|||||||
|
{
|
||||||
|
"Tactics": "전략",
|
||||||
|
"Lean Game Server": "린 게임 서버",
|
||||||
|
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>게임 규칙에 따라, 단계들을 건너뛰어도 되는지 그리고 증명을 작성할 때 잠금 해제가 된 전략과 정리만 이용할 수 있는지가 정해집니다.</p><1>\n\n참고: '잠금 해제'가 된 전략이나 정리는 다음 두 부류로 정해집니다. (1) 해당 단계를 푸는 데 필요한 최소한의 전략이나 정리의 모임, (2) 다른 단계에서 잠금 해제를 한 전략이나 정리. 따라서 여러분이 <1>simp</1> 전략을 잠금 해제 하면, 그 뒤로 어느 단계에서든 이 전략을 이용할 수 있습니다.</1><p>선택할 수 있는 게임 규칙은 다음과 같습니다.</p>",
|
||||||
|
"Game Rules": "게임 규칙",
|
||||||
|
"levels": "단계",
|
||||||
|
"tactics": "전략",
|
||||||
|
"regular": "일반",
|
||||||
|
"relaxed": "완화됨",
|
||||||
|
"none": "없음",
|
||||||
|
"Rules": "규칙",
|
||||||
|
"Intro": "소개",
|
||||||
|
"Game Introduction": "게임 소개",
|
||||||
|
"World selection": "세계 선택",
|
||||||
|
"Start": "시작하기",
|
||||||
|
"Inventory": "인벤토리",
|
||||||
|
"next level": "다음 단계",
|
||||||
|
"Next": "다음",
|
||||||
|
"back to world selection": "세계 선택하러 돌아가기",
|
||||||
|
"Leave World": "세계에서 나가기",
|
||||||
|
"previous level": "이전 단계",
|
||||||
|
"Previous": "이전",
|
||||||
|
"Editor mode is enforced!": "편집기 모드가 강제됐습니다!",
|
||||||
|
"Editor mode": "편집기 모드",
|
||||||
|
"Typewriter mode": "타자기 모드",
|
||||||
|
"information, Impressum, privacy policy": "정보, 관리자 정보, 사생활 정책",
|
||||||
|
"Preferences": "기본 설정",
|
||||||
|
"Game Info & Credits": "게임 정보 및 제작자 명단",
|
||||||
|
"Game Info": "게임 정보",
|
||||||
|
"Clear Progress": "진도 없애기",
|
||||||
|
"Erase": "지우기",
|
||||||
|
"Download Progress": "진도 내려받기",
|
||||||
|
"Download": "내려받기",
|
||||||
|
"Load Progress from JSON": "JSON에서 진도 불러오기",
|
||||||
|
"Upload": "업로드",
|
||||||
|
"Home": "홈",
|
||||||
|
"back to games selection": "게임 선택하러 돌아가기",
|
||||||
|
"close inventory": "인벤토리 닫기",
|
||||||
|
"show inventory": "인벤토리 보기",
|
||||||
|
"World": "세계",
|
||||||
|
"Show more help!": "도움말 더 보기!",
|
||||||
|
"Goal": "목표",
|
||||||
|
"Current Goal": "현재 목표",
|
||||||
|
"Objects": "객체",
|
||||||
|
"Assumptions": "가정",
|
||||||
|
"Further Goals": "이후 목표",
|
||||||
|
"No Goals": "목표 없음",
|
||||||
|
"Loading goal…": "목표 불러오는 중…",
|
||||||
|
"Click somewhere in the Lean file to enable the infoview.": "린 파일의 아무 곳이나 눌러 정보창을 여십시오.",
|
||||||
|
"Waiting for Lean server to start…": "린 서버가 시작하기를 기다리는 중…",
|
||||||
|
"Level completed! 🎉": "단계 완료! 🎉",
|
||||||
|
"Level completed with warnings 🎭": "경고 있는 채로 단계 완료 🎭",
|
||||||
|
"Active Goal": "활성화된 목표",
|
||||||
|
"Crashed! Go to editor mode and fix your proof! Last server response:": "시스템 다운됨! 편집기 모드에서 증명을 고치십시오! 마지막 서버 응답:",
|
||||||
|
"Line": "줄",
|
||||||
|
"Character": "문자",
|
||||||
|
"Loading messages…": "메시지 불러오는 중…",
|
||||||
|
"Execute": "실행하기",
|
||||||
|
"Definitions": "정의",
|
||||||
|
"Theorems": "정리",
|
||||||
|
"Not unlocked yet": "아직 잠금 해제가 안 됨",
|
||||||
|
"Not available in this level": "이 단계에서 쓸 수 없음",
|
||||||
|
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "<1>린(Lean 4)</1> 증명 보조기와 그 수학 라이브러리 <5>매스리브(mathlib)</5>를 학습하기 위한 게임들의 저장소",
|
||||||
|
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "불러온 게임 없음. <1>http://localhost:3000/#/g/local/FOLDER</1>를 이용해 지역[로컬] 폴더에서 게임을 직접 여십시오.",
|
||||||
|
"Prerequisites": "선행 요건",
|
||||||
|
"Worlds": "세계",
|
||||||
|
"Levels": "단계",
|
||||||
|
"Language": "언어",
|
||||||
|
"Server capacity": "서버 이용량",
|
||||||
|
"RAM": "램",
|
||||||
|
"CPU": "CPU",
|
||||||
|
"Development notes": "개발 노트",
|
||||||
|
"Adding new games": "새 게임 추가하기",
|
||||||
|
"Funding": "재정 지원",
|
||||||
|
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>저장된 진도를 불가역적으로 삭제하시겠습니까?</p><p>(이를 선택하시면 증명과 인벤토리 안의 수집 항목들이 삭제됩니다. 다른 게임에 저장된 정보는 삭제되지 않습니다.)</p>",
|
||||||
|
"Delete Progress?": "진도를 삭제하시겠습니까?",
|
||||||
|
"Delete": "삭제하기",
|
||||||
|
"Download & Delete": "내려받고 삭제하기",
|
||||||
|
"Cancel": "취소하기",
|
||||||
|
"Layout": "레이아웃",
|
||||||
|
"Always visible": "항상 보임",
|
||||||
|
"Save my settings (in the browser store)": "(브라우저에) 설정 저장하기",
|
||||||
|
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>저장된 게임 진도가 있는 JSON 파일을 선택해 진도를 불러오십시오.</p><1><0>경고:</0> 이를 실행하면 현재의 게임 진도가 삭제됩니다! <2>현재의 게임 진도</2>를 먼저 내려받을지 판단하십시오!</1>",
|
||||||
|
"Upload Saved Progress": "저장된 진도 업로드",
|
||||||
|
"Load selected file": "선택한 파일 열기",
|
||||||
|
"Mobile": "모바일",
|
||||||
|
"Auto": "자동",
|
||||||
|
"Desktop": "데스크톱",
|
||||||
|
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>여러분이 직접 게임을 작성할 생각이 있다면, <1>GameSkeleton 깃허브 저장소</1>를 양식[템플릿]으로 이용하고 <3>'게임 만들기(Creating a Game)'</3> 문서를 읽으십시오.</0><1>여러분이 작성한 게임을 직접 서버에서 불러오고, 정확한 URL을 이용해 그 게임을 하실 수 있습니다. 여러분의 게임을 서버에서 불러오는 방법에 관한 세부 사항도 위의 <1>설명서</1>에 나와 있습니다. 궁금한 점이 있으면 저희에게 연락해 주십시오.</1><p>이 페이지에 실린 게임들은 수동으로 추가됐습니다. 저희에게 연락하시면 여러분의 게임을 기꺼이 추가하겠습니다.",
|
||||||
|
"Level": "단계",
|
||||||
|
"Introduction": "소개",
|
||||||
|
"Retry proof from here": "여기부터 증명 다시 시도하기",
|
||||||
|
"Retry": "다시 시도하기",
|
||||||
|
"Failed command": "실패한 명령",
|
||||||
|
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "",
|
||||||
|
"<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "",
|
||||||
|
"This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "",
|
||||||
|
" used": ""
|
||||||
|
}
|
||||||
@ -0,0 +1 @@
|
|||||||
|
target/translation.json
|
||||||
Binary file not shown.
|
Before Width: | Height: | Size: 398 KiB |
@ -0,0 +1,37 @@
|
|||||||
|
{
|
||||||
|
"allGames": [
|
||||||
|
"leanprover-community/nng4",
|
||||||
|
"hhu-adam/robo",
|
||||||
|
"djvelleman/stg4",
|
||||||
|
"trequetrum/lean4game-logic",
|
||||||
|
"jadabouhawili/knightsandknaves-lean4game"
|
||||||
|
],
|
||||||
|
|
||||||
|
"languages": [
|
||||||
|
{
|
||||||
|
"iso": "en",
|
||||||
|
"flag": "GB",
|
||||||
|
"name": "English"
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"iso": "de",
|
||||||
|
"flag": "DE",
|
||||||
|
"name": "Deutsch"
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"iso": "zh",
|
||||||
|
"flag": "CN",
|
||||||
|
"name": "中文"
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"iso": "es",
|
||||||
|
"flag": "ES",
|
||||||
|
"name": "Español"
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"iso": "ko",
|
||||||
|
"flag": "KR",
|
||||||
|
"name": "한국어"
|
||||||
|
}
|
||||||
|
]
|
||||||
|
}
|
||||||
@ -1,68 +0,0 @@
|
|||||||
/**
|
|
||||||
* @fileOverview todo
|
|
||||||
*/
|
|
||||||
|
|
||||||
import * as React from 'react';
|
|
||||||
import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
|
|
||||||
import { LeanClient } from 'lean4web/client/src/editor/leanclient';
|
|
||||||
|
|
||||||
export class Connection {
|
|
||||||
private game: string = undefined // We only keep a connection to a single game at a time
|
|
||||||
private leanClient: LeanClient = null
|
|
||||||
|
|
||||||
getLeanClient(game): LeanClient {
|
|
||||||
if (this.game !== game) {
|
|
||||||
if (this.leanClient) {
|
|
||||||
this.leanClient.stop() // Stop previous Lean client
|
|
||||||
}
|
|
||||||
this.game = game
|
|
||||||
// Start a new Lean client for the new `gameId`.
|
|
||||||
const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + game
|
|
||||||
const uri = monaco.Uri.parse('file:///')
|
|
||||||
this.leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
|
|
||||||
}
|
|
||||||
|
|
||||||
return this.leanClient
|
|
||||||
}
|
|
||||||
|
|
||||||
/** If not already started, starts the Lean client. resolves the returned promise as soon as a
|
|
||||||
* Lean client is running.
|
|
||||||
*/
|
|
||||||
startLeanClient = (game) => {
|
|
||||||
return new Promise<LeanClient>((resolve) => {
|
|
||||||
const leanClient = this.getLeanClient(game)
|
|
||||||
if (leanClient.isRunning()) {
|
|
||||||
resolve(leanClient)
|
|
||||||
} else {
|
|
||||||
if (!leanClient.isStarted()) {
|
|
||||||
leanClient.start()
|
|
||||||
}
|
|
||||||
leanClient.restarted(() => {
|
|
||||||
// This keep alive message is not recognized by the server,
|
|
||||||
// but it makes sure that the websocket connection does not
|
|
||||||
// time out after 60 seconds.
|
|
||||||
setInterval(() => {leanClient.sendNotification('$/keepAlive', {}) }, 5000)
|
|
||||||
resolve(leanClient)
|
|
||||||
})
|
|
||||||
}
|
|
||||||
})
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
export const connection = new Connection()
|
|
||||||
|
|
||||||
export const ConnectionContext = React.createContext(null);
|
|
||||||
|
|
||||||
export const useLeanClient = (gameId) => {
|
|
||||||
const leanClient = connection.getLeanClient(gameId)
|
|
||||||
const [leanClientStarted, setLeanClientStarted] = React.useState(leanClient.isStarted())
|
|
||||||
|
|
||||||
React.useEffect(() => {
|
|
||||||
const t1 = leanClient.restarted(() => { console.log("START"); setLeanClientStarted(true) })
|
|
||||||
const t2 = leanClient.stopped(() => { console.log("STOP"); setLeanClientStarted(false) })
|
|
||||||
|
|
||||||
return () => {t1.dispose(); t2.dispose()}
|
|
||||||
}, [leanClient, setLeanClientStarted])
|
|
||||||
|
|
||||||
return {leanClientStarted, leanClient}
|
|
||||||
}
|
|
||||||
@ -0,0 +1,35 @@
|
|||||||
|
import i18n from "i18next";
|
||||||
|
import Backend from "i18next-http-backend"
|
||||||
|
import { initReactI18next } from "react-i18next";
|
||||||
|
|
||||||
|
i18n
|
||||||
|
.use(initReactI18next)
|
||||||
|
.use(Backend)
|
||||||
|
.init({
|
||||||
|
ns: ['translation'],
|
||||||
|
backend: {
|
||||||
|
// > see https://github.com/i18next/i18next-http-backend
|
||||||
|
loadPath: function(lngs, namespaces: Array<string>) {
|
||||||
|
if (namespaces[0].startsWith("g/")) {
|
||||||
|
return '/i18n/{{ns}}/{{lng}}/Game.json';
|
||||||
|
} else {
|
||||||
|
return '/locales/{{lng}}/{{ns}}.json';
|
||||||
|
}
|
||||||
|
}
|
||||||
|
},
|
||||||
|
// > language to use, more information here:
|
||||||
|
// > https://www.i18next.com/overview/configuration-options#languages-namespaces-resources
|
||||||
|
lng: "en",
|
||||||
|
// we use natural language keys, so we don't need a fallback language.
|
||||||
|
fallbackLng: false,
|
||||||
|
// > you can use the i18n.changeLanguage function to change the language manually:
|
||||||
|
// > https://www.i18next.com/overview/api#changelanguage
|
||||||
|
// > if you're using a language detector, do not define the lng option
|
||||||
|
returnEmptyString: false,
|
||||||
|
interpolation: {
|
||||||
|
// > react already safes from xss
|
||||||
|
escapeValue: false
|
||||||
|
}
|
||||||
|
});
|
||||||
|
|
||||||
|
export default i18n;
|
||||||
@ -0,0 +1,45 @@
|
|||||||
|
import React, { useState } from "react";
|
||||||
|
import { useAppDispatch, useAppSelector } from "../../hooks";
|
||||||
|
import {
|
||||||
|
PreferencesState,
|
||||||
|
setLayout as setPreferencesLayout,
|
||||||
|
setIsSavePreferences as setPreferencesIsSavePreferences,
|
||||||
|
setLanguage as setLanguagePreferences,
|
||||||
|
getWindowDimensions,
|
||||||
|
AUTO_SWITCH_THRESHOLD
|
||||||
|
} from "../preferences";
|
||||||
|
|
||||||
|
|
||||||
|
const UsePreferences = () => {
|
||||||
|
const dispatch = useAppDispatch()
|
||||||
|
const [mobile, setMobile] = React.useState<boolean>()
|
||||||
|
|
||||||
|
const layout = useAppSelector((state) => state.preferences.layout);
|
||||||
|
const setLayout = (layout: PreferencesState["layout"]) => dispatch(setPreferencesLayout(layout))
|
||||||
|
|
||||||
|
const isSavePreferences = useAppSelector((state) => state.preferences.isSavePreferences);
|
||||||
|
const setIsSavePreferences = (isSave: boolean) => dispatch(setPreferencesIsSavePreferences(isSave))
|
||||||
|
|
||||||
|
const language = useAppSelector((state) => state.preferences.language);
|
||||||
|
const setLanguage = (lang: string) => dispatch(setLanguagePreferences(lang))
|
||||||
|
|
||||||
|
const automaticallyAdjustLayout = () => {
|
||||||
|
const {width} = getWindowDimensions()
|
||||||
|
setMobile(width < AUTO_SWITCH_THRESHOLD)
|
||||||
|
}
|
||||||
|
|
||||||
|
React.useEffect(()=>{
|
||||||
|
if (layout === "auto"){
|
||||||
|
void automaticallyAdjustLayout()
|
||||||
|
window.addEventListener('resize', automaticallyAdjustLayout)
|
||||||
|
|
||||||
|
return () => window.removeEventListener('resize', automaticallyAdjustLayout)
|
||||||
|
} else {
|
||||||
|
setMobile(layout === "mobile")
|
||||||
|
}
|
||||||
|
}, [layout])
|
||||||
|
|
||||||
|
return {mobile, layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage}
|
||||||
|
}
|
||||||
|
|
||||||
|
export default UsePreferences;
|
||||||
@ -0,0 +1,9 @@
|
|||||||
|
# Changelog
|
||||||
|
|
||||||
|
## v4.5.0
|
||||||
|
|
||||||
|
### Breaking changes
|
||||||
|
|
||||||
|
* Fix (#183): local store accepts case insensitive URL. The game progress has previously been saved under case sensitive URLs. You might need to recover old progress from your browser storage.
|
||||||
|
|
||||||
|
## Other
|
||||||
@ -0,0 +1,105 @@
|
|||||||
|
# Hints
|
||||||
|
|
||||||
|
Most important for game development are probably the "Hints". You can add Hints at any place in your proof using the `Hint` tactic
|
||||||
|
|
||||||
|
```
|
||||||
|
Statement .... := by
|
||||||
|
Hint "Hint to show at the start"
|
||||||
|
rw [h]
|
||||||
|
Hint "some tip after using rw"
|
||||||
|
...
|
||||||
|
```
|
||||||
|
|
||||||
|
Note that hints are only **context-aware but not history-aware**. In particular, they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps to place hints outside the sample solution's proof.
|
||||||
|
|
||||||
|
## 1. When do hints show?
|
||||||
|
|
||||||
|
A hint will be displayed if the player's goal matches the one where the hint was placed in the
|
||||||
|
sample solutions and the entire context from the sample solutions is present in the
|
||||||
|
player's context. The player's context may contain additional items.
|
||||||
|
|
||||||
|
This means if you have multiple identical
|
||||||
|
subgoals, you should only place a single hint in one of them, and it will be displayed in
|
||||||
|
all of them.
|
||||||
|
|
||||||
|
However, identical (non-hidden) hints which where already present in the step
|
||||||
|
before are omitted. This is to allow a player to add new assumptions to context, for example
|
||||||
|
with `have`, without seeing the same hint over and over again.
|
||||||
|
Hidden hints are not filtered.
|
||||||
|
|
||||||
|
## 2. Alternative Proofs / `Branch`
|
||||||
|
|
||||||
|
You can use `Branch` to place hints
|
||||||
|
in dead ends or alternative proof strands.
|
||||||
|
|
||||||
|
A proof inside a `Branch`-block is normally evaluated by lean, but it's discarded at the end
|
||||||
|
so that no progress has been made on proving the goal.
|
||||||
|
|
||||||
|
```
|
||||||
|
Statement .... := by
|
||||||
|
Hint "use `rw` or `rewrite`."
|
||||||
|
Branch
|
||||||
|
rewrite [h]
|
||||||
|
Hint "now you still need `rfl`"
|
||||||
|
rw [h]
|
||||||
|
```
|
||||||
|
|
||||||
|
## 3. Variables names
|
||||||
|
|
||||||
|
Put variables in the hint text inside brackets like this: `{h}`! This way the server can replace
|
||||||
|
the variable's name with the one the user actually used.
|
||||||
|
|
||||||
|
*Note*: This means you need to escape any other uses of **opening** curly brackets (i.e. `\{`). See also [LaTeX in Games](latex.md) for
|
||||||
|
examples of this.
|
||||||
|
|
||||||
|
For example, if the sample proof contains
|
||||||
|
|
||||||
|
```
|
||||||
|
have h : True := trivial
|
||||||
|
Hint "Now use `rw [{h}]` to use your assumption `{h}`."
|
||||||
|
```
|
||||||
|
|
||||||
|
but the player writes `have g : True := trivial`, they will see a hint saying
|
||||||
|
"Now use `rw [g]` to use your assumption `g`."
|
||||||
|
|
||||||
|
## 4. Hidden hints
|
||||||
|
|
||||||
|
Some hints can be hidden, and only show after the user clicks on a button to get additional
|
||||||
|
help. You mark a hint as hidden with `(hidden := true)`:
|
||||||
|
|
||||||
|
```
|
||||||
|
Hint (hidden := true) "some hidden hint"
|
||||||
|
```
|
||||||
|
|
||||||
|
## 5. Strict context matching
|
||||||
|
|
||||||
|
If you use the attribute `(strict := true)` a hint is only shown if the entire context
|
||||||
|
matches exactly the one where the hint is placed. With `(hint := false)`, which is the default,
|
||||||
|
it does not matter if additional assumptions are present in the player's context.
|
||||||
|
|
||||||
|
```
|
||||||
|
Hint (strict := true) "now use `have` to create a new assumption."
|
||||||
|
```
|
||||||
|
|
||||||
|
You should probably use `(strict := true)` if you want to give fine-grained details about
|
||||||
|
tactics like `have` which do not modify the goal or any existing assumptions, but only
|
||||||
|
create new assumptions.
|
||||||
|
|
||||||
|
## 6. Formatting
|
||||||
|
|
||||||
|
You can use Markdown to format your hints and you can
|
||||||
|
use LaTeX. See [LaTeX in Games](latex.md) for more details.
|
||||||
|
|
||||||
|
### Images
|
||||||
|
|
||||||
|
Hints and introductions/conclusions can also contain images.
|
||||||
|
|
||||||
|
For remote images, simply add:
|
||||||
|
|
||||||
|
```
|
||||||
|
<img src=\"https://url.com/to/image\"/>
|
||||||
|
```
|
||||||
|
|
||||||
|
Local images can currently only be included with a hack:
|
||||||
|
|
||||||
|
Images in the game's `images/` folder will be accessible at `data/g/[user]/[repo]/[image].[png|jpg|…]` and thus can be included as if they were external images.
|
||||||
@ -0,0 +1,78 @@
|
|||||||
|
There are multiple ways how to format the text content of your game. Notably Markdown with KaTeX.
|
||||||
|
|
||||||
|
# Escaping
|
||||||
|
Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
|
||||||
|
backslashes, but if you provide text inside a doc comment
|
||||||
|
`/-- -/` (e.g. in the `Statement` description) you do not!
|
||||||
|
|
||||||
|
This means for example you'd write `/-- $\iff$ -/` but `"$\\iff$"`.
|
||||||
|
|
||||||
|
Furthermore, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`.
|
||||||
|
|
||||||
|
# KaTeX
|
||||||
|
|
||||||
|
LaTeX syntax is provided trough the [KaTeX library](https://katex.org). KateX supports most but not all of latex and its packages.
|
||||||
|
See [supported](https://katex.org/docs/supported.html).
|
||||||
|
|
||||||
|
## Examples
|
||||||
|
|
||||||
|
### Commutative diagrams
|
||||||
|
|
||||||
|
Here is an example of how to write a commutative diagram in KaTeX:
|
||||||
|
|
||||||
|
$$
|
||||||
|
\begin{CD}
|
||||||
|
A @>{f}>> B @<{g}<< C \\
|
||||||
|
@V{h}VV @V{i}VV @V{j}VV \\
|
||||||
|
D @<{k}<< E @>{l}>> F \\
|
||||||
|
@A{m}AA @A{n}AA @V{p}VV \\
|
||||||
|
G @<{q}<< H @>{r}>> I
|
||||||
|
\end{CD}
|
||||||
|
$$
|
||||||
|
|
||||||
|
```
|
||||||
|
$$
|
||||||
|
\begin{CD}
|
||||||
|
A @>{f}>> B @<{g}<< C \\
|
||||||
|
@V{h}VV @V{i}VV @V{j}VV \\
|
||||||
|
D @<{k}<< E @>{l}>> F \\
|
||||||
|
@A{m}AA @A{n}AA @V{p}VV \\
|
||||||
|
G @<{q}<< H @>{r}>> I
|
||||||
|
\end{CD}
|
||||||
|
$$
|
||||||
|
```
|
||||||
|
|
||||||
|
Again, note that inside a string like `Hint`/`Introduction`/`Conclusion`/etc. you need to escape `\` and potentially `{`.
|
||||||
|
|
||||||
|
E.g. `\begin` as `\\begin`, `\\` as `\\\\` and inside a
|
||||||
|
`Hint`, `@>{f}>>` as `@>\{f}>>`.
|
||||||
|
|
||||||
|
See https://www.jmilne.org/not/Mamscd.pdf
|
||||||
|
|
||||||
|
### Truth Tables
|
||||||
|
|
||||||
|
KaTeX does not support the tabular environment. You can use the array environment instead.
|
||||||
|
|
||||||
|
$$
|
||||||
|
\begin{array}{|c|c|}
|
||||||
|
\hline
|
||||||
|
P & ¬P \\
|
||||||
|
\hline
|
||||||
|
T & F \\
|
||||||
|
F & T \\
|
||||||
|
\hline
|
||||||
|
\end{array}
|
||||||
|
$$
|
||||||
|
|
||||||
|
```
|
||||||
|
$$
|
||||||
|
\begin{array}{|c|c|}
|
||||||
|
\hline
|
||||||
|
P & ¬P \\
|
||||||
|
\hline
|
||||||
|
T & F \\
|
||||||
|
F & T \\
|
||||||
|
\hline
|
||||||
|
\end{array}
|
||||||
|
$$
|
||||||
|
```
|
||||||
@ -0,0 +1,36 @@
|
|||||||
|
# Publishing games
|
||||||
|
|
||||||
|
You can publish your game on the official [Lean Game Server](https://adam.math.hhu.de) in a few simple
|
||||||
|
steps.
|
||||||
|
|
||||||
|
## 1. Upload Game to github
|
||||||
|
|
||||||
|
First, you need your game in a public Github repository and make sure the github action has run.
|
||||||
|
You can check this by spotting the green checkmark on the start page, or by looking at the "Actions"
|
||||||
|
tab.
|
||||||
|
|
||||||
|
## 2. Import the game
|
||||||
|
|
||||||
|
You call the URL that's listed under "What's Next?" in the latest action run. Explicitly you call
|
||||||
|
the URL of the form
|
||||||
|
|
||||||
|
> adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY}
|
||||||
|
|
||||||
|
where `{USER}` and `{REPOSITORY}` are replaced with the github user and repository name.
|
||||||
|
|
||||||
|
You should see a white screen which shows import updates and eventually reports "Done."
|
||||||
|
|
||||||
|
## 3. Play the game
|
||||||
|
|
||||||
|
Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITORY}`!
|
||||||
|
|
||||||
|
## 4. Update
|
||||||
|
|
||||||
|
To upload a new version of the game you will have to repeat 1. and 2. whenever you want to publish the updated version.
|
||||||
|
|
||||||
|
## 5. Main page
|
||||||
|
|
||||||
|
Adding games to the main page happens manually by the server maintainers. Tell us if you want us
|
||||||
|
to add a tile for your game!
|
||||||
|
|
||||||
|
For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).
|
||||||
@ -0,0 +1,47 @@
|
|||||||
|
|
||||||
|
# Notes for Server maintainer
|
||||||
|
|
||||||
|
In order to set up the server to allow imports, one needs to create a
|
||||||
|
[Github Access token](https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens). A fine-grained access token with only reading rights for public
|
||||||
|
repos will suffice.
|
||||||
|
|
||||||
|
You need to set the environment variables `LEAN4GAME_GITHUB_USER` and `LEAN4GAME_GITHUB_TOKEN`
|
||||||
|
with your user name and access token. For example, you can set these in `ecosystem.config.cjs` if
|
||||||
|
you're using `pm2`
|
||||||
|
|
||||||
|
Then people can call:
|
||||||
|
|
||||||
|
> https://{website}/import/trigger/{owner}/{repo}
|
||||||
|
|
||||||
|
where you replace:
|
||||||
|
- website: The website your server runs on, e.g. `localhost:3000`
|
||||||
|
- owner, repo: The owner and repository name of the game you want to load from github.
|
||||||
|
|
||||||
|
will trigger to download the latest version of your game from github onto your server.
|
||||||
|
Once this import reports "Done", you should be able to play your game under:
|
||||||
|
|
||||||
|
> https://{website}/#/g/{owner}/{repo}
|
||||||
|
|
||||||
|
## Data management
|
||||||
|
Everything downloaded remains in the folder `lean4game/games`.
|
||||||
|
The subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
|
||||||
|
The other folders should only contain the built lean-games, sorted by owner and repo.
|
||||||
|
|
||||||
|
## Server capacity
|
||||||
|
|
||||||
|
If you would like to display the server capacity on the landing page,
|
||||||
|
you can create a file `lean4game/games/stats.csv` of the following form:
|
||||||
|
|
||||||
|
```
|
||||||
|
CPU,MEM
|
||||||
|
0.1,0.8
|
||||||
|
```
|
||||||
|
|
||||||
|
These numbers will be displayed on the landing page ("CPU: 10 % used" and "RAM: 80 % used").
|
||||||
|
|
||||||
|
If you only want one of the numbers, replace the number you don't want with `nan` (or anything
|
||||||
|
else which does not parse as number).
|
||||||
|
|
||||||
|
If you don't want to show either, simply do not create `stats.csv`
|
||||||
|
|
||||||
|
Use your own script or cronjob to update the CSV file as desired.
|
||||||
@ -0,0 +1,30 @@
|
|||||||
|
# Translation
|
||||||
|
|
||||||
|
The game server supports internationalisation ("i18n") using [lean-i18n](https://github.com/hhu-adam/lean-i18n) and [i18next](https://www.npmjs.com/package/i18next).
|
||||||
|
|
||||||
|
The intended workflow currently is the following:
|
||||||
|
|
||||||
|
1. When you call `lake build` in your game, it should automatically create a template file `.i18n/en/Game.pot`. Alternatively you can call `lake exe i18n --template` to recreate it.
|
||||||
|
2. Open the file `Game.pot` (the "t" stands for "template") with [Poedit](https://poedit.net/) (or a similar software) and translate all strings. Save your work as `.i18n/{language}/Game.po`.
|
||||||
|
4. Call `lake exe i18n --export-json` to create all Json files `.i18n/{language}/Game.json` which the server needs.
|
||||||
|
5. Add your translations (i.e. `.po` and `.json`, but not the `.mo` files) and push your results, and [publish the game](publish_game.md).
|
||||||
|
|
||||||
|
If you choose the correct language in the "Preferences" of the game, you should see your translations.
|
||||||
|
|
||||||
|
## Alternative: avoiding .po
|
||||||
|
|
||||||
|
Note: This workflow is subject to change, and it might be that in future the server can directly read `.po` files. Until then, there is also an alternative workflow you might choose:
|
||||||
|
|
||||||
|
0. Add `useJson: true` to `.i18n/config.json`
|
||||||
|
1. `lake build` or `lake exe i18n --template` will now create a Json instead: `.i18n/en/Game.json`.
|
||||||
|
2. Add translations to a copy of this Json an save it as `.i18n/{language}/Game.json`
|
||||||
|
|
||||||
|
## Non-English games
|
||||||
|
|
||||||
|
For games written in a language different than English, you should set the correct source language (`sourceLang`) in `.i18n/config.json`. Afterwards, on `lake build` the template should appear under the chosen language, and can be translated (e.g. into English) as described above.
|
||||||
|
|
||||||
|
## New languages
|
||||||
|
|
||||||
|
The server has a set number of languages one can select.
|
||||||
|
If your game has been translated to a language not selectable, [open an issue at lean4game](https://github.com/leanprover-community/lean4game/issues) requesting this new language.
|
||||||
|
Or, even better, create a PR to translate the [server interface](https://github.com/leanprover-community/lean4game/tree/main/client/public/locales) into that new language.
|
||||||
@ -0,0 +1,37 @@
|
|||||||
|
# Troubleshooting
|
||||||
|
|
||||||
|
Here are some issues experienced by users.
|
||||||
|
|
||||||
|
- You can reset the lake projects involved (i.e. the `server/` folder here as well as your [game's folder](https://github.com/hhu-adam/GameSkeleton)) with the following commands:
|
||||||
|
```
|
||||||
|
cd [THE PROJECT]
|
||||||
|
rm -rf .lake/
|
||||||
|
lake update -R
|
||||||
|
lake build
|
||||||
|
```
|
||||||
|
If you experience problems related to Lean or lake, you should first try to reset it this way.
|
||||||
|
|
||||||
|
# VSCode Dev-Container
|
||||||
|
* If you don't get the pop-up, you might have disabled them, and you can reenable it by
|
||||||
|
running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
|
||||||
|
* If the starting the container fails, in particular with a message `Error: network xyz not found`,
|
||||||
|
you might have deleted stuff from docker via your shell. Try deleting the container and image
|
||||||
|
explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
|
||||||
|
container. (this will again take some time)
|
||||||
|
* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.
|
||||||
|
|
||||||
|
|
||||||
|
# Manual Installation
|
||||||
|
Here are known issues/pitfalls with the local setup using `npm`.
|
||||||
|
|
||||||
|
* If `CDPATH` is set on your mac/linux system, it might provide issues with `npm start` resulting in a server crash or blank screen. In particular `npm start` will display
|
||||||
|
```
|
||||||
|
[server] sh: line 0: cd: server: No such file or directory
|
||||||
|
[server] npm run start_server exited with code 1
|
||||||
|
```
|
||||||
|
As a fix you might need to delete your manually set `CDPATH` environment variable.
|
||||||
|
|
||||||
|
# Publication
|
||||||
|
Errors concerning uploads to the server.
|
||||||
|
|
||||||
|
* Your game overview loads but the server crashes on loading a level: Check your game's github action is identical to the [GameSkeleton's](https://github.com/hhu-adam/GameSkeleton/blob/main/.github/workflows/build.yml), in particular that there is a step about building the "`gameserver`-executable".
|
||||||
@ -0,0 +1,52 @@
|
|||||||
|
# How to update your Game
|
||||||
|
|
||||||
|
## New Lean version
|
||||||
|
|
||||||
|
You can update the game to any Lean version by simply editing the `lean-toolchain` in your game repo to contain the
|
||||||
|
new lean version `leanprover/lean4:v4.X.0`.
|
||||||
|
|
||||||
|
Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https://github.com/leanprover-community/lean4game/tags).
|
||||||
|
|
||||||
|
Then, depending on the setup you use, do one of the following:
|
||||||
|
|
||||||
|
* **Dev Container**: Rebuild the VSCode Devcontainer (without Cache!).
|
||||||
|
* **Local Setup**: in your game's folder run the following:
|
||||||
|
```
|
||||||
|
lake update -R
|
||||||
|
lake build
|
||||||
|
```
|
||||||
|
|
||||||
|
* Additionally, if you have a local copy of the server `lean4game`,
|
||||||
|
you should update this one to the matching version. Run the following in the folder `lean4game/`:
|
||||||
|
```
|
||||||
|
git fetch
|
||||||
|
git checkout {VERSION_TAG}
|
||||||
|
npm install
|
||||||
|
```
|
||||||
|
where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
|
||||||
|
* **Gitpod/Codespaces**: Create a fresh one
|
||||||
|
|
||||||
|
This will update your game (and the mathlib version you might be using) to the new lean version.
|
||||||
|
|
||||||
|
## Newest developing setup
|
||||||
|
|
||||||
|
There are a few files in your game repository which are used for the developing setup
|
||||||
|
(dev container/codespaces/gitpod). If you need to update your developing setup, for example because it doesn't work
|
||||||
|
anymore, you will need to copy the relevant files from the [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) template into your game repo.
|
||||||
|
|
||||||
|
The relevant files are:
|
||||||
|
|
||||||
|
```
|
||||||
|
.devcontainer/
|
||||||
|
.docker/
|
||||||
|
.github/
|
||||||
|
.gitpod/
|
||||||
|
.vscode/
|
||||||
|
lakefile.lean
|
||||||
|
```
|
||||||
|
|
||||||
|
simply copy them from the `GameSkeleton` into your game and proceed as above,
|
||||||
|
i.e. `lake update -R && lake build`.
|
||||||
|
|
||||||
|
(Note: You should not need to modify any of these files, with the exception of the `lakefile.lean`,
|
||||||
|
where you need to add any dependencies of your game, or remove mathlib if you don't need it.)
|
||||||
@ -0,0 +1,14 @@
|
|||||||
|
services:
|
||||||
|
lean4game:
|
||||||
|
build: .
|
||||||
|
privileged: true # needed to run bubblewrap inside docker
|
||||||
|
environment:
|
||||||
|
- LEAN4GAME_GITHUB_USER=${LEAN4GAME_GITHUB_USER}
|
||||||
|
- LEAN4GAME_GITHUB_TOKEN=${LEAN4GAME_GITHUB_TOKEN}
|
||||||
|
ports:
|
||||||
|
- "8080:8080"
|
||||||
|
volumes:
|
||||||
|
- games_data:/app/games
|
||||||
|
|
||||||
|
volumes:
|
||||||
|
games_data:
|
||||||
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,43 @@
|
|||||||
|
import time
|
||||||
|
|
||||||
|
def measure_proc_stat() -> dict[str, int]:
|
||||||
|
proc_stat_header = open("/proc/stat", "r").readline()
|
||||||
|
proc_stat = proc_stat_header.split(' ')[2:]
|
||||||
|
proc_stat[-1] = proc_stat[-1].removesuffix('\n')
|
||||||
|
proc_stat = list(map(int, proc_stat))
|
||||||
|
|
||||||
|
proc_stat_dict= {'user': proc_stat[0],
|
||||||
|
'nice': proc_stat[1],
|
||||||
|
'system': proc_stat[2],
|
||||||
|
'idle': proc_stat[3],
|
||||||
|
'iowait': proc_stat[4],
|
||||||
|
'irq': proc_stat[5],
|
||||||
|
'softirq': proc_stat[6],
|
||||||
|
'steal': proc_stat[7],
|
||||||
|
'guest': proc_stat[8],
|
||||||
|
'guest_nice': proc_stat[9]}
|
||||||
|
|
||||||
|
return proc_stat_dict
|
||||||
|
|
||||||
|
if __name__ == "__main__":
|
||||||
|
"""
|
||||||
|
Script emulates htop calculation of CPU at the
|
||||||
|
moment of calling.
|
||||||
|
"""
|
||||||
|
prev = measure_proc_stat()
|
||||||
|
prev_idle = prev.get('idle') + prev.get('iowait')
|
||||||
|
prev_non_idle = prev.get('user') + prev.get('nice') + prev.get('system') + prev.get('irq') + prev.get('softirq') + prev.get('steal')
|
||||||
|
prev_total = prev_idle + prev_non_idle
|
||||||
|
|
||||||
|
time.sleep(0.1)
|
||||||
|
|
||||||
|
curr = measure_proc_stat()
|
||||||
|
curr_idle = curr.get('idle') + curr.get('iowait')
|
||||||
|
curr_non_idle = curr.get('user') + curr.get('nice') + curr.get('system') + curr.get('irq') + curr.get('softirq') + curr.get('steal')
|
||||||
|
curr_total = curr_idle + curr_non_idle
|
||||||
|
|
||||||
|
d_total = curr_total - prev_total
|
||||||
|
d_idle = curr_idle - prev_idle
|
||||||
|
|
||||||
|
cpu_usage = ((d_total - d_idle)/d_total)
|
||||||
|
print(cpu_usage)
|
||||||
@ -0,0 +1,251 @@
|
|||||||
|
import { WebSocketServer } from 'ws';
|
||||||
|
import express from 'express'
|
||||||
|
import path from 'path'
|
||||||
|
import * as cp from 'child_process';
|
||||||
|
import * as url from 'url';
|
||||||
|
import * as rpc from 'vscode-ws-jsonrpc';
|
||||||
|
import * as jsonrpcserver from 'vscode-ws-jsonrpc/server';
|
||||||
|
import os from 'os';
|
||||||
|
import fs from 'fs';
|
||||||
|
import anonymize from 'ip-anonymize';
|
||||||
|
import { importTrigger, importStatus } from './import.mjs'
|
||||||
|
import process from 'process';
|
||||||
|
import { spawn } from 'child_process'
|
||||||
|
// import fs from 'fs'
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Add a game here if the server should keep a queue of pre-loaded games ready at all times.
|
||||||
|
*
|
||||||
|
* IMPORTANT! Tags here need to be lower case!
|
||||||
|
*/
|
||||||
|
const queueLength = {
|
||||||
|
"g/hhu-adam/robo": 2,
|
||||||
|
"g/leanprover-community/nng4": 5,
|
||||||
|
"g/djvelleman/stg4": 2,
|
||||||
|
"g/trequetrum/lean4game-logic": 2,
|
||||||
|
}
|
||||||
|
|
||||||
|
const __filename = url.fileURLToPath(import.meta.url);
|
||||||
|
const __dirname = url.fileURLToPath(new URL('.', import.meta.url));
|
||||||
|
|
||||||
|
const app = express()
|
||||||
|
|
||||||
|
const PORT = process.env.PORT || 8080;
|
||||||
|
|
||||||
|
var router = express.Router();
|
||||||
|
|
||||||
|
router.get('/import/status/:owner/:repo', importStatus)
|
||||||
|
router.get('/import/trigger/:owner/:repo', importTrigger)
|
||||||
|
|
||||||
|
const server = app
|
||||||
|
.use(express.static(path.join(__dirname, '..', 'client', 'dist'))) // TODO: add a dist folder from inside the game
|
||||||
|
.use('/i18n/g/:owner/:repo/:lang/*', (req, res, next) => {
|
||||||
|
const owner = req.params.owner;
|
||||||
|
const repo = req.params.repo
|
||||||
|
const lang = req.params.lang
|
||||||
|
|
||||||
|
const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
|
||||||
|
const log = `${process.cwd()}/logs/game-access.log`
|
||||||
|
const header = "date;anon-ip;game;lang\n"
|
||||||
|
const data = `${new Date()};${ip};${owner}/${repo};${lang}\n`
|
||||||
|
|
||||||
|
fs.writeFile(log, header.concat(data), { flag: 'ax' }, (file_exists) => {
|
||||||
|
if (file_exists) {
|
||||||
|
fs.appendFile(log, data, (err) => {
|
||||||
|
if (err) console.log("Failed to append to log!")
|
||||||
|
});
|
||||||
|
}
|
||||||
|
});
|
||||||
|
|
||||||
|
console.log(`[${new Date()}] ${ip} requested translation for ${owner}/${repo} in ${lang}`)
|
||||||
|
|
||||||
|
const filename = req.params[0];
|
||||||
|
req.url = filename;
|
||||||
|
express.static(path.join(getGameDir(owner,repo),".i18n",lang))(req, res, next);
|
||||||
|
})
|
||||||
|
.use('/data/g/:owner/:repo/*', (req, res, next) => {
|
||||||
|
const owner = req.params.owner;
|
||||||
|
const repo = req.params.repo
|
||||||
|
const filename = req.params[0];
|
||||||
|
req.url = filename;
|
||||||
|
express.static(path.join(getGameDir(owner,repo),".lake","gamedata"))(req, res, next);
|
||||||
|
})
|
||||||
|
.use('/data/stats', (req, res, next) => {
|
||||||
|
const statsProcess = spawn('/bin/bash', [path.join(__dirname, "stats.sh"), process.pid])
|
||||||
|
let outputData = ''
|
||||||
|
let errorData = ''
|
||||||
|
statsProcess.stdout.on('data', (data) => {
|
||||||
|
outputData += data.toString();
|
||||||
|
})
|
||||||
|
statsProcess.stderr.on('data', (data) => {
|
||||||
|
errorData += data.toString();
|
||||||
|
})
|
||||||
|
statsProcess.on('close', (code) => {
|
||||||
|
if (code === 0) {
|
||||||
|
res.send(outputData);
|
||||||
|
} else {
|
||||||
|
res.status(500).send(`Error executing script: ${errorData}`)
|
||||||
|
console.error(`stats.sh exited with code ${code}. Error: ${errorData}`)
|
||||||
|
}
|
||||||
|
})
|
||||||
|
})
|
||||||
|
.use('/', router)
|
||||||
|
.listen(PORT, () => console.log(`Listening on ${PORT}`));
|
||||||
|
|
||||||
|
const wss = new WebSocketServer({ server })
|
||||||
|
|
||||||
|
var socketCounter = 0
|
||||||
|
|
||||||
|
const environment = process.env.NODE_ENV
|
||||||
|
const isDevelopment = environment === 'development'
|
||||||
|
|
||||||
|
/** We keep queues of started Lean Server processes to be ready when a user arrives */
|
||||||
|
const queue = {}
|
||||||
|
|
||||||
|
function getTag(owner, repo) {
|
||||||
|
return `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
|
||||||
|
}
|
||||||
|
|
||||||
|
function getGameDir(owner, repo) {
|
||||||
|
owner = owner.toLowerCase()
|
||||||
|
if (owner == 'local') {
|
||||||
|
if(!isDevelopment) {
|
||||||
|
console.error(`No local games in production mode.`)
|
||||||
|
return ""
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
if(!fs.existsSync(path.join(__dirname, '..', 'games'))) {
|
||||||
|
console.error(`Did not find the following folder: ${path.join(__dirname, '..', 'games')}`)
|
||||||
|
console.error('Did you already import any games?')
|
||||||
|
return ""
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
let game_dir = (owner == 'local') ?
|
||||||
|
path.join(__dirname, '..', '..', repo) : // note: here we need `repo` to be case sensitive
|
||||||
|
path.join(__dirname, '..', 'games', `${owner}`, `${repo.toLowerCase()}`)
|
||||||
|
|
||||||
|
if(!fs.existsSync(game_dir)) {
|
||||||
|
console.error(`Game '${game_dir}' does not exist!`)
|
||||||
|
return ""
|
||||||
|
}
|
||||||
|
|
||||||
|
return game_dir;
|
||||||
|
}
|
||||||
|
|
||||||
|
function startServerProcess(owner, repo) {
|
||||||
|
|
||||||
|
let game_dir = getGameDir(owner, repo)
|
||||||
|
if (!game_dir) return;
|
||||||
|
|
||||||
|
let serverProcess
|
||||||
|
if (isDevelopment) {
|
||||||
|
let args = ["--server", game_dir]
|
||||||
|
let binDir = path.join(game_dir, ".lake", "packages", "GameServer", "server", ".lake", "build", "bin")
|
||||||
|
// Note: `cwd` is important to be the `bin` directory as `Watchdog` calls `./gameserver` again
|
||||||
|
if (fs.existsSync(binDir)) {
|
||||||
|
// Try to use the game's own copy of `gameserver`.
|
||||||
|
serverProcess = cp.spawn("./gameserver", args, { cwd: binDir })
|
||||||
|
} else {
|
||||||
|
// If the game is built with `-Klean4game.local` there is no copy in the lake packages.
|
||||||
|
serverProcess = cp.spawn("./gameserver", args,
|
||||||
|
{ cwd: path.join(__dirname, "..", "server", ".lake", "build", "bin") })
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
serverProcess = cp.spawn("./bubblewrap.sh",
|
||||||
|
[ game_dir, path.join(__dirname, '..')],
|
||||||
|
{ cwd: __dirname })
|
||||||
|
}
|
||||||
|
|
||||||
|
serverProcess.on('error', error =>
|
||||||
|
console.error(`Launching Lean Server failed: ${error}`)
|
||||||
|
)
|
||||||
|
if (serverProcess.stderr !== null) {
|
||||||
|
serverProcess.stderr.on('data', data =>
|
||||||
|
console.error(`Lean Server: ${data}`)
|
||||||
|
)
|
||||||
|
}
|
||||||
|
return serverProcess
|
||||||
|
}
|
||||||
|
|
||||||
|
/** start Lean Server processes to refill the queue */
|
||||||
|
function fillQueue(tag) {
|
||||||
|
while (queue[tag].length < queueLength[tag]) {
|
||||||
|
let serverProcess
|
||||||
|
serverProcess = startServerProcess(tag)
|
||||||
|
if (serverProcess == null) {
|
||||||
|
console.error('serverProcess was undefined/null')
|
||||||
|
return
|
||||||
|
}
|
||||||
|
queue[tag].push(serverProcess)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// // TODO: We disabled queue for now
|
||||||
|
// if (!isDevelopment) { // Don't use queue in development
|
||||||
|
// for (let tag in queueLength) {
|
||||||
|
// queue[tag] = []
|
||||||
|
// fillQueue(tag)
|
||||||
|
// }
|
||||||
|
// }
|
||||||
|
|
||||||
|
const urlRegEx = /^\/websocket\/g\/([\w.-]+)\/([\w.-]+)$/
|
||||||
|
|
||||||
|
wss.addListener("connection", function(ws, req) {
|
||||||
|
const reRes = urlRegEx.exec(req.url)
|
||||||
|
if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; }
|
||||||
|
const owner = reRes[1]
|
||||||
|
const repo = reRes[2]
|
||||||
|
|
||||||
|
const tag = getTag(owner, repo)
|
||||||
|
|
||||||
|
let ps
|
||||||
|
if (!queue[tag] || queue[tag].length == 0) {
|
||||||
|
ps = startServerProcess(owner, repo)
|
||||||
|
} else {
|
||||||
|
console.info('Got process from the queue')
|
||||||
|
ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately
|
||||||
|
fillQueue(tag)
|
||||||
|
}
|
||||||
|
|
||||||
|
if (ps == null) {
|
||||||
|
console.error('server process is undefined/null')
|
||||||
|
return
|
||||||
|
}
|
||||||
|
|
||||||
|
socketCounter += 1;
|
||||||
|
const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
|
||||||
|
|
||||||
|
// TODO (Matvey): extract further information from `req`, for example browser language.
|
||||||
|
console.log(`[${new Date()}] Socket opened - ${ip} - ${owner}/${repo}`)
|
||||||
|
|
||||||
|
const socket = {
|
||||||
|
onMessage: (cb) => { ws.on("message", cb) },
|
||||||
|
onError: (cb) => { ws.on("error", cb) },
|
||||||
|
onClose: (cb) => { ws.on("close", cb) },
|
||||||
|
send: (data, cb) => { ws.send(data,cb) }
|
||||||
|
}
|
||||||
|
const reader = new rpc.WebSocketMessageReader(socket)
|
||||||
|
const writer = new rpc.WebSocketMessageWriter(socket)
|
||||||
|
const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
|
||||||
|
const serverConnection = jsonrpcserver.createProcessStreamConnection(ps)
|
||||||
|
socketConnection.forward(serverConnection, message => {
|
||||||
|
if (isDevelopment) {console.log(`CLIENT: ${JSON.stringify(message)}`)}
|
||||||
|
return message;
|
||||||
|
})
|
||||||
|
serverConnection.forward(socketConnection, message => {
|
||||||
|
if (isDevelopment) {console.log(`SERVER: ${JSON.stringify(message)}`)}
|
||||||
|
return message;
|
||||||
|
});
|
||||||
|
|
||||||
|
console.log(`[${new Date()}] Number of open sockets - ${socketCounter}`)
|
||||||
|
console.log(`[${new Date()}] Free RAM - ${Math.round(os.freemem() / 1024 / 1024)} / ${Math.round(os.totalmem() / 1024 / 1024)} MB`)
|
||||||
|
|
||||||
|
ws.on('close', () => {
|
||||||
|
console.log(`[${new Date()}] Socket closed - ${ip}`)
|
||||||
|
socketCounter -= 1
|
||||||
|
})
|
||||||
|
|
||||||
|
socketConnection.onClose(() => serverConnection.dispose())
|
||||||
|
serverConnection.onClose(() => socketConnection.dispose())
|
||||||
|
})
|
||||||
@ -0,0 +1,12 @@
|
|||||||
|
#!/usr/bin/env bash
|
||||||
|
|
||||||
|
# Load python interpreter
|
||||||
|
python=/usr/bin/python3
|
||||||
|
# Load python script
|
||||||
|
cpu_usage=relay/cpu_usage.py
|
||||||
|
# Execute python script
|
||||||
|
cpu=$($python $cpu_usage)
|
||||||
|
# Calculate memory usage by computing 1 - %free_memory
|
||||||
|
mem=$(free | sed '2q;d' | awk '{print 1 - ($4/$2)}')
|
||||||
|
|
||||||
|
printf "CPU, MEM\n%f, %f\n" $cpu $mem
|
||||||
@ -0,0 +1,34 @@
|
|||||||
|
#/bin/bash
|
||||||
|
|
||||||
|
ARTIFACT_ID=$1
|
||||||
|
OWNER=$2
|
||||||
|
REPO=$3
|
||||||
|
|
||||||
|
# mkdir -p games
|
||||||
|
cd games
|
||||||
|
|
||||||
|
# mkdir -p tmp
|
||||||
|
mkdir -p ${OWNER}
|
||||||
|
|
||||||
|
echo "Unpacking ZIP."
|
||||||
|
unzip -o tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip -d tmp/${OWNER}_${REPO}_${ARTIFACT_ID}
|
||||||
|
echo "Unpacking game."
|
||||||
|
|
||||||
|
# exit the npm project to avoid reloading. TODO: Where should we actually save these?
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
echo "Delete old version of the game"
|
||||||
|
rm -rf ${OWNER}/${REPO}
|
||||||
|
mkdir -p ${OWNER}/${REPO}
|
||||||
|
|
||||||
|
for f in tmp/${OWNER}_${REPO}_${ARTIFACT_ID}/* #Should only be one file
|
||||||
|
do
|
||||||
|
echo "Unpacking $f"
|
||||||
|
#tar -xvzf $f -C games/${OWNER}/${REPO}
|
||||||
|
unzip -q -o $f -d ${OWNER}/${REPO}
|
||||||
|
done
|
||||||
|
|
||||||
|
# Delete temporary files
|
||||||
|
rm -f tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip
|
||||||
|
rm -fr tmp/${OWNER}_${REPO}_${ARTIFACT_ID}
|
||||||
@ -1,3 +0,0 @@
|
|||||||
build
|
|
||||||
adam
|
|
||||||
nng
|
|
||||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue