lean4game/client/src/components/landing_page.tsx

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 './landing_page.css'
import coverRobo from '../assets/covers/formaloversum.png'
import bgImage from '../assets/bg.jpg'

import Markdown from './markdown';
import {PrivacyPolicyPopup} from './privacy_policy'

const flag = {
  'Dutch': '🇳🇱',
  'English': '🇬🇧',
  'French': '🇫🇷',
  'German': '🇩🇪',
  'Italian': '🇮🇹',
}

function GithubIcon({url='https://github.com'}) {

  return <div className="github-link">
    <a title="view the Lean game server on Github" href={url}>
    <svg height="24" aria-hidden="true" viewBox="0 0 16 16" version="1.1" width="24" className="">
      <path fill="#fff" d="M8 0c4.42 0 8 3.58 8 8a8.013 8.013 0 0 1-5.45 7.59c-.4.08-.55-.17-.55-.38 0-.27.01-1.13.01-2.2 0-.75-.25-1.23-.54-1.48 1.78-.2 3.65-.88 3.65-3.95 0-.88-.31-1.59-.82-2.15.08-.2.36-1.02-.08-2.12 0 0-.67-.22-2.2.82-.64-.18-1.32-.27-2-.27-.68 0-1.36.09-2 .27-1.53-1.03-2.2-.82-2.2-.82-.44 1.1-.16 1.92-.08 2.12-.51.56-.82 1.28-.82 2.15 0 3.06 1.86 3.75 3.64 3.95-.23.2-.44.55-.51 1.07-.46.21-1.61.55-2.33-.66-.15-.24-.6-.83-1.23-.82-.67.01-.27.38.01.53.34.19.73.9.82 1.13.16.45.68 1.31 2.69.94 0 .67.01 1.3.01 1.49 0 .21-.15.45-.55.38A7.995 7.995 0 0 1 0 8c0-4.42 3.58-8 8-8Z"></path>
    </svg>
    </a>
    </div>
}

function GameTile({
  title,
  gameId,
  intro, // Catchy intro phrase.
  image=null,
  worlds='?',
  levels='?',
  prereq='&ndash;', // Optional list of games that this game builds on. Use markdown.
  description, // Longer description. Supports Markdown.
  language}) {

  let navigate = useNavigate();
  const routeChange = () =>{
    navigate(gameId);
  }

  return <div className="game" onClick={routeChange}>
    <div className="wrapper">
      <div className="title">{title}</div>
      <div className="short-description">{intro}
      </div>
      { image ? <img className="image" src={image} alt="" /> : <div className="image"/> }
      <div className="long description"><Markdown>{description}</Markdown></div>
    </div>
    <table className="info">
      <tr>
        <td title="consider playing these games first.">Prerequisites</td>
        <td><Markdown>{prereq}</Markdown></td>
      </tr>
      <tr>
        <td>Worlds</td>
        <td>{worlds}</td>
      </tr>
      <tr>
        <td>Levels</td>
        <td>{levels}</td>
      </tr>
      <tr>
        <td>Language</td>
        <td title={`in ${language}`}>{flag[language]}</td>
      </tr>
    </table>
  </div>

}

function LandingPage() {

  const navigate = useNavigate();

  const [impressum, setImpressum] = React.useState(false);
  const openImpressum = () => setImpressum(true);
  const closeImpressum = () => setImpressum(false);


  return <div className="landing-page">
    <header style={{backgroundImage: `url(${bgImage})`}}>
      <nav>
        <GithubIcon url="https://github.com/leanprover-community/lean4game"/>
      </nav>
      <div id="main-title">
        <h1>Lean Game Server</h1>
        <p>
          A repository of learning games for the
          proof assistant <a target="_blank" href="https://leanprover-community.github.io/">Lean</a> <i>(Lean 4)</i> and
          its mathematical library <a target="_blank" href="https://github.com/leanprover-community/mathlib4">mathlib</a>
        </p>
      </div>
    </header>
    <div className="game-list">

      <GameTile
        title="Natural Number Game"
        gameId="g/hhu-adam/NNG4"
        intro="The classical introduction game for Lean."
        description="In this game you recreate the natural numbers $\mathbb{N}$ from the Peano axioms,
learning the basics about theorem proving in Lean.

This is a good first introduction to Lean!"
        worlds="4"
        levels="30"
        language="English"
        />

      <GameTile
        title="Formaloversum"
        gameId="g/hhu-adam/Robo"
        intro="Erkunde das Leansche Universum mit deinem Robo, welcher dir bei der Verständigung mit den Formalosophen zur Seite steht."
        description="
Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet danach verschiedene Bereiche des Bachelorstudiums an.

(Das Spiel befindet sich noch in der Entstehungsphase.)"
        image={coverRobo}
        language="German"
        />

      <GameTile
        title="NNG (OLD)"
        gameId="g/hhu-adam/nng-old"
        intro="The old version of the NNG copied from lean3."
        description="This version is not maintained and might break at any point. You should play the new version instead"
        worlds="9"
        levels="72"
        language="English"
        />
    </div>
    <section>
      <div className="wrapper">
        <h2>Development notes</h2>
        <p>
          As this server runs lean on our university machines, it has a limited capacity.
          Our current estimate is about 55 copies of the NNG or 25 copies of games importing
          mathlib. We hope to address this limitation in the future.
        </p>
        <p>
          Most aspects of the games and the infrastructure are still in development. Feel free to
          file a <a target="_blank" href="https://github.com/leanprover-community/lean4game/issues">GitHub Issue</a> about
          any problems you experience!
        </p>
      </div>
    </section>
    <section>
      <div className="wrapper">
        <h2>Adding new games</h2>
        <p>
          If you are considering writing your own game, you should use
          the <a target="_blank" href="https://github.com/hhu-adam/NNG4">NNG Github Repo</a> as
          a template.
        </p>
        <p>
          There is an option to load and run your own games direclty on the server,
          instructions are in the NNG repo. Since this is still in development we'd like to
          encourage you to contact us for support creating your own game. The documentation is
          not polished yet.
        </p>
        <p>
          To add games to this main page, you should get in contact as
          games will need to be added manually.
        </p>
      </div>
    </section>
    <section>
      <div className="wrapper">
        <h2>Funding</h2>
        <p>
          This server has been developed as part of the
          project <a target="_blank" href="https://hhu-adam.github.io">ADAM : Anticipating the Digital Age of Mathematics</a> at
          Heinrich-Heine-Universität in Düsseldorf.
        </p>
      </div>
    </section>
    <footer>
      <a className="link" onClick={openImpressum}>Impressum</a>
      {impressum? <PrivacyPolicyPopup handleClose={closeImpressum} />: null}
    </footer>

    {/* <PrivacyPolicy/> */}

  </div>

}

export default LandingPage