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' 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
{data.title}
{data.short}
{ data.image ? :
}
{data.long}
{t("Prerequisites")} {data.prerequisites.join(', ')}
{t("Worlds")} {data.worlds}
{t("Levels")} {data.levels}
{t("Language")} {data.languages.map((lang) => { let langOpt = lean4gameConfig.languages.find((e) => e.iso == lang) if (langOpt) { return } else 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); let allTiles = lean4gameConfig.allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile)) const { t, i18n } = useTranslation() return

{t("Lean Game Server")}

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.

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

{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!

{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-Universität in Düsseldorf.

} export default LandingPage