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 |
@ -0,0 +1,37 @@
|
||||
{
|
||||
"allGames": [
|
||||
"leanprover-community/nng4",
|
||||
"hhu-adam/robo",
|
||||
"djvelleman/stg4",
|
||||
"trequetrum/lean4game-logic",
|
||||
"jadabouhawili/knightsandknaves-lean4game"
|
||||
],
|
||||
|
||||
"languages": [
|
||||
{
|
||||
"iso": "en",
|
||||
"flag": "GB",
|
||||
"name": "English"
|
||||
},
|
||||
{
|
||||
"iso": "de",
|
||||
"flag": "DE",
|
||||
"name": "Deutsch"
|
||||
},
|
||||
{
|
||||
"iso": "zh",
|
||||
"flag": "CN",
|
||||
"name": "中文"
|
||||
},
|
||||
{
|
||||
"iso": "es",
|
||||
"flag": "ES",
|
||||
"name": "Español"
|
||||
},
|
||||
{
|
||||
"iso": "ko",
|
||||
"flag": "KR",
|
||||
"name": "한국어"
|
||||
}
|
||||
]
|
||||
}
|
||||
@ -1,68 +0,0 @@
|
||||
/**
|
||||
* @fileOverview todo
|
||||
*/
|
||||
|
||||
import * as React from 'react';
|
||||
import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
|
||||
import { LeanClient } from 'lean4web/client/src/editor/leanclient';
|
||||
|
||||
export class Connection {
|
||||
private game: string = undefined // We only keep a connection to a single game at a time
|
||||
private leanClient: LeanClient = null
|
||||
|
||||
getLeanClient(game): LeanClient {
|
||||
if (this.game !== game) {
|
||||
if (this.leanClient) {
|
||||
this.leanClient.stop() // Stop previous Lean client
|
||||
}
|
||||
this.game = game
|
||||
// Start a new Lean client for the new `gameId`.
|
||||
const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + game
|
||||
const uri = monaco.Uri.parse('file:///')
|
||||
this.leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
|
||||
}
|
||||
|
||||
return this.leanClient
|
||||
}
|
||||
|
||||
/** If not already started, starts the Lean client. resolves the returned promise as soon as a
|
||||
* Lean client is running.
|
||||
*/
|
||||
startLeanClient = (game) => {
|
||||
return new Promise<LeanClient>((resolve) => {
|
||||
const leanClient = this.getLeanClient(game)
|
||||
if (leanClient.isRunning()) {
|
||||
resolve(leanClient)
|
||||
} else {
|
||||
if (!leanClient.isStarted()) {
|
||||
leanClient.start()
|
||||
}
|
||||
leanClient.restarted(() => {
|
||||
// This keep alive message is not recognized by the server,
|
||||
// but it makes sure that the websocket connection does not
|
||||
// time out after 60 seconds.
|
||||
setInterval(() => {leanClient.sendNotification('$/keepAlive', {}) }, 5000)
|
||||
resolve(leanClient)
|
||||
})
|
||||
}
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
export const connection = new Connection()
|
||||
|
||||
export const ConnectionContext = React.createContext(null);
|
||||
|
||||
export const useLeanClient = (gameId) => {
|
||||
const leanClient = connection.getLeanClient(gameId)
|
||||
const [leanClientStarted, setLeanClientStarted] = React.useState(leanClient.isStarted())
|
||||
|
||||
React.useEffect(() => {
|
||||
const t1 = leanClient.restarted(() => { console.log("START"); setLeanClientStarted(true) })
|
||||
const t2 = leanClient.stopped(() => { console.log("STOP"); setLeanClientStarted(false) })
|
||||
|
||||
return () => {t1.dispose(); t2.dispose()}
|
||||
}, [leanClient, setLeanClientStarted])
|
||||
|
||||
return {leanClientStarted, leanClient}
|
||||
}
|
||||
@ -0,0 +1,35 @@
|
||||
import i18n from "i18next";
|
||||
import Backend from "i18next-http-backend"
|
||||
import { initReactI18next } from "react-i18next";
|
||||
|
||||
i18n
|
||||
.use(initReactI18next)
|
||||
.use(Backend)
|
||||
.init({
|
||||
ns: ['translation'],
|
||||
backend: {
|
||||
// > see https://github.com/i18next/i18next-http-backend
|
||||
loadPath: function(lngs, namespaces: Array<string>) {
|
||||
if (namespaces[0].startsWith("g/")) {
|
||||
return '/i18n/{{ns}}/{{lng}}/Game.json';
|
||||
} else {
|
||||
return '/locales/{{lng}}/{{ns}}.json';
|
||||
}
|
||||
}
|
||||
},
|
||||
// > language to use, more information here:
|
||||
// > https://www.i18next.com/overview/configuration-options#languages-namespaces-resources
|
||||
lng: "en",
|
||||
// we use natural language keys, so we don't need a fallback language.
|
||||
fallbackLng: false,
|
||||
// > you can use the i18n.changeLanguage function to change the language manually:
|
||||
// > https://www.i18next.com/overview/api#changelanguage
|
||||
// > if you're using a language detector, do not define the lng option
|
||||
returnEmptyString: false,
|
||||
interpolation: {
|
||||
// > react already safes from xss
|
||||
escapeValue: false
|
||||
}
|
||||
});
|
||||
|
||||
export default i18n;
|
||||
@ -0,0 +1,45 @@
|
||||
import React, { useState } from "react";
|
||||
import { useAppDispatch, useAppSelector } from "../../hooks";
|
||||
import {
|
||||
PreferencesState,
|
||||
setLayout as setPreferencesLayout,
|
||||
setIsSavePreferences as setPreferencesIsSavePreferences,
|
||||
setLanguage as setLanguagePreferences,
|
||||
getWindowDimensions,
|
||||
AUTO_SWITCH_THRESHOLD
|
||||
} from "../preferences";
|
||||
|
||||
|
||||
const UsePreferences = () => {
|
||||
const dispatch = useAppDispatch()
|
||||
const [mobile, setMobile] = React.useState<boolean>()
|
||||
|
||||
const layout = useAppSelector((state) => state.preferences.layout);
|
||||
const setLayout = (layout: PreferencesState["layout"]) => dispatch(setPreferencesLayout(layout))
|
||||
|
||||
const isSavePreferences = useAppSelector((state) => state.preferences.isSavePreferences);
|
||||
const setIsSavePreferences = (isSave: boolean) => dispatch(setPreferencesIsSavePreferences(isSave))
|
||||
|
||||
const language = useAppSelector((state) => state.preferences.language);
|
||||
const setLanguage = (lang: string) => dispatch(setLanguagePreferences(lang))
|
||||
|
||||
const automaticallyAdjustLayout = () => {
|
||||
const {width} = getWindowDimensions()
|
||||
setMobile(width < AUTO_SWITCH_THRESHOLD)
|
||||
}
|
||||
|
||||
React.useEffect(()=>{
|
||||
if (layout === "auto"){
|
||||
void automaticallyAdjustLayout()
|
||||
window.addEventListener('resize', automaticallyAdjustLayout)
|
||||
|
||||
return () => window.removeEventListener('resize', automaticallyAdjustLayout)
|
||||
} else {
|
||||
setMobile(layout === "mobile")
|
||||
}
|
||||
}, [layout])
|
||||
|
||||
return {mobile, layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage}
|
||||
}
|
||||
|
||||
export default UsePreferences;
|
||||
@ -0,0 +1,9 @@
|
||||
# Changelog
|
||||
|
||||
## v4.5.0
|
||||
|
||||
### Breaking changes
|
||||
|
||||
* Fix (#183): local store accepts case insensitive URL. The game progress has previously been saved under case sensitive URLs. You might need to recover old progress from your browser storage.
|
||||
|
||||
## Other
|
||||
@ -0,0 +1,105 @@
|
||||
# Hints
|
||||
|
||||
Most important for game development are probably the "Hints". You can add Hints at any place in your proof using the `Hint` tactic
|
||||
|
||||
```
|
||||
Statement .... := by
|
||||
Hint "Hint to show at the start"
|
||||
rw [h]
|
||||
Hint "some tip after using rw"
|
||||
...
|
||||
```
|
||||
|
||||
Note that hints are only **context-aware but not history-aware**. In particular, they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps to place hints outside the sample solution's proof.
|
||||
|
||||
## 1. When do hints show?
|
||||
|
||||
A hint will be displayed if the player's goal matches the one where the hint was placed in the
|
||||
sample solutions and the entire context from the sample solutions is present in the
|
||||
player's context. The player's context may contain additional items.
|
||||
|
||||
This means if you have multiple identical
|
||||
subgoals, you should only place a single hint in one of them, and it will be displayed in
|
||||
all of them.
|
||||
|
||||
However, identical (non-hidden) hints which where already present in the step
|
||||
before are omitted. This is to allow a player to add new assumptions to context, for example
|
||||
with `have`, without seeing the same hint over and over again.
|
||||
Hidden hints are not filtered.
|
||||
|
||||
## 2. Alternative Proofs / `Branch`
|
||||
|
||||
You can use `Branch` to place hints
|
||||
in dead ends or alternative proof strands.
|
||||
|
||||
A proof inside a `Branch`-block is normally evaluated by lean, but it's discarded at the end
|
||||
so that no progress has been made on proving the goal.
|
||||
|
||||
```
|
||||
Statement .... := by
|
||||
Hint "use `rw` or `rewrite`."
|
||||
Branch
|
||||
rewrite [h]
|
||||
Hint "now you still need `rfl`"
|
||||
rw [h]
|
||||
```
|
||||
|
||||
## 3. Variables names
|
||||
|
||||
Put variables in the hint text inside brackets like this: `{h}`! This way the server can replace
|
||||
the variable's name with the one the user actually used.
|
||||
|
||||
*Note*: This means you need to escape any other uses of **opening** curly brackets (i.e. `\{`). See also [LaTeX in Games](latex.md) for
|
||||
examples of this.
|
||||
|
||||
For example, if the sample proof contains
|
||||
|
||||
```
|
||||
have h : True := trivial
|
||||
Hint "Now use `rw [{h}]` to use your assumption `{h}`."
|
||||
```
|
||||
|
||||
but the player writes `have g : True := trivial`, they will see a hint saying
|
||||
"Now use `rw [g]` to use your assumption `g`."
|
||||
|
||||
## 4. Hidden hints
|
||||
|
||||
Some hints can be hidden, and only show after the user clicks on a button to get additional
|
||||
help. You mark a hint as hidden with `(hidden := true)`:
|
||||
|
||||
```
|
||||
Hint (hidden := true) "some hidden hint"
|
||||
```
|
||||
|
||||
## 5. Strict context matching
|
||||
|
||||
If you use the attribute `(strict := true)` a hint is only shown if the entire context
|
||||
matches exactly the one where the hint is placed. With `(hint := false)`, which is the default,
|
||||
it does not matter if additional assumptions are present in the player's context.
|
||||
|
||||
```
|
||||
Hint (strict := true) "now use `have` to create a new assumption."
|
||||
```
|
||||
|
||||
You should probably use `(strict := true)` if you want to give fine-grained details about
|
||||
tactics like `have` which do not modify the goal or any existing assumptions, but only
|
||||
create new assumptions.
|
||||
|
||||
## 6. Formatting
|
||||
|
||||
You can use Markdown to format your hints and you can
|
||||
use LaTeX. See [LaTeX in Games](latex.md) for more details.
|
||||
|
||||
### Images
|
||||
|
||||
Hints and introductions/conclusions can also contain images.
|
||||
|
||||
For remote images, simply add:
|
||||
|
||||
```
|
||||
<img src=\"https://url.com/to/image\"/>
|
||||
```
|
||||
|
||||
Local images can currently only be included with a hack:
|
||||
|
||||
Images in the game's `images/` folder will be accessible at `data/g/[user]/[repo]/[image].[png|jpg|…]` and thus can be included as if they were external images.
|
||||
@ -0,0 +1,78 @@
|
||||
There are multiple ways how to format the text content of your game. Notably Markdown with KaTeX.
|
||||
|
||||
# Escaping
|
||||
Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
|
||||
backslashes, but if you provide text inside a doc comment
|
||||
`/-- -/` (e.g. in the `Statement` description) you do not!
|
||||
|
||||
This means for example you'd write `/-- $\iff$ -/` but `"$\\iff$"`.
|
||||
|
||||
Furthermore, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`.
|
||||
|
||||
# KaTeX
|
||||
|
||||
LaTeX syntax is provided trough the [KaTeX library](https://katex.org). KateX supports most but not all of latex and its packages.
|
||||
See [supported](https://katex.org/docs/supported.html).
|
||||
|
||||
## Examples
|
||||
|
||||
### Commutative diagrams
|
||||
|
||||
Here is an example of how to write a commutative diagram in KaTeX:
|
||||
|
||||
$$
|
||||
\begin{CD}
|
||||
A @>{f}>> B @<{g}<< C \\
|
||||
@V{h}VV @V{i}VV @V{j}VV \\
|
||||
D @<{k}<< E @>{l}>> F \\
|
||||
@A{m}AA @A{n}AA @V{p}VV \\
|
||||
G @<{q}<< H @>{r}>> I
|
||||
\end{CD}
|
||||
$$
|
||||
|
||||
```
|
||||
$$
|
||||
\begin{CD}
|
||||
A @>{f}>> B @<{g}<< C \\
|
||||
@V{h}VV @V{i}VV @V{j}VV \\
|
||||
D @<{k}<< E @>{l}>> F \\
|
||||
@A{m}AA @A{n}AA @V{p}VV \\
|
||||
G @<{q}<< H @>{r}>> I
|
||||
\end{CD}
|
||||
$$
|
||||
```
|
||||
|
||||
Again, note that inside a string like `Hint`/`Introduction`/`Conclusion`/etc. you need to escape `\` and potentially `{`.
|
||||
|
||||
E.g. `\begin` as `\\begin`, `\\` as `\\\\` and inside a
|
||||
`Hint`, `@>{f}>>` as `@>\{f}>>`.
|
||||
|
||||
See https://www.jmilne.org/not/Mamscd.pdf
|
||||
|
||||
### Truth Tables
|
||||
|
||||
KaTeX does not support the tabular environment. You can use the array environment instead.
|
||||
|
||||
$$
|
||||
\begin{array}{|c|c|}
|
||||
\hline
|
||||
P & ¬P \\
|
||||
\hline
|
||||
T & F \\
|
||||
F & T \\
|
||||
\hline
|
||||
\end{array}
|
||||
$$
|
||||
|
||||
```
|
||||
$$
|
||||
\begin{array}{|c|c|}
|
||||
\hline
|
||||
P & ¬P \\
|
||||
\hline
|
||||
T & F \\
|
||||
F & T \\
|
||||
\hline
|
||||
\end{array}
|
||||
$$
|
||||
```
|
||||
@ -0,0 +1,36 @@
|
||||
# Publishing games
|
||||
|
||||
You can publish your game on the official [Lean Game Server](https://adam.math.hhu.de) in a few simple
|
||||
steps.
|
||||
|
||||
## 1. Upload Game to github
|
||||
|
||||
First, you need your game in a public Github repository and make sure the github action has run.
|
||||
You can check this by spotting the green checkmark on the start page, or by looking at the "Actions"
|
||||
tab.
|
||||
|
||||
## 2. Import the game
|
||||
|
||||
You call the URL that's listed under "What's Next?" in the latest action run. Explicitly you call
|
||||
the URL of the form
|
||||
|
||||
> adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY}
|
||||
|
||||
where `{USER}` and `{REPOSITORY}` are replaced with the github user and repository name.
|
||||
|
||||
You should see a white screen which shows import updates and eventually reports "Done."
|
||||
|
||||
## 3. Play the game
|
||||
|
||||
Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITORY}`!
|
||||
|
||||
## 4. Update
|
||||
|
||||
To upload a new version of the game you will have to repeat 1. and 2. whenever you want to publish the updated version.
|
||||
|
||||
## 5. Main page
|
||||
|
||||
Adding games to the main page happens manually by the server maintainers. Tell us if you want us
|
||||
to add a tile for your game!
|
||||
|
||||
For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster).
|
||||
@ -0,0 +1,47 @@
|
||||
|
||||
# Notes for Server maintainer
|
||||
|
||||
In order to set up the server to allow imports, one needs to create a
|
||||
[Github Access token](https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens). A fine-grained access token with only reading rights for public
|
||||
repos will suffice.
|
||||
|
||||
You need to set the environment variables `LEAN4GAME_GITHUB_USER` and `LEAN4GAME_GITHUB_TOKEN`
|
||||
with your user name and access token. For example, you can set these in `ecosystem.config.cjs` if
|
||||
you're using `pm2`
|
||||
|
||||
Then people can call:
|
||||
|
||||
> https://{website}/import/trigger/{owner}/{repo}
|
||||
|
||||
where you replace:
|
||||
- website: The website your server runs on, e.g. `localhost:3000`
|
||||
- owner, repo: The owner and repository name of the game you want to load from github.
|
||||
|
||||
will trigger to download the latest version of your game from github onto your server.
|
||||
Once this import reports "Done", you should be able to play your game under:
|
||||
|
||||
> https://{website}/#/g/{owner}/{repo}
|
||||
|
||||
## Data management
|
||||
Everything downloaded remains in the folder `lean4game/games`.
|
||||
The subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
|
||||
The other folders should only contain the built lean-games, sorted by owner and repo.
|
||||
|
||||
## Server capacity
|
||||
|
||||
If you would like to display the server capacity on the landing page,
|
||||
you can create a file `lean4game/games/stats.csv` of the following form:
|
||||
|
||||
```
|
||||
CPU,MEM
|
||||
0.1,0.8
|
||||
```
|
||||
|
||||
These numbers will be displayed on the landing page ("CPU: 10 % used" and "RAM: 80 % used").
|
||||
|
||||
If you only want one of the numbers, replace the number you don't want with `nan` (or anything
|
||||
else which does not parse as number).
|
||||
|
||||
If you don't want to show either, simply do not create `stats.csv`
|
||||
|
||||
Use your own script or cronjob to update the CSV file as desired.
|
||||
@ -0,0 +1,30 @@
|
||||
# Translation
|
||||
|
||||
The game server supports internationalisation ("i18n") using [lean-i18n](https://github.com/hhu-adam/lean-i18n) and [i18next](https://www.npmjs.com/package/i18next).
|
||||
|
||||
The intended workflow currently is the following:
|
||||
|
||||
1. When you call `lake build` in your game, it should automatically create a template file `.i18n/en/Game.pot`. Alternatively you can call `lake exe i18n --template` to recreate it.
|
||||
2. Open the file `Game.pot` (the "t" stands for "template") with [Poedit](https://poedit.net/) (or a similar software) and translate all strings. Save your work as `.i18n/{language}/Game.po`.
|
||||
4. Call `lake exe i18n --export-json` to create all Json files `.i18n/{language}/Game.json` which the server needs.
|
||||
5. Add your translations (i.e. `.po` and `.json`, but not the `.mo` files) and push your results, and [publish the game](publish_game.md).
|
||||
|
||||
If you choose the correct language in the "Preferences" of the game, you should see your translations.
|
||||
|
||||
## Alternative: avoiding .po
|
||||
|
||||
Note: This workflow is subject to change, and it might be that in future the server can directly read `.po` files. Until then, there is also an alternative workflow you might choose:
|
||||
|
||||
0. Add `useJson: true` to `.i18n/config.json`
|
||||
1. `lake build` or `lake exe i18n --template` will now create a Json instead: `.i18n/en/Game.json`.
|
||||
2. Add translations to a copy of this Json an save it as `.i18n/{language}/Game.json`
|
||||
|
||||
## Non-English games
|
||||
|
||||
For games written in a language different than English, you should set the correct source language (`sourceLang`) in `.i18n/config.json`. Afterwards, on `lake build` the template should appear under the chosen language, and can be translated (e.g. into English) as described above.
|
||||
|
||||
## New languages
|
||||
|
||||
The server has a set number of languages one can select.
|
||||
If your game has been translated to a language not selectable, [open an issue at lean4game](https://github.com/leanprover-community/lean4game/issues) requesting this new language.
|
||||
Or, even better, create a PR to translate the [server interface](https://github.com/leanprover-community/lean4game/tree/main/client/public/locales) into that new language.
|
||||
@ -0,0 +1,37 @@
|
||||
# Troubleshooting
|
||||
|
||||
Here are some issues experienced by users.
|
||||
|
||||
- You can reset the lake projects involved (i.e. the `server/` folder here as well as your [game's folder](https://github.com/hhu-adam/GameSkeleton)) with the following commands:
|
||||
```
|
||||
cd [THE PROJECT]
|
||||
rm -rf .lake/
|
||||
lake update -R
|
||||
lake build
|
||||
```
|
||||
If you experience problems related to Lean or lake, you should first try to reset it this way.
|
||||
|
||||
# VSCode Dev-Container
|
||||
* If you don't get the pop-up, you might have disabled them, and you can reenable it by
|
||||
running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
|
||||
* If the starting the container fails, in particular with a message `Error: network xyz not found`,
|
||||
you might have deleted stuff from docker via your shell. Try deleting the container and image
|
||||
explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
|
||||
container. (this will again take some time)
|
||||
* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.
|
||||
|
||||
|
||||
# Manual Installation
|
||||
Here are known issues/pitfalls with the local setup using `npm`.
|
||||
|
||||
* If `CDPATH` is set on your mac/linux system, it might provide issues with `npm start` resulting in a server crash or blank screen. In particular `npm start` will display
|
||||
```
|
||||
[server] sh: line 0: cd: server: No such file or directory
|
||||
[server] npm run start_server exited with code 1
|
||||
```
|
||||
As a fix you might need to delete your manually set `CDPATH` environment variable.
|
||||
|
||||
# Publication
|
||||
Errors concerning uploads to the server.
|
||||
|
||||
* Your game overview loads but the server crashes on loading a level: Check your game's github action is identical to the [GameSkeleton's](https://github.com/hhu-adam/GameSkeleton/blob/main/.github/workflows/build.yml), in particular that there is a step about building the "`gameserver`-executable".
|
||||
@ -0,0 +1,52 @@
|
||||
# How to update your Game
|
||||
|
||||
## New Lean version
|
||||
|
||||
You can update the game to any Lean version by simply editing the `lean-toolchain` in your game repo to contain the
|
||||
new lean version `leanprover/lean4:v4.X.0`.
|
||||
|
||||
Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https://github.com/leanprover-community/lean4game/tags).
|
||||
|
||||
Then, depending on the setup you use, do one of the following:
|
||||
|
||||
* **Dev Container**: Rebuild the VSCode Devcontainer (without Cache!).
|
||||
* **Local Setup**: in your game's folder run the following:
|
||||
```
|
||||
lake update -R
|
||||
lake build
|
||||
```
|
||||
|
||||
* Additionally, if you have a local copy of the server `lean4game`,
|
||||
you should update this one to the matching version. Run the following in the folder `lean4game/`:
|
||||
```
|
||||
git fetch
|
||||
git checkout {VERSION_TAG}
|
||||
npm install
|
||||
```
|
||||
where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
|
||||
* **Gitpod/Codespaces**: Create a fresh one
|
||||
|
||||
This will update your game (and the mathlib version you might be using) to the new lean version.
|
||||
|
||||
## Newest developing setup
|
||||
|
||||
There are a few files in your game repository which are used for the developing setup
|
||||
(dev container/codespaces/gitpod). If you need to update your developing setup, for example because it doesn't work
|
||||
anymore, you will need to copy the relevant files from the [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) template into your game repo.
|
||||
|
||||
The relevant files are:
|
||||
|
||||
```
|
||||
.devcontainer/
|
||||
.docker/
|
||||
.github/
|
||||
.gitpod/
|
||||
.vscode/
|
||||
lakefile.lean
|
||||
```
|
||||
|
||||
simply copy them from the `GameSkeleton` into your game and proceed as above,
|
||||
i.e. `lake update -R && lake build`.
|
||||
|
||||
(Note: You should not need to modify any of these files, with the exception of the `lakefile.lean`,
|
||||
where you need to add any dependencies of your game, or remove mathlib if you don't need it.)
|
||||
@ -0,0 +1,14 @@
|
||||
services:
|
||||
lean4game:
|
||||
build: .
|
||||
privileged: true # needed to run bubblewrap inside docker
|
||||
environment:
|
||||
- LEAN4GAME_GITHUB_USER=${LEAN4GAME_GITHUB_USER}
|
||||
- LEAN4GAME_GITHUB_TOKEN=${LEAN4GAME_GITHUB_TOKEN}
|
||||
ports:
|
||||
- "8080:8080"
|
||||
volumes:
|
||||
- games_data:/app/games
|
||||
|
||||
volumes:
|
||||
games_data:
|
||||
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,43 @@
|
||||
import time
|
||||
|
||||
def measure_proc_stat() -> dict[str, int]:
|
||||
proc_stat_header = open("/proc/stat", "r").readline()
|
||||
proc_stat = proc_stat_header.split(' ')[2:]
|
||||
proc_stat[-1] = proc_stat[-1].removesuffix('\n')
|
||||
proc_stat = list(map(int, proc_stat))
|
||||
|
||||
proc_stat_dict= {'user': proc_stat[0],
|
||||
'nice': proc_stat[1],
|
||||
'system': proc_stat[2],
|
||||
'idle': proc_stat[3],
|
||||
'iowait': proc_stat[4],
|
||||
'irq': proc_stat[5],
|
||||
'softirq': proc_stat[6],
|
||||
'steal': proc_stat[7],
|
||||
'guest': proc_stat[8],
|
||||
'guest_nice': proc_stat[9]}
|
||||
|
||||
return proc_stat_dict
|
||||
|
||||
if __name__ == "__main__":
|
||||
"""
|
||||
Script emulates htop calculation of CPU at the
|
||||
moment of calling.
|
||||
"""
|
||||
prev = measure_proc_stat()
|
||||
prev_idle = prev.get('idle') + prev.get('iowait')
|
||||
prev_non_idle = prev.get('user') + prev.get('nice') + prev.get('system') + prev.get('irq') + prev.get('softirq') + prev.get('steal')
|
||||
prev_total = prev_idle + prev_non_idle
|
||||
|
||||
time.sleep(0.1)
|
||||
|
||||
curr = measure_proc_stat()
|
||||
curr_idle = curr.get('idle') + curr.get('iowait')
|
||||
curr_non_idle = curr.get('user') + curr.get('nice') + curr.get('system') + curr.get('irq') + curr.get('softirq') + curr.get('steal')
|
||||
curr_total = curr_idle + curr_non_idle
|
||||
|
||||
d_total = curr_total - prev_total
|
||||
d_idle = curr_idle - prev_idle
|
||||
|
||||
cpu_usage = ((d_total - d_idle)/d_total)
|
||||
print(cpu_usage)
|
||||
@ -0,0 +1,251 @@
|
||||
import { WebSocketServer } from 'ws';
|
||||
import express from 'express'
|
||||
import path from 'path'
|
||||
import * as cp from 'child_process';
|
||||
import * as url from 'url';
|
||||
import * as rpc from 'vscode-ws-jsonrpc';
|
||||
import * as jsonrpcserver from 'vscode-ws-jsonrpc/server';
|
||||
import os from 'os';
|
||||
import fs from 'fs';
|
||||
import anonymize from 'ip-anonymize';
|
||||
import { importTrigger, importStatus } from './import.mjs'
|
||||
import process from 'process';
|
||||
import { spawn } from 'child_process'
|
||||
// import fs from 'fs'
|
||||
|
||||
/**
|
||||
* Add a game here if the server should keep a queue of pre-loaded games ready at all times.
|
||||
*
|
||||
* IMPORTANT! Tags here need to be lower case!
|
||||
*/
|
||||
const queueLength = {
|
||||
"g/hhu-adam/robo": 2,
|
||||
"g/leanprover-community/nng4": 5,
|
||||
"g/djvelleman/stg4": 2,
|
||||
"g/trequetrum/lean4game-logic": 2,
|
||||
}
|
||||
|
||||
const __filename = url.fileURLToPath(import.meta.url);
|
||||
const __dirname = url.fileURLToPath(new URL('.', import.meta.url));
|
||||
|
||||
const app = express()
|
||||
|
||||
const PORT = process.env.PORT || 8080;
|
||||
|
||||
var router = express.Router();
|
||||
|
||||
router.get('/import/status/:owner/:repo', importStatus)
|
||||
router.get('/import/trigger/:owner/:repo', importTrigger)
|
||||
|
||||
const server = app
|
||||
.use(express.static(path.join(__dirname, '..', 'client', 'dist'))) // TODO: add a dist folder from inside the game
|
||||
.use('/i18n/g/:owner/:repo/:lang/*', (req, res, next) => {
|
||||
const owner = req.params.owner;
|
||||
const repo = req.params.repo
|
||||
const lang = req.params.lang
|
||||
|
||||
const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
|
||||
const log = `${process.cwd()}/logs/game-access.log`
|
||||
const header = "date;anon-ip;game;lang\n"
|
||||
const data = `${new Date()};${ip};${owner}/${repo};${lang}\n`
|
||||
|
||||
fs.writeFile(log, header.concat(data), { flag: 'ax' }, (file_exists) => {
|
||||
if (file_exists) {
|
||||
fs.appendFile(log, data, (err) => {
|
||||
if (err) console.log("Failed to append to log!")
|
||||
});
|
||||
}
|
||||
});
|
||||
|
||||
console.log(`[${new Date()}] ${ip} requested translation for ${owner}/${repo} in ${lang}`)
|
||||
|
||||
const filename = req.params[0];
|
||||
req.url = filename;
|
||||
express.static(path.join(getGameDir(owner,repo),".i18n",lang))(req, res, next);
|
||||
})
|
||||
.use('/data/g/:owner/:repo/*', (req, res, next) => {
|
||||
const owner = req.params.owner;
|
||||
const repo = req.params.repo
|
||||
const filename = req.params[0];
|
||||
req.url = filename;
|
||||
express.static(path.join(getGameDir(owner,repo),".lake","gamedata"))(req, res, next);
|
||||
})
|
||||
.use('/data/stats', (req, res, next) => {
|
||||
const statsProcess = spawn('/bin/bash', [path.join(__dirname, "stats.sh"), process.pid])
|
||||
let outputData = ''
|
||||
let errorData = ''
|
||||
statsProcess.stdout.on('data', (data) => {
|
||||
outputData += data.toString();
|
||||
})
|
||||
statsProcess.stderr.on('data', (data) => {
|
||||
errorData += data.toString();
|
||||
})
|
||||
statsProcess.on('close', (code) => {
|
||||
if (code === 0) {
|
||||
res.send(outputData);
|
||||
} else {
|
||||
res.status(500).send(`Error executing script: ${errorData}`)
|
||||
console.error(`stats.sh exited with code ${code}. Error: ${errorData}`)
|
||||
}
|
||||
})
|
||||
})
|
||||
.use('/', router)
|
||||
.listen(PORT, () => console.log(`Listening on ${PORT}`));
|
||||
|
||||
const wss = new WebSocketServer({ server })
|
||||
|
||||
var socketCounter = 0
|
||||
|
||||
const environment = process.env.NODE_ENV
|
||||
const isDevelopment = environment === 'development'
|
||||
|
||||
/** We keep queues of started Lean Server processes to be ready when a user arrives */
|
||||
const queue = {}
|
||||
|
||||
function getTag(owner, repo) {
|
||||
return `g/${owner.toLowerCase()}/${repo.toLowerCase()}`
|
||||
}
|
||||
|
||||
function getGameDir(owner, repo) {
|
||||
owner = owner.toLowerCase()
|
||||
if (owner == 'local') {
|
||||
if(!isDevelopment) {
|
||||
console.error(`No local games in production mode.`)
|
||||
return ""
|
||||
}
|
||||
} else {
|
||||
if(!fs.existsSync(path.join(__dirname, '..', 'games'))) {
|
||||
console.error(`Did not find the following folder: ${path.join(__dirname, '..', 'games')}`)
|
||||
console.error('Did you already import any games?')
|
||||
return ""
|
||||
}
|
||||
}
|
||||
|
||||
let game_dir = (owner == 'local') ?
|
||||
path.join(__dirname, '..', '..', repo) : // note: here we need `repo` to be case sensitive
|
||||
path.join(__dirname, '..', 'games', `${owner}`, `${repo.toLowerCase()}`)
|
||||
|
||||
if(!fs.existsSync(game_dir)) {
|
||||
console.error(`Game '${game_dir}' does not exist!`)
|
||||
return ""
|
||||
}
|
||||
|
||||
return game_dir;
|
||||
}
|
||||
|
||||
function startServerProcess(owner, repo) {
|
||||
|
||||
let game_dir = getGameDir(owner, repo)
|
||||
if (!game_dir) return;
|
||||
|
||||
let serverProcess
|
||||
if (isDevelopment) {
|
||||
let args = ["--server", game_dir]
|
||||
let binDir = path.join(game_dir, ".lake", "packages", "GameServer", "server", ".lake", "build", "bin")
|
||||
// Note: `cwd` is important to be the `bin` directory as `Watchdog` calls `./gameserver` again
|
||||
if (fs.existsSync(binDir)) {
|
||||
// Try to use the game's own copy of `gameserver`.
|
||||
serverProcess = cp.spawn("./gameserver", args, { cwd: binDir })
|
||||
} else {
|
||||
// If the game is built with `-Klean4game.local` there is no copy in the lake packages.
|
||||
serverProcess = cp.spawn("./gameserver", args,
|
||||
{ cwd: path.join(__dirname, "..", "server", ".lake", "build", "bin") })
|
||||
}
|
||||
} else {
|
||||
serverProcess = cp.spawn("./bubblewrap.sh",
|
||||
[ game_dir, path.join(__dirname, '..')],
|
||||
{ cwd: __dirname })
|
||||
}
|
||||
|
||||
serverProcess.on('error', error =>
|
||||
console.error(`Launching Lean Server failed: ${error}`)
|
||||
)
|
||||
if (serverProcess.stderr !== null) {
|
||||
serverProcess.stderr.on('data', data =>
|
||||
console.error(`Lean Server: ${data}`)
|
||||
)
|
||||
}
|
||||
return serverProcess
|
||||
}
|
||||
|
||||
/** start Lean Server processes to refill the queue */
|
||||
function fillQueue(tag) {
|
||||
while (queue[tag].length < queueLength[tag]) {
|
||||
let serverProcess
|
||||
serverProcess = startServerProcess(tag)
|
||||
if (serverProcess == null) {
|
||||
console.error('serverProcess was undefined/null')
|
||||
return
|
||||
}
|
||||
queue[tag].push(serverProcess)
|
||||
}
|
||||
}
|
||||
|
||||
// // TODO: We disabled queue for now
|
||||
// if (!isDevelopment) { // Don't use queue in development
|
||||
// for (let tag in queueLength) {
|
||||
// queue[tag] = []
|
||||
// fillQueue(tag)
|
||||
// }
|
||||
// }
|
||||
|
||||
const urlRegEx = /^\/websocket\/g\/([\w.-]+)\/([\w.-]+)$/
|
||||
|
||||
wss.addListener("connection", function(ws, req) {
|
||||
const reRes = urlRegEx.exec(req.url)
|
||||
if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; }
|
||||
const owner = reRes[1]
|
||||
const repo = reRes[2]
|
||||
|
||||
const tag = getTag(owner, repo)
|
||||
|
||||
let ps
|
||||
if (!queue[tag] || queue[tag].length == 0) {
|
||||
ps = startServerProcess(owner, repo)
|
||||
} else {
|
||||
console.info('Got process from the queue')
|
||||
ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately
|
||||
fillQueue(tag)
|
||||
}
|
||||
|
||||
if (ps == null) {
|
||||
console.error('server process is undefined/null')
|
||||
return
|
||||
}
|
||||
|
||||
socketCounter += 1;
|
||||
const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
|
||||
|
||||
// TODO (Matvey): extract further information from `req`, for example browser language.
|
||||
console.log(`[${new Date()}] Socket opened - ${ip} - ${owner}/${repo}`)
|
||||
|
||||
const socket = {
|
||||
onMessage: (cb) => { ws.on("message", cb) },
|
||||
onError: (cb) => { ws.on("error", cb) },
|
||||
onClose: (cb) => { ws.on("close", cb) },
|
||||
send: (data, cb) => { ws.send(data,cb) }
|
||||
}
|
||||
const reader = new rpc.WebSocketMessageReader(socket)
|
||||
const writer = new rpc.WebSocketMessageWriter(socket)
|
||||
const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
|
||||
const serverConnection = jsonrpcserver.createProcessStreamConnection(ps)
|
||||
socketConnection.forward(serverConnection, message => {
|
||||
if (isDevelopment) {console.log(`CLIENT: ${JSON.stringify(message)}`)}
|
||||
return message;
|
||||
})
|
||||
serverConnection.forward(socketConnection, message => {
|
||||
if (isDevelopment) {console.log(`SERVER: ${JSON.stringify(message)}`)}
|
||||
return message;
|
||||
});
|
||||
|
||||
console.log(`[${new Date()}] Number of open sockets - ${socketCounter}`)
|
||||
console.log(`[${new Date()}] Free RAM - ${Math.round(os.freemem() / 1024 / 1024)} / ${Math.round(os.totalmem() / 1024 / 1024)} MB`)
|
||||
|
||||
ws.on('close', () => {
|
||||
console.log(`[${new Date()}] Socket closed - ${ip}`)
|
||||
socketCounter -= 1
|
||||
})
|
||||
|
||||
socketConnection.onClose(() => serverConnection.dispose())
|
||||
serverConnection.onClose(() => socketConnection.dispose())
|
||||
})
|
||||
@ -0,0 +1,12 @@
|
||||
#!/usr/bin/env bash
|
||||
|
||||
# Load python interpreter
|
||||
python=/usr/bin/python3
|
||||
# Load python script
|
||||
cpu_usage=relay/cpu_usage.py
|
||||
# Execute python script
|
||||
cpu=$($python $cpu_usage)
|
||||
# Calculate memory usage by computing 1 - %free_memory
|
||||
mem=$(free | sed '2q;d' | awk '{print 1 - ($4/$2)}')
|
||||
|
||||
printf "CPU, MEM\n%f, %f\n" $cpu $mem
|
||||
@ -0,0 +1,34 @@
|
||||
#/bin/bash
|
||||
|
||||
ARTIFACT_ID=$1
|
||||
OWNER=$2
|
||||
REPO=$3
|
||||
|
||||
# mkdir -p games
|
||||
cd games
|
||||
|
||||
# mkdir -p tmp
|
||||
mkdir -p ${OWNER}
|
||||
|
||||
echo "Unpacking ZIP."
|
||||
unzip -o tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip -d tmp/${OWNER}_${REPO}_${ARTIFACT_ID}
|
||||
echo "Unpacking game."
|
||||
|
||||
# exit the npm project to avoid reloading. TODO: Where should we actually save these?
|
||||
|
||||
|
||||
|
||||
echo "Delete old version of the game"
|
||||
rm -rf ${OWNER}/${REPO}
|
||||
mkdir -p ${OWNER}/${REPO}
|
||||
|
||||
for f in tmp/${OWNER}_${REPO}_${ARTIFACT_ID}/* #Should only be one file
|
||||
do
|
||||
echo "Unpacking $f"
|
||||
#tar -xvzf $f -C games/${OWNER}/${REPO}
|
||||
unzip -q -o $f -d ${OWNER}/${REPO}
|
||||
done
|
||||
|
||||
# Delete temporary files
|
||||
rm -f tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip
|
||||
rm -fr tmp/${OWNER}_${REPO}_${ARTIFACT_ID}
|
||||
@ -1,3 +0,0 @@
|
||||
build
|
||||
adam
|
||||
nng
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue