diff --git a/client/i18next-scanner.config.cjs b/client/i18next-scanner.config.cjs index de63e15..268e75f 100644 --- a/client/i18next-scanner.config.cjs +++ b/client/i18next-scanner.config.cjs @@ -99,7 +99,7 @@ module.exports = { }, lngs: ['en','de'], ns: [], - defaultLng: 'en-GB', + defaultLng: 'en', defaultNs: 'translation', defaultValue: (lng, ns, key) => { if (lng === 'en') { @@ -139,15 +139,9 @@ module.exports = { 'use strict'; const parser = this.parser; - let count = 0; - parser.parseTransFromString(outputText); parser.parseFuncFromString(outputText); - if (count > 0) { - console.log(`[i18next-scanner] transform: count=${chalk.cyan(count)}, file=${chalk.yellow(JSON.stringify(file.relative))}`); - } - done(); } ), diff --git a/client/public/locales/de/translation.json b/client/public/locales/de/translation.json index 24fb915..3bd4074 100644 --- a/client/public/locales/de/translation.json +++ b/client/public/locales/de/translation.json @@ -38,5 +38,54 @@ "back to games selection": "", "close inventory": "", "show inventory": "", - "World": "" + "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 🎭": "", + "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": "", + "locked": "", + "disabled": "", + "new": "", + "Not unlocked yet": "", + "Not available in this level": "", + "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib": "", + "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.": "", + "

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.

<1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue about any problems you experience!": "", + "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above 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.

Featured games on this page are added manually. Please get in contact and we-ll happily add yours.

": "", + "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics at Heinrich-Heine-Universität in Düsseldorf.": "", + "Prerequisites": "", + "Worlds": "", + "Levels": "", + "Language": "", + "Development notes": "", + "Adding new games": "", + "Funding": "", + "

Do you want to delete your saved progress irreversibly?

(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)

": "", + "Delete Progress?": "", + "Delete": "", + "Download & Delete": "", + "Cancel": "", + "Layout": "", + "Always visible": "", + "Save my settings (in the browser store)": "", + "

Select a JSON file with the saved game progress to load your progress.

<1><0>Warning: This will delete your current game progress! Consider <2>downloading your current progress first!": "", + "Upload Saved Progress": "", + "Load selected file": "" } diff --git a/client/public/locales/en/translation.json b/client/public/locales/en/translation.json index 85cb20f..7ecf0f2 100644 --- a/client/public/locales/en/translation.json +++ b/client/public/locales/en/translation.json @@ -38,5 +38,54 @@ "back to games selection": "back to games selection", "close inventory": "close inventory", "show inventory": "show inventory", - "World": "World" + "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 🎭", + "Retry proof from here": "Retry proof from here", + "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", + "locked": "locked", + "disabled": "disabled", + "new": "new", + "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 (Lean 4) and its mathematical library <5>mathlib": "A repository of learning games for the proof assistant <1>Lean (Lean 4) and its mathematical library <5>mathlib", + "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.": "No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER to open a game directly from a local folder.", + "

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.

<1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue about any problems you experience!": "

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.

<1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue about any problems you experience!", + "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above 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.

Featured games on this page are added manually. Please get in contact and we-ll happily add yours.

": "<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo as a template and read <3>How to Create a Game.<1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above 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.

Featured games on this page are added manually. Please get in contact and we-ll happily add yours.

", + "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics at Heinrich-Heine-Universität in Düsseldorf.": "This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics at Heinrich-Heine-Universität in Düsseldorf.", + "Prerequisites": "Prerequisites", + "Worlds": "Worlds", + "Levels": "Levels", + "Language": "Language", + "Development notes": "Development notes", + "Adding new games": "Adding new games", + "Funding": "Funding", + "

Do you want to delete your saved progress irreversibly?

(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)

": "

Do you want to delete your saved progress irreversibly?

(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)

", + "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)", + "

Select a JSON file with the saved game progress to load your progress.

<1><0>Warning: This will delete your current game progress! Consider <2>downloading your current progress first!": "

Select a JSON file with the saved game progress to load your progress.

<1><0>Warning: This will delete your current game progress! Consider <2>downloading your current progress first!", + "Upload Saved Progress": "Upload Saved Progress", + "Load selected file": "Load selected file" } diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx index b65e12e..2362da9 100644 --- a/client/src/components/app_bar.tsx +++ b/client/src/components/app_bar.tsx @@ -13,13 +13,14 @@ import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress } import { useAppDispatch, useAppSelector } from '../hooks' import { Button } from './button' import { downloadProgress } from './popup/erase' -import { t } from 'i18next' +import { useTranslation } from 'react-i18next' /** navigation buttons for mobile welcome page to switch between intro/tree/inventory. */ function MobileNavButtons({pageNumber, setPageNumber}: { pageNumber: number, setPageNumber: any}) { const gameId = React.useContext(GameIdContext) + const { t } = useTranslation() const dispatch = useAppDispatch() // if `prevText` or `prevIcon` is set, show a button to go back @@ -64,6 +65,7 @@ function MenuButton({navOpen, setNavOpen}) { * for the last level, this button turns into a button going back to the welcome page. */ function NextButton({worldSize, difficulty, completed, setNavOpen}) { + const { t } = useTranslation() const gameId = React.useContext(GameIdContext) const {worldId, levelId} = React.useContext(WorldLevelIdContext) return (levelId < worldSize ? @@ -84,6 +86,7 @@ function NextButton({worldSize, difficulty, completed, setNavOpen}) { * only renders if the current level id is > 0. */ function PreviousButton({setNavOpen}) { + const { t } = useTranslation() const gameId = React.useContext(GameIdContext) const {worldId, levelId} = React.useContext(WorldLevelIdContext) return (levelId > 0 && <> @@ -98,6 +101,7 @@ function PreviousButton({setNavOpen}) { /** button to toggle between editor and typewriter */ function InputModeButton({setNavOpen, isDropdown}) { + const { t } = useTranslation() const {levelId} = React.useContext(WorldLevelIdContext) const {typewriterMode, setTypewriterMode, lockEditorMode} = React.useContext(InputModeContext) @@ -124,6 +128,7 @@ function InputModeButton({setNavOpen, isDropdown}) { * Note: Do not translate the word "Impressum"! German GDPR needs this. */ function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) { + const { t } = useTranslation() return } function GameInfoButton({setNavOpen, toggleInfo}) { + const { t } = useTranslation() return } function DownloadButton ({setNavOpen, gameId, gameProgress}) { + const { t } = useTranslation() return } function UploadButton ({setNavOpen, toggleUploadMenu}) { + const { t } = useTranslation() return @@ -164,6 +174,7 @@ function UploadButton ({setNavOpen, toggleUploadMenu}) { /** button to go back to welcome page */ function HomeButton({isDropdown}) { + const { t } = useTranslation() const gameId = React.useContext(GameIdContext) return @@ -181,6 +193,7 @@ function LandingPageButton() { * only displays a button if `setPageNumber` is set. */ function InventoryButton({pageNumber, setPageNumber}) { + const { t } = useTranslation() return (setPageNumber && } } diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index f4b4b5b..bbd7f29 100644 --- a/client/src/components/infoview/goals.tsx +++ b/client/src/components/infoview/goals.tsx @@ -14,6 +14,7 @@ import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, Interacti import { RpcSessionAtPos } from '@leanprover/infoview/*'; import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; import { DiagnosticSeverity } from 'vscode-languageserver-protocol'; +import { useTranslation } from 'react-i18next'; /** Returns true if `h` is inaccessible according to Lean's default name rendering. */ function isInaccessibleName(h: string): boolean { @@ -134,11 +135,6 @@ interface GoalProps { typewriter: boolean } -interface ProofDisplayProps { - proof: string -} - - /** * Displays the hypotheses, target type and optional case label of a goal according to the * provided `filter`. */ @@ -186,6 +182,7 @@ export const Goal = React.memo((props: GoalProps) => { }) export const MainAssumptions = React.memo((props: GoalProps2) => { + let { t } = useTranslation() const { goals, filter } = props const goal = goals[0] @@ -200,7 +197,7 @@ export const MainAssumptions = React.memo((props: GoalProps2) => { [locs, goal.mvarId]) const goalLi =
-
Goal:
+
{t("Goal") + ":"}
@@ -210,25 +207,26 @@ export const MainAssumptions = React.memo((props: GoalProps2) => { const assumptionHyps = hyps.filter(hyp => hyp.isAssumption) return
-
Current Goal
+
{t("Current Goal")}
{filter.reverse && goalLi} { objectHyps.length > 0 && -
Objects:
+
{t("Objects") + ":"}
{objectHyps.map((h, i) => )}
} { assumptionHyps.length > 0 &&
-
Assumptions:
+
{t("Assumptions") + ":"}
{assumptionHyps.map((h, i) => )}
}
}) export const OtherGoals = React.memo((props: GoalProps2) => { + let { t } = useTranslation() const { goals, filter } = props return <> {goals && goals.length > 1 &&
-
Further Goals
+
{t("Further Goals")}
{goals.slice(1).map((goal, i) =>
@@ -240,25 +238,6 @@ export const OtherGoals = React.memo((props: GoalProps2) => { }) -// TODO: deprecated -export const ProofDisplay = React.memo((props : ProofDisplayProps) => { - const { proof } = props - const steps = proof.match(/.+/g) - return <> - { steps && -
-
Proof history
-
-
- {steps.map((s) => -
{s}
- )} -
-
-
} - -}) - interface GoalsProps { goals: InteractiveGoalsWithHints filter: GoalFilterState diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx index 9189b8d..3ade899 100644 --- a/client/src/components/infoview/info.tsx +++ b/client/src/components/infoview/info.tsx @@ -13,9 +13,10 @@ import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-i import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation' import { AllMessages, lspDiagToInteractive } from './messages' -import { goalsToString, Goal, MainAssumptions, OtherGoals, ProofDisplay } from './goals' +import { goalsToString, Goal, MainAssumptions, OtherGoals } from './goals' import { InteractiveTermGoal, InteractiveGoalsWithHints, InteractiveGoals, ProofState } from './rpc_api' import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from './context' +import { useTranslation } from 'react-i18next' // TODO: All about pinning could probably be removed type InfoKind = 'cursor' | 'pin' @@ -87,6 +88,7 @@ interface InfoDisplayContentProps extends PausableProps { } const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { + let { t } = useTranslation() const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proofString} = props const hasWidget = userWidgets.length > 0 @@ -131,7 +133,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
{ goals && (goals.goals.length > 0 ? - :
No Goals
+ :
{t("No Goals")}
)}
@@ -150,7 +152,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { {' '}or { e.preventDefault(); setPaused(false) }}>resume updating {' '}to see information. : - <>
Loading goal...
)} + <>
{t("Loading goal…")}
)} {/* {goals && goals.goals.length > 1 &&
diff --git a/client/src/components/infoview/infos.tsx b/client/src/components/infoview/infos.tsx index b077150..bf41a68 100644 --- a/client/src/components/infoview/infos.tsx +++ b/client/src/components/infoview/infos.tsx @@ -6,9 +6,11 @@ import { DidChangeTextDocumentParams, DidCloseTextDocumentParams, TextDocumentCo import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; import { DocumentPosition, Keyed, PositionHelpers, useClientNotificationEffect, useClientNotificationState, useEvent, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util'; import { Info, InfoProps } from './info'; +import { useTranslation } from 'react-i18next'; /** Manages and displays pinned infos, as well as info for the current location. */ export function Infos() { + let { t } = useTranslation() const ec = React.useContext(EditorContext); // Update pins when the document changes. In particular, when edits are made @@ -126,6 +128,6 @@ export function Infos() { return
{infoProps.map (ps => )} - {!curPos &&

Click somewhere in the Lean file to enable the infoview.

} + {!curPos &&

{t("Click somewhere in the Lean file to enable the infoview.")}

}
; } diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 3268b72..061ae5f 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -37,6 +37,7 @@ import { store } from '../../state/store'; import { Hints, MoreHelpButton, filterHints } from '../hints'; import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; import { DiagnosticSeverity } from 'vscode-languageclient'; +import { useTranslation } from 'react-i18next'; /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is * always present, or the monaco editor cannot start. @@ -151,6 +152,7 @@ function ExerciseStatement({ data, showLeanStatement = false }) { // TODO: This is only used in `EditorInterface` // while `TypewriterInterface` has this copy-pasted in. export function Main(props: { world: string, level: number, data: LevelInfo}) { + let { t } = useTranslation() const ec = React.useContext(EditorContext); const gameId = React.useContext(GameIdContext) const {worldId, levelId} = React.useContext(WorldLevelIdContext) @@ -228,14 +230,14 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) { // that we want to persist. let ret if (!serverVersion) { - ret =

Waiting for Lean server to start...

+ ret =

{t("Waiting for Lean server to start…")}

} else if (serverStoppedResult) { ret =

{serverStoppedResult.message}

{serverStoppedResult.reason}

} else { ret =
{proof?.completedWithWarnings &&
- {proof?.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"} + {proof?.completed ? t("Level completed! 🎉") : t("Level completed with warnings 🎭")}
} @@ -272,8 +274,8 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele } else { return
{proof?.steps[i].command}
-
} @@ -332,7 +334,7 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele /** The tabs of goals that lean ahs after the command of this step has been processed */ function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: InteractiveGoalsWithHints, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) { - + let { t } = useTranslation() const [selectedGoal, setSelectedGoal] = React.useState(0) if (proofStep.goals.length == 0) { @@ -344,7 +346,7 @@ function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofSte {proofStep.goals.map((goal, i) => ( // TODO: Should not use index as key.
{ onGoalChange(i); setSelectedGoal(i); ev.stopPropagation() }}> - {i ? `Goal ${i + 1}` : "Active Goal"} + {i ? t("Goal") + ` ${i + 1}` : t("Active Goal")}
))}
@@ -389,6 +391,7 @@ export function TypewriterInterfaceWrapper(props: { world: string, level: number /** The interface in command line mode */ export function TypewriterInterface({props}) { + let { t } = useTranslation() const ec = React.useContext(EditorContext) const gameId = React.useContext(GameIdContext) const editor = React.useContext(MonacoEditorContext) @@ -500,8 +503,7 @@ export function TypewriterInterface({props}) {
{crashed ?
-

Crashed! Go to editor mode and fix your proof! - Last server response:

+

{t("Crashed! Go to editor mode and fix your proof! Last server response:")}

{interimDiags.map(diag => { const severityClass = diag.severity ? { [DiagnosticSeverity.Error]: 'error', @@ -512,7 +514,7 @@ export function TypewriterInterface({props}) { return
-

Line {diag.range.start.line}, Character {diag.range.start.character}

+

{t("Line")} {diag.range.start.line}, {t("Character")} {diag.range.start.character}

                   {diag.message}
@@ -579,7 +581,7 @@ export function TypewriterInterface({props}) {
{props.level >= props.worldSize ? :
diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index 7441fff..6eb84cb 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -10,6 +10,7 @@ import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadIn import { selectDifficulty, selectInventory } from '../state/progress'; import { store } from '../state/store'; import { useSelector } from 'react-redux'; +import { useTranslation } from 'react-i18next'; import { t } from 'i18next'; export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=false} : @@ -20,6 +21,7 @@ export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll= setLemmaTab: any, enableAll?: boolean, }) { + const { t } = useTranslation() return (
@@ -29,11 +31,11 @@ export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll= {levelInfo?.tactics && } -

Definitions

+

{t("Definitions")}

{levelInfo?.definitions && } -

Theorems

+

{t("Theorems")}

{levelInfo?.lemmas && } @@ -98,11 +100,11 @@ function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, lev function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, enableAll=false}) { const icon = locked ? : disabled ? : item.st - const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : "" + const className = locked ? t("locked") : disabled ? t("disabled") : newly ? t("new") : "" // Note: This is somewhat a hack as the statement of lemmas comes currently in the form // `Namespace.statement_name (x y : Nat) : some type` - const title = locked ? "Not unlocked yet" : - disabled ? "Not available in this level" : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '') + const title = locked ? t("Not unlocked yet") : + disabled ? t("Not available in this level") : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '') const [copied, setCopied] = useState(false) diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index e71d0f4..a50af9b 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -1,6 +1,6 @@ import * as React from 'react'; import { useNavigate, Link } from "react-router-dom"; -import { useTranslation } from 'react-i18next'; +import { Trans, useTranslation } from 'react-i18next'; import '@fontsource/roboto/300.css'; import '@fontsource/roboto/400.css'; @@ -15,6 +15,8 @@ import {PrivacyPolicyPopup} from './popup/privacy_policy' import { GameTile, useGetGameInfoQuery } from '../state/api' import path from 'path'; +import lean4gameConfig from '../config.json' + const flag = { 'Dutch': '🇳🇱', 'English': '🇬🇧', @@ -36,7 +38,7 @@ function GithubIcon({url='https://github.com'}) { } function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { - + let { t } = useTranslation() let navigate = useNavigate(); const routeChange = () =>{ navigate(gameId); @@ -57,19 +59,19 @@ function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { - + - + - + - + @@ -86,59 +88,7 @@ function LandingPage() { const openImpressum = () => setImpressum(true); const closeImpressum = () => setImpressum(false); - // const [allGames, setAllGames] = React.useState([]) - // const [allTiles, setAllTiles] = React.useState([]) - - // const getTiles=()=>{ - // fetch('featured_games.json', { - // headers : { - // 'Content-Type': 'application/json', - // 'Accept': 'application/json' - // } - // } - // ).then(function(response){ - // return response.json() - // }).then(function(data) { - // setAllGames(data.featured_games) - - // }) - // } - - // React.useEffect(()=>{ - // getTiles() - // },[]) - - // React.useEffect(()=>{ - - // Promise.allSettled( - // allGames.map((gameId) => ( - // fetch(`data/g/${gameId}/game.json`).catch(err => {return undefined}))) - // ).then(responses => - // responses.forEach((result) => console.log(result))) - // // Promise.all(responses.map(res => { - // // if (res.status == "fulfilled") { - // // console.log(res.value.json()) - // // return res.value.json() - // // } else { - // // return undefined - // // } - // // })) - // // ).then(allData => { - // // setAllTiles(allData.map(data => data?.tile)) - // // }) - // },[allGames]) - - // TODO: I would like to read the supported games list form a JSON, - // Then load all these games in - // - let allGames = [ - "leanprover-community/nng4", - "hhu-adam/robo", - "djvelleman/stg4", - "miguelmarco/stg4", - "trequetrum/lean4game-logic", - ] - let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile)) + let allTiles = lean4gameConfig.allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile)) const { t, i18n } = useTranslation() return
@@ -155,18 +105,23 @@ function LandingPage() {

{t("Lean Game Server")}

- A repository of learning games for the - proof assistant Lean (Lean 4) and - its mathematical library mathlib + + A repository of learning games for the + proof assistant Lean (Lean 4) and + its mathematical library mathlib +

{allTiles.length == 0 ? -

No Games loaded. Use http://localhost:3000/#/g/local/FOLDER to open a - game directly from a local folder. +

+ + No Games loaded. Use http://localhost:3000/#/g/local/FOLDER to open a + game directly from a local folder. +

- : allGames.map((id, i) => ( + : lean4gameConfig.allGames.map((id, i) => (
-

Development notes

-

- 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. -

-

- Most aspects of the games and the infrastructure are still in development. Feel free to - file a GitHub Issue about - any problems you experience! -

+

{t("Development notes")}

+ +

+ 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. +

+

+ Most aspects of the games and the infrastructure are still in development. Feel free to + file a GitHub Issue about + any problems you experience! +

+
-

Adding new games

-

- If you are considering writing your own game, you should use - the GameSkeleton Github Repo as - a template and read How to Create a Game. -

-

- You can directly load your games into the server and play it using - the correct URL. The instructions above 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. -

-

- Featured games on this page are added manually. - Please get in contact and we-ll happily add yours. -

+

{t("Adding new games")}

+ +

+ If you are considering writing your own game, you should use + the GameSkeleton Github Repo as + a template and read How to Create a Game. +

+

+ You can directly load your games into the server and play it using + the correct URL. The instructions above 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. +

+

+ Featured games on this page are added manually. + Please get in contact and we-ll happily add yours. +

+
-

Funding

+

{t("Funding")}

- This server has been developed as part of the - project ADAM : Anticipating the Digital Age of Mathematics at - Heinrich-Heine-Universität in Düsseldorf. + + This server has been developed as part of the + project ADAM : Anticipating the Digital Age of Mathematics at + Heinrich-Heine-Universität in Düsseldorf. +

+ {/* Do not translate "Impressum", it's needed for German GDPR */} Impressum {impressum? : null}
diff --git a/client/src/components/popup/erase.tsx b/client/src/components/popup/erase.tsx index b445532..41f8005 100644 --- a/client/src/components/popup/erase.tsx +++ b/client/src/components/popup/erase.tsx @@ -8,6 +8,7 @@ import { useAppDispatch } from '../../hooks' import { deleteProgress, selectProgress } from '../../state/progress' import { downloadFile } from '../world_tree' import { Button } from '../button' +import { Trans, useTranslation } from 'react-i18next' /** download the current progress (i.e. what's saved in the browser store) */ export function downloadProgress(gameId: string, gameProgress: any, ev: React.MouseEvent) { @@ -25,6 +26,7 @@ export function downloadProgress(gameId: string, gameProgress: any, ev: React.Mo * controlled by the containing element. */ export function ErasePopup ({handleClose}) { + let { t } = useTranslation() const gameId = React.useContext(GameIdContext) const gameProgress = useSelector(selectProgress(gameId)) const dispatch = useAppDispatch() @@ -43,17 +45,17 @@ export function ErasePopup ({handleClose}) {
-

Delete Progress?

- -

Do you want to delete your saved progress irreversibly?

-

- (This deletes your proofs and your collected inventory. - Saves from other games are not deleted.) -

- - - - +

{t("Delete Progress?")}

+ +

Do you want to delete your saved progress irreversibly?

+

+ (This deletes your proofs and your collected inventory. + Saves from other games are not deleted.) +

+ + + +
} diff --git a/client/src/components/popup/preferences.tsx b/client/src/components/popup/preferences.tsx index 9b2d270..823e57e 100644 --- a/client/src/components/popup/preferences.tsx +++ b/client/src/components/popup/preferences.tsx @@ -4,18 +4,20 @@ import Markdown from '../markdown' import { Switch, Button, ButtonGroup } from '@mui/material'; import Box from '@mui/material/Box'; import Slider from '@mui/material/Slider'; -import supportedLanguages from './language_config.json' +import lean4gameConfig from '../../config.json' import FormControlLabel from '@mui/material/FormControlLabel'; import { IPreferencesContext } from "../infoview/context" import ReactCountryFlag from 'react-country-flag'; +import { useTranslation } from 'react-i18next'; interface PreferencesPopupProps extends Omit { handleClose: () => void } export function PreferencesPopup({ layout, setLayout, isSavePreferences, language, setIsSavePreferences, handleClose, setLanguage }: PreferencesPopupProps) { + let { t } = useTranslation() const marks = [ { @@ -50,7 +52,7 @@ export function PreferencesPopup({ layout, setLayout, isSavePreferences, languag
-

Language

+

{t("Language")}

} @@ -70,14 +72,14 @@ export function PreferencesPopup({ layout, setLayout, isSavePreferences, languag
-

Layout

+

{t("Layout")}

item.key === layout).value} step={1} marks={marks} @@ -105,7 +107,7 @@ export function PreferencesPopup({ layout, setLayout, isSavePreferences, languag color="primary" /> } - label="Save my settings (in the browser store)" + label={t("Save my settings (in the browser store)")} labelPlacement="end" />
diff --git a/client/src/components/popup/privacy_policy.tsx b/client/src/components/popup/privacy_policy.tsx index e3046b7..f205abb 100644 --- a/client/src/components/popup/privacy_policy.tsx +++ b/client/src/components/popup/privacy_policy.tsx @@ -9,6 +9,8 @@ import * as React from 'react' * * `handleClose` is the function to close it again because it's open/closed state is * controlled by the containing element. + * + * Note: Do not translate the Impressum! */ export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) { return
@@ -57,19 +59,3 @@ export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
} - -export const PrivacyPolicy: React.FC = () => { - const [open, setOpen] = React.useState(false) - const handleOpen = () => setOpen(true) - const handleClose = () => setOpen(false) - return ( - <> -
- -

legal

-

notes

-
- {open ? : null} - - ) -} diff --git a/client/src/components/popup/rules_help.tsx b/client/src/components/popup/rules_help.tsx index ca85386..cb16af5 100644 --- a/client/src/components/popup/rules_help.tsx +++ b/client/src/components/popup/rules_help.tsx @@ -10,7 +10,7 @@ import { Trans, useTranslation } from 'react-i18next' * controlled by the containing element. */ export function RulesHelpPopup ({handleClose}: {handleClose: () => void}) { - const { t, i18n } = useTranslation() + const { t } = useTranslation() return
diff --git a/client/src/components/popup/upload.tsx b/client/src/components/popup/upload.tsx index cfaae8b..0a9d9ec 100644 --- a/client/src/components/popup/upload.tsx +++ b/client/src/components/popup/upload.tsx @@ -8,6 +8,7 @@ import { useAppDispatch } from '../../hooks' import { GameProgressState, loadProgress, selectProgress } from '../../state/progress' import { downloadFile } from '../world_tree' import { Button } from '../button' +import { Trans, useTranslation } from 'react-i18next' /** Pop-up that is displaying the Game Info. * @@ -15,6 +16,8 @@ import { Button } from '../button' * controlled by the containing element. */ export function UploadPopup ({handleClose}) { + let { t } = useTranslation() + const [file, setFile] = React.useState(); const gameId = React.useContext(GameIdContext) const gameProgress = useSelector(selectProgress(gameId)) @@ -54,17 +57,19 @@ export function UploadPopup ({handleClose}) {
-

Upload Saved Progress

- -

Select a JSON file with the saved game progress to load your progress.

+

{t("Upload Saved Progress")}

+ +

Select a JSON file with the saved game progress to load your progress.

-

Warning: This will delete your current game progress! - Consider downloading your current progress first!

+

Warning: This will delete your current game progress! + Consider downloading your current progress first! +

+

- +
} diff --git a/client/src/components/popup/language_config.json b/client/src/config.json similarity index 52% rename from client/src/components/popup/language_config.json rename to client/src/config.json index 5e219dd..638a313 100644 --- a/client/src/components/popup/language_config.json +++ b/client/src/config.json @@ -1,4 +1,12 @@ { + "allGames": [ + "leanprover-community/nng4", + "hhu-adam/robo", + "djvelleman/stg4", + "miguelmarco/stg4", + "trequetrum/lean4game-logic" + ], + "languages": [ { "iso": "en", @@ -11,4 +19,5 @@ "name": "Deutsch" } ] + }
Prerequisites{t("Prerequisites")} {data.prerequisites.join(', ')}
Worlds{t("Worlds")} {data.worlds}
Levels{t("Levels")} {data.levels}
Language{t("Language")} {data.languages.map((lan) => flag[lan]).join(', ')}