import * as React from 'react'; import { useNavigate, Link } from "react-router-dom"; import { Trans, useTranslation } from 'react-i18next'; import '@fontsource/roboto/300.css'; import '@fontsource/roboto/400.css'; import '@fontsource/roboto/500.css'; import '@fontsource/roboto/700.css'; import '../css/landing_page.css' import bgImage from '../assets/bg.jpg' import Markdown from './markdown'; import {PrivacyPolicyPopup} from './popup/privacy_policy' import { GameTile, useGetGameInfoQuery } from '../state/api' import path from 'path'; import { PreferencesPopup } from './popup/preferences'; import { ImpressumButton, MenuButton, PreferencesButton } from './app_bar'; import ReactCountryFlag from 'react-country-flag'; import lean4gameConfig from '../config.json' import i18next from 'i18next'; function GithubIcon({url='https://github.com'}) { return
} function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { let { t } = useTranslation() let navigate = useNavigate(); const routeChange = () =>{ navigate(gameId); } if (typeof data === 'undefined') { return <> } return
{t(data.title, { ns: gameId })}
{t(data.short, { ns: gameId })}
{ data.image ? :
}
{t(data.long, { ns: gameId })}
{t("Prerequisites")} {t(data.prerequisites.join(', '), { ns: gameId })}
{t("Worlds")} {data.worlds}
{t("Levels")} {data.levels}
{t("Language")} {data.languages.map((lang) => { let langOpt = lean4gameConfig.languages.find((e) => e.iso == lang) return })}
} function LandingPage() { const navigate = useNavigate(); const [impressumPopup, setImpressumPopup] = React.useState(false); const [preferencesPopup, setPreferencesPopup] = React.useState(false); const [navOpen, setNavOpen] = React.useState(false); const openImpressum = () => setImpressumPopup(true); const closeImpressum = () => setImpressumPopup(false); const toggleImpressum = () => setImpressumPopup(!impressumPopup); const closePreferencesPopup = () => setPreferencesPopup(false); const togglePreferencesPopup = () => setPreferencesPopup(!preferencesPopup); const [usageCPU, setUsageCPU] = React.useState() const [usageMem, setUsageMem] = React.useState() const { t, i18n } = useTranslation() // Load the namespaces of all games // TODO: should `allGames` contain game-ids starting with `g/`? i18next.loadNamespaces(lean4gameConfig.allGames.map(id => `g/${id}`)) let allTiles = lean4gameConfig.allGames.map((gameId) => { let q = useGetGameInfoQuery({game: `g/${gameId}`}) // if (q.isError) { // if (q.error?.originalStatus === 404) { // // Handle 404 error // console.log('File not found'); // } else { // // Suppress additional console.error messages // console.error(q.error); // } // } return q.data?.tile }) /** Parse `games/stats.csv` if present and display server capacity. */ React.useEffect(() => { fetch(`${window.location.origin}/data/stats`) .then(response => {if (response.ok) { return response.text() } else {throw ""}}) .then(data => { // Parse the CSV content const lines = data.split('\n'); const [header, line2] = lines; if (!(header.replace(' ', '').startsWith("CPU,MEM"))) { console.info("Not displaying server stats: received unexpected: ", header) } if (line2) { let values = line2.split(',') setUsageCPU(100 * parseFloat(values[0])); setUsageMem(100 * parseFloat(values[1])); } }).catch(err => { console.info('server stats unavailable') console.debug(err) }) }, []) return

{t("Lean Game Server")}

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

{allTiles.filter(x => x != null).length == 0 ?

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

: lean4gameConfig.allGames.map((id, i) => ( )) }
{ // show server capacity from `games/stats.csv` if present (usageMem >= 0 || usageCPU >= 0 ) &&

{t("Server capacity")}

As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.

{ usageMem >= 0 && <> {t("RAM")}: {usageMem.toFixed(2)} %{t(" used")}.
} { usageCPU >= 0 && <> {t("CPU")}: {usageCPU.toFixed(2)} %{t(" used")}. }

}

{t("Development notes")}

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("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("Funding")}

This server has been developed as part of the project ADAM: Anticipating the Digital Age of Mathematics at Heinrich Heine University Düsseldorf.

} export default LandingPage