Questo è un fork di **lean4game** con supporto per essere self-hostato con Docker.
## Deployment con Docker Compose
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
This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
@ -40,8 +8,7 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular,
* 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)
* Step 8: [How to Publishing a Game](doc/publish_game.md)
## Documentation
@ -69,24 +36,13 @@ not fully written yet.
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.
The project has pimarily 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
"<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!",
"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>",
"<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.",
"<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!",
"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.",
"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>",
"<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.",
저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
"<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>",
"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.":"",
"<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>注意：“解锁”的策略（或定理）由两个因素决定：解决关卡所需的最小策略集合，加上你在其他关卡中解锁的任何策略。这意味着，如果你在某个关卡中解锁了<1>simp</1>，你可以在任何关卡中使用它。</1><p>选项有：</p>",
"Click somewhere in the Lean file to enable the infoview.":"单击 Lean 文件中的某处以启用信息视图。",
"Waiting for Lean server to start…":"等待 Lean 服务器启动中…",
"Level completed! 🎉":"关卡完成！🎉",
"Level completed with warnings 🎭":"关卡完成（带有警告） 🎭",
"Retry proof from here":"从这里重新尝试证明",
"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</1> <i>(Lean 4)</i> 及其数学库 <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> 从本地文件夹打开游戏。",
"<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 Github Repo</1> 作为模板，并参阅 <3>如何创建游戏</3>。</0><1>你可以直接将游戏上传至服务器，并通过正确的 URL 进行游戏。上面的 <1>说明</1> 已详细介绍了如何将游戏加载到服务器的步骤。如果你有任何疑问，请随时联系我们。</1><p>本页上的精选游戏都是手动添加的。如果你想添加你的游戏，请与我们联系，我们非常欢迎。</p>",
"Prerequisites":"前置条件",
"Worlds":"世界",
"Levels":"关卡",
"Language":"语言",
"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":"桌面端",
"Level":"关卡",
"Introduction":"介绍",
"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.":"",
@ -8,7 +8,7 @@ relays messages between the lean server and the client. `index.mjs` is the file
be run, which is done for example using `pm2` or by calling `npm run start_server` or
`npm run production`, see more later.
The latter, "server", is the lean server which has two jobs. For one, it produces the "gameserver"
The latter, "server", is the lean server which has two jobs. For one it produces the "gameserver"
executable which is the lean server that handles the files the player plays on. The second job
is to provide the lean commands which are used when creating a game. These are located in
`Commands.lean`.
@ -27,7 +27,7 @@ saved to lean env-extensions which the lean server has access to after loading t
For games to be run successfully, it is important that the "gameserver" executable inside
the game's `.lake` folder is actually built.
Currently, this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`.
Currently this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`.
(both commands are to be executed in the game's directory!)
## Modifying the server
@ -50,7 +50,7 @@ npm run start_client
npm run production
```
(in two separate terminals) to test the production mode of the server. This way it will only
(in two separate terminals) to test the production modus of the server. This way it will only
* 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.
@ -6,11 +6,11 @@ This tutorial walks you through creating a new game for lean4. It covers from wr
1. Use the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
2. Clone the game repo.
3. Call `lake update -R && lake build` to build the Lean project.
3. Call `lake update && lake exe cache get && lake build` to build the Lean project.
### Running the game
Note that you need to host your game's code on github to publish it online later on. If you only
want to play it locally, you can simply clone the NNG repo and start modifying that one.
Now you can open the game in VSCode (`cd YourGame/` and `code .`), and start modifying it like a regular Lean project. To run the game consult the section "**5. Testing the Game Locally**" below.
## 2. Game.lean
@ -98,7 +98,7 @@ This introduction text is shown when one first enters a world.
1. Use the template above and make sure you import all levels of this world.
1. In `Game.lean` import the world with `import Game.Levels.MyWorld`
Now you created a world with one level and added it🎉 The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently, it shows
Now you created a world with one level and added it🎉 The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently it shows
```text
No world introducing sorry, but required by MyWorld
@ -125,32 +125,26 @@ The player has an inventory with tactics, theorems, and definitions that unlock
```lean
NewTactic induction simp
NewTheorem Nat.zero_mul
NewLemma Nat.zero_mul
NewDefinition Pow
```
**Important:** All commands in this section 6a) expect the `Name` they take as input
to be **fully qualified**. For example `NewTheorem Nat.zero_mul` and not `NewTheorem zero_mul`.
to be **fully qualified**. For example `NewLemma Nat.zero_mul` and not `NewLemma zero_mul`.
#### Doc entries
You'll see a warning about a missing Theorem documentation. You can fix it by adding doc-entries like the following somewhere above it.
You'll see a warning about a missing Lemma documentation. You can fix it by adding doc-entries like the following somewhere above it.
```lean
/--
some description
-/
TheoremDoc Nat.zero_mul as "zero_mul" in "Mul"
/--
some description
-/
LemmaDoc Nat.zero_mul as "zero_mul" in "Mul"
"some description"
TacticDoc simp
"some description"
/--
some description
-/
DefinitionDoc Pow as "^"
"some description"
```
(e.g. you could also create a file `Game/Doc/MyTheorems.lean`, add there your documentation and import it)
@ -162,7 +156,7 @@ If you do not provide any content for the inventory, the game will try to find a
You have a few options to disable inventory items that have been unlocked in previous levels:
have the same syntax as above. The former two disable items for this level, the latter two
@ -170,7 +164,7 @@ disable all items except the ones specified.
#### Theorem Tab
Theorems are sorted into tabs. With `TheoremTab "Mul"` you specify which tab should be open by default in this level.
Theorems are sorted into tabs. with `LemmaTab "Mul"` you specify which tab should be open by default in this level.
#### HiddenTactic
@ -185,16 +179,17 @@ and only `rw` would show up in the inventory.
### 6. b) Statement
The statement is the exercise of the level. The basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax
The statement is the exercise of the level. the basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax
#### Name
You can give your exercise a name: `Statement my_first_exercise (n : Nat) …`. If you do so, it will be added to the inventory and be available in future levels.
You can give your exercise a name: `Statement my_first_exercise (n : Nat) ...`. If you do so, it will be added to the inventory and be available in future levels.
You can but a `Statement` inside namespaces like you would with `theorem`.
#### Doc String / Exercise statement
Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. See [LaTeX in Games](latex.md) for more details on formatting.
Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports Latex.
```lean
/-- The exercise statement in natural language using latex: $\iff$. -/
@ -202,18 +197,25 @@ Statement ...
sorry
```
For more details and features, read [Writing Exercises](writing_exercises.md)
#### Attributes
You can add attributes as you would for a `theorem`. Most notably, you can make your named exercise a `simp` lemma:
```lean
@[simp]
Statement my_simp_lemma ...
```
### 6. c) Proof
The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax.
There are a few extra tactics that help you with structuring the proof:
There are a few extra tactics that help you structuring the proof:
- `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
the one where `Hint` is placed. For more options about hints, see below.
- `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which
helps to set `Hints` in different places. The `Branch` does not affect the main
helps setting`Hints` in different places. The `Branch` does not affect the main
proof and does not need to finish any goals.
- `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template`
will be copied into the editor with all `Hole`s replaced with `sorry`. Note that
@ -228,7 +230,7 @@ Most important for game development are probably the `Hints`.
The hints will be displayed whenever the player's current goal matches the goal the hint is
placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands.
Read [More about Hints](hints.md) for how they work and what the options are.
Read [More about Hints](doc/hints.md) for how they work and what the options are.
### 6. e) Extra: Images
You can add images on any layer of the game (i.e. game/world/level). These will be displayed in your game.
@ -240,15 +242,11 @@ NOTE: At present, only the images for a world are displayed. They appear in the
## 7. Update your game
In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](update_game.md).
In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](doc/update_game.md).
## 8. Add translation
## 8. Publish your game
See [Translating a game](translate.md).
## 9. Publish your game
To publish your game on the official server, see [Publishing a game](publish_game.md)
To publish your game on the official server, see [Publishing a game](doc/publish_game.md)
There are a few more options you can add in `Game.lean` before the `MakeGame` command, which describe the tile that is visible on the server's landing page:
@ -260,26 +258,18 @@ Prerequisites "NNG"
CoverImage "images/cover.png"
```
* `Languages`: Currently only a single language (capital English name). The tile will show a corresponding flag.
* `CaptionShort`: One catchphrase. Appears above the image.
* `CaptionShort`: One catchphrase. Appears above the image.
* `CaptionLong`: 2-4 sentences to describe the game.
* `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text.
* `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens.
## 10. Advanced Topics
## Further Notes
### Escaping
Here are some random further things you should consider designing a new game:
Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you
* Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you
would write `Introduction "some latex here: $\\iff$."` but
`/-- some latex here: $\iff$. -/ Statement ...`
### LaTeX support
LaTeX is rendered using the [KaTeX library](https://katex.org/),
see [Using LaTeX in the Game](latex.md) for details.
### Number Of Levels Limit
A world with more than 16 levels will be displayed with the levels spiraling outwards,
it might be desirable to stay below that bound. Above 22 levels the spiral starts getting out
of control.
* A world with more than 16 levels will be displayed with the levels spiraling outwards,
it might be desirable to stay below that bound. Above 22 levels the spiral starts getting out
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.
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 placing hints outside the sample solution's proof.
## 1. When do hints show?
@ -19,7 +19,7 @@ sample solutions and the entire context from the sample solutions is present in
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
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
@ -32,12 +32,12 @@ Hidden hints are not filtered.
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.
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 proofing the goal.
```
Statement .... := by
Hint "use `rw` or `rewrite`."
Hint "Huse `rw` or `rewrite`."
Branch
rewrite [h]
Hint "now you still need `rfl`"
@ -49,9 +49,6 @@ Statement .... := by
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
```
@ -87,19 +84,6 @@ 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:
```
<imgsrc=\"https://url.com/to/image\"/>
```
Local images can currently only be included with a hack:
You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$`
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.
TODO: Write a doc about latex/markdown options available.
@ -7,13 +7,3 @@ Internally, websocket requests to `ws://localhost:3000/websockets` will be forwa
On the server side, the command will set up a docker image containing the Lean server. The two parts can be built separately using `npm run build_client` and `npm run build_server`.
* `npm run production`: Start the project in production mode. This requires that the build script has been run. It will start a server on the port specified in the `PORT` environment variable or by default on `8080`. You can run on a specific port by running `PORT=80 npm run production`. The server will serve the files in `client/dist` via http and give access to the bubblewrapped Lean server via the web socket protocol.
### Environment Variables
The client and server ports, as well as the default language, can be configured using environment variables:
* `PORT`: Sets the port for the backend server (default: `8080`).
* `CLIENT_PORT`: Sets the port for the client server (default: `3000`).
* `VITE_CLIENT_DEFAULT_LANGUAGE`: Sets the default language for the application (default: `en`).
Ensure these environment variables are set appropriately in your environment to configure the project as needed.
The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
Please also consult the [Troubleshooting Collection](troubleshoot.md), where some known pitfalls are collected.
Please also consult the [Troubleshooting Collection](doc/troubleshoot.md), where some known pitfalls are collected.
There are several options to play a game locally:
@ -33,14 +33,14 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta
* The first start will take a while, ca. 2-15 minutes. After the first
start this should be very quickly.
* Once built, you can open http://localhost:3000 in your browser, which should load the game.
* Once built, you can open http://localhost:3000 in your browser. which should load the game.
3. **Editing Files***(everytime)*:<br/>
After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes.
## Codespaces
You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
Note: You have to wait until npm started properly, which might take a good while.
@ -100,29 +100,6 @@ Run the game:
npm start
```
You should see a message like this:
```bash
[server] > lean4-game@0.1.0 start_server
[server] > (cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec "node ./index.mjs")
[server]
[client]
[client] > lean4-game@0.1.0 start_client
[client] > cross-env NODE_ENV=development vite --host
[client]
[server] [nodemon] 3.0.#
[server] [nodemon] to restart at any time, enter `rs`
[server] (node:#####) [DEP0040] [server] Listening on 8080
```
This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/GameSkeleton. Replace `GameSkeleton` with the folder name of your local game.
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.
- 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".