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
|
||||
run-name: Build the project
|
||||
on: [push]
|
||||
on:
|
||||
workflow_dispatch:
|
||||
push:
|
||||
jobs:
|
||||
build:
|
||||
runs-on: ubuntu-latest
|
||||
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
|
||||
- name: print lean and lake versions
|
||||
run: |
|
||||
lean --version
|
||||
lake --version
|
||||
- run: npm install
|
||||
- run: npm run build
|
||||
|
||||
@ -1,6 +1,8 @@
|
||||
node_modules
|
||||
client/dist
|
||||
server/build
|
||||
server/lakefile.olean
|
||||
**/lake-packages/
|
||||
games/
|
||||
server/.lake
|
||||
**/.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
|
||||
(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).
|
||||
## Deployment con Docker Compose
|
||||
|
||||
## 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).
|
||||
In particular step 5 thereof explains [How to Run Games Locally](doc/running_locally.md).
|
||||
This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
|
||||
|
||||
### 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
|
||||
|
||||
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)
|
||||
- [Old documentation](doc/DOCUMENTATION.md)
|
||||
### Backend
|
||||
|
||||
not fully written yet.
|
||||
|
||||
* [Server](doc/DOCUMENTATION.md): describes the server part (i.e. the content of `server/` und `relay/`).
|
||||
|
||||
## Contributing
|
||||
|
||||
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
|
||||
|
||||
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 |
@ -1,55 +1,115 @@
|
||||
import * as React from 'react'
|
||||
import { Input, Typography } from '@mui/material'
|
||||
import { Input, MenuItem, Select, SelectChangeEvent, Typography } from '@mui/material'
|
||||
import Markdown from '../markdown'
|
||||
import Switch from '@mui/material/Switch';
|
||||
import { Switch, Button, ButtonGroup } from '@mui/material';
|
||||
import Box from '@mui/material/Box';
|
||||
import Slider from '@mui/material/Slider';
|
||||
import lean4gameConfig from '../../config.json'
|
||||
|
||||
import FormControlLabel from '@mui/material/FormControlLabel';
|
||||
|
||||
import { IMobileContext } from "../infoview/context"
|
||||
|
||||
interface PreferencesPopupProps extends IMobileContext{
|
||||
handleClose: () => void
|
||||
}
|
||||
|
||||
export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile, handleClose }: PreferencesPopupProps) {
|
||||
return <div className="modal-wrapper">
|
||||
<div className="modal-backdrop" onClick={handleClose} />
|
||||
<div className="modal">
|
||||
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
|
||||
<Typography variant="body1" component="div" className="settings">
|
||||
<div className='preferences-category'>
|
||||
<div className='category-title'>
|
||||
<h3>Mobile layout</h3>
|
||||
</div>
|
||||
<div className='preferences-item'>
|
||||
<FormControlLabel
|
||||
control={
|
||||
<Switch
|
||||
checked={mobile}
|
||||
onChange={() => setMobile(!mobile)}
|
||||
name="checked"
|
||||
color="primary"
|
||||
/>
|
||||
}
|
||||
label="Enable"
|
||||
labelPlacement="start"
|
||||
/>
|
||||
</div>
|
||||
<div className='preferences-item'>
|
||||
<FormControlLabel
|
||||
control={
|
||||
<Switch
|
||||
checked={!lockMobile}
|
||||
onChange={() => setLockMobile(!lockMobile)}
|
||||
name="checked"
|
||||
color="primary"
|
||||
/>
|
||||
}
|
||||
label="Auto"
|
||||
labelPlacement="start"
|
||||
/>
|
||||
</div>
|
||||
</div>
|
||||
</Typography>
|
||||
import { IPreferencesContext, PreferencesContext } from "../infoview/context"
|
||||
import ReactCountryFlag from 'react-country-flag';
|
||||
import { useTranslation } from 'react-i18next';
|
||||
|
||||
export function PreferencesPopup({ handleClose }: { handleClose: () => void }) {
|
||||
let { t } = useTranslation()
|
||||
const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
|
||||
|
||||
const marks = [
|
||||
{
|
||||
value: 0,
|
||||
label: t('Mobile'),
|
||||
key: "mobile"
|
||||
},
|
||||
{
|
||||
value: 1,
|
||||
label: t('Auto'),
|
||||
key: "auto"
|
||||
},
|
||||
{
|
||||
value: 2,
|
||||
label: t('Desktop'),
|
||||
key: "desktop"
|
||||
},
|
||||
];
|
||||
|
||||
const handlerChangeLayout = (_: Event, value: number) => {
|
||||
setLayout(marks[value].key as IPreferencesContext["layout"])
|
||||
}
|
||||
|
||||
const handlerChangeLanguage = (ev: SelectChangeEvent<string>) => {
|
||||
setLanguage(ev.target.value as IPreferencesContext["language"])
|
||||
}
|
||||
|
||||
return <div className="modal-wrapper">
|
||||
<div className="modal-backdrop" onClick={handleClose} />
|
||||
<div className="modal">
|
||||
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
|
||||
<Typography variant="body1" component="div" className="settings">
|
||||
<div className='preferences-category'>
|
||||
<div className='category-title'>
|
||||
<h3>{t("Language")}</h3>
|
||||
</div>
|
||||
<div className='preferences-item first leave-left-gap'>
|
||||
<FormControlLabel
|
||||
control={
|
||||
<Box sx={{ width: 300 }}>
|
||||
<Select
|
||||
value={language}
|
||||
label={t("Language")}
|
||||
onChange={handlerChangeLanguage}>
|
||||
{lean4gameConfig.languages.map(lang => {return <MenuItem key={`menu-item-lang-${lang.iso}`} value={lang.iso}><ReactCountryFlag countryCode={lang.flag}/> {lang.name}</MenuItem>})}
|
||||
</Select>
|
||||
</Box>
|
||||
}
|
||||
label=""
|
||||
/>
|
||||
</div>
|
||||
</div>
|
||||
<div className='preferences-category'>
|
||||
<div className='category-title'>
|
||||
<h3>{t("Layout")}</h3>
|
||||
</div>
|
||||
<div className='preferences-item first leave-left-gap'>
|
||||
<FormControlLabel
|
||||
control={
|
||||
<Box sx={{ width: 300 }}>
|
||||
<Slider
|
||||
aria-label={t("Always visible")}
|
||||
value={marks.find(item => item.key === layout).value}
|
||||
step={1}
|
||||
marks={marks}
|
||||
max={2}
|
||||
sx={{
|
||||
'& .MuiSlider-track': { display: 'none', },
|
||||
}}
|
||||
onChange={handlerChangeLayout}
|
||||
/>
|
||||
</Box>
|
||||
}
|
||||
label=""
|
||||
/>
|
||||
</div>
|
||||
</div>
|
||||
|
||||
<div className='preferences-category tail-category'>
|
||||
<div className='preferences-item'>
|
||||
<FormControlLabel
|
||||
control={
|
||||
<Switch
|
||||
checked={isSavePreferences}
|
||||
onChange={() => setIsSavePreferences(!isSavePreferences)}
|
||||
name="checked"
|
||||
color="primary"
|
||||
/>
|
||||
}
|
||||
label={t("Save my settings (in the browser store)")}
|
||||
labelPlacement="end"
|
||||
/>
|
||||
</div>
|
||||
</div>
|
||||
</Typography>
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
|
||||
@ -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
|
||||
File diff suppressed because it is too large
Load Diff
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue