import * as React from 'react'; import { useNavigate, Link } from "react-router-dom"; 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'; const flag = { 'Dutch': '🇳🇱', 'English': '🇬🇧', 'French': '🇫🇷', 'German': '🇩🇪', 'Italian': '🇮🇹', 'Spanish': '🇪🇸', } function GithubIcon({url='https://github.com'}) { return
} function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { let navigate = useNavigate(); const routeChange = () =>{ navigate(gameId); } if (typeof data === 'undefined') { return <> } return
{data.title}
{data.short}
{ data.image ? :
}
{data.long}
Prerequisites {data.prerequisites.join(', ')}
Worlds {data.worlds}
Levels {data.levels}
Language {data.languages.map((lan) => flag[lan]).join(', ')}
} function LandingPage() { const navigate = useNavigate(); const [impressum, setImpressum] = React.useState(false); 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", ] let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile)) return

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.

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

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

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