partial bump to v4.8.0: simple fixes

Fix Bug with Environment Variables for Ports

client/public/locales/es/translation.json

@@ -0,0 +1,94 @@
+ {
+  "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",
+  "<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>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!</1>": "<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. Esperamos afrontar y comprobar mejor esta limitación en el futuro.</p>. <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>",
+  "<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>",
+  "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in 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.",
+  "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"
+}

client/src/config.json

@@ -21,6 +21,11 @@
       "iso": "zh",
       "flag": "CN",
       "name": "中文"
+    },
+    {
+      "iso": "es",
+      "flag": "ES",
+      "name": "Español"
     }
   ]
 }

doc/hints.md

@@ -33,7 +33,7 @@ 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 proofing the goal.
+so that no progress has been made on proving the goal.
 
 ```
 Statement .... := by

server/GameServer/EnvExtensions.lean

@@ -190,7 +190,7 @@ def getCurLayer [MonadError m] : m Layer := do
 def getCurGameId [Monad m] : m Name := do
   match curGameExt.getState (← getEnv) with
   | some game => return game
-  | none => return defaultGameName
+  | none => return (.mkSimple defaultGameName)
 
 /-- Get the current world -/
 def getCurWorldId [MonadError m] : m Name := do
@@ -468,8 +468,8 @@ def getLevel? (levelId : LevelId) : m (Option GameLevel) := do
 
 def getCurGame [Monad m] : m Game := do
   let some game ← getGame? (← getCurGameId)
-    | let game := {name := defaultGameName}
-      insertGame defaultGameName game
+    | let game := {name := (.mkSimple defaultGameName)}
+      insertGame (.mkSimple defaultGameName) game
       return game
   return game
 

server/GameServer/Helpers/PrettyPrinter.lean

@@ -3,7 +3,7 @@ import Lean.PrettyPrinter.Delaborator.Builtins
 import Lean.PrettyPrinter
 import Lean
 
-import Std.Tactic.OpenPrivate
+import Batteries.Tactic.OpenPrivate
 
 namespace GameServer
 

server/GameServer/ImportModules.lean

@@ -1,5 +1,5 @@
 import Lean.Environment
-import Std.Tactic.OpenPrivate
+import Batteries.Tactic.OpenPrivate
 import Lean.Data.Lsp.Communication
 
 open Lean

server/GameServer/Inventory.lean

@@ -124,7 +124,7 @@ partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : Co
     let allowed := GameServer.ALLOWED_KEYWORDS
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
       let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      return {acc with tactics := acc.tactics.insert val}
+      return {acc with tactics := acc.tactics.insert (.mkSimple val)}
     else
       return acc
   | .ident _info _rawVal val _preresolved =>

server/GameServer/RpcHandlers.lean

@@ -17,7 +17,7 @@ def levelIdFromFileName? (initParams : Lsp.InitializeParams) (fileName : String)
   let fileParts := fileName.splitOn "/"
   if fileParts.length == 3 then
     if let (some level, some game) := (fileParts[2]!.toNat?, initParams.rootUri?) then
-      return some {game, world := fileParts[1]!, level := level}
+      return some {game := .mkSimple game, world := .mkSimple fileParts[1]!, level := level}
   return none
 
 def getLevelByFileName? [Monad m] [MonadEnv m] (initParams : Lsp.InitializeParams) (fileName : String) : m (Option GameLevel) := do
@@ -123,7 +123,7 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
           let mut hintFVarsNames : Array Expr := #[]
           for fvar in hintFVars do
             let name₁ ← fvar.fvarId!.getUserName
-            hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨s!"«\{{name₁}}»"⟩
+            hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨.mkSimple s!"«\{{name₁}}»"⟩
 
           let lctx := (← goal.getDecl).lctx -- the player's local context
           if let some bij ← matchDecls hintFVars lctx.getFVars

server/GameServer/Utils.lean

@@ -35,7 +35,7 @@ elab "#show_option" verbose:(ppSpace showOptArg)? id:(ppSpace Parser.rawIdent)?
     | .ofNat val => s!"Nat := {repr val}"
     | .ofInt val => s!"Int := {repr val}"
     | .ofSyntax val => s!"Syntax := {repr val}"
-    if let some val := opts.find name then
+    if let some val := opts.find (.mkSimple name) then
       msg1 := s!"{msg1}  (currently: {val})"
     msg := match verbose with
     | some opt =>

server/lake-manifest.json

@@ -1,13 +1,13 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4.git",
+ [{"url": "https://github.com/leanprover-community/batteries.git",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
-   "name": "std",
+   "rev": "51e6e0d24db9341fb031288c298b7e6b56102253",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
+   "inputRev": "v4.8.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/mhuisi/lean4-cli",
@@ -22,20 +22,20 @@
   {"url": "https://github.com/hhu-adam/lean-i18n.git",
    "type": "git",
    "subDir": null,
-   "rev": "7550f08140c59c9a604bbcc23ab7830c103a3e39",
+   "rev": "5158ce6720d88fa1f53fdb86aea8d515af69571c",
    "name": "i18n",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
+   "inputRev": "v4.8.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "ac07367cbdd57440e6fe78e5be13b41f9cb0f896",
+   "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
+   "inputRev": "v4.8.0",
    "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.toml"}],
  "name": "GameServer",
  "lakeDir": ".lake"}

server/lakefile.lean

@@ -6,7 +6,7 @@ package GameServer
 -- Using this assumes that each dependency has a tag of the form `v4.X.0`.
 def leanVersion : String := s!"v{Lean.versionString}"
 
-require std from git "https://github.com/leanprover/std4.git" @ leanVersion
+require batteries from git "https://github.com/leanprover-community/batteries.git" @ leanVersion
 require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ leanVersion
 
 require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion
@@ -28,4 +28,4 @@ post_update pkg do
   let rootPkg ← getRootPackage
   if rootPkg.name = pkg.name then
     return -- do not run in GameServer itself
-  discard <| runBuild gameserver.build >>= (·.await)
+  discard <| runBuild gameserver.fetch

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0

vite.config.ts

@@ -3,6 +3,9 @@ import react from '@vitejs/plugin-react-swc'
 import { viteStaticCopy } from 'vite-plugin-static-copy'
 import svgr from "vite-plugin-svgr"
 
+const backendPort = process.env.PORT || 8080;
+const clientPort = process.env.CLIENT_PORT || 3000;
+
 // https://vitejs.dev/config/
 export default defineConfig({
   //root: 'client/src',
@@ -32,20 +35,20 @@ export default defineConfig({
     exclude: ['games']
   },
   server: {
-    port: 3000,
+    port: Number(clientPort),
     proxy: {
       '/websocket': {
-        target: 'ws://localhost:8080',
+        target: `ws://localhost:${backendPort}`,
         ws: true
       },
       '/import': {
-        target: 'http://localhost:8080',
+        target: `http://localhost:${backendPort}`,
       },
       '/data': {
-        target: 'http://localhost:8080',
+        target: `http://localhost:${backendPort}`,
       },
       '/i18n': {
-        target: 'http://localhost:8080',
+        target: `http://localhost:${backendPort}`,
       },
     }
   },