remove landing page html file
Alexander Bentkamp
3 years ago
parent
9ba5acef4d
commit
e9a434e26c
@ -1,164 +0,0 @@
|
|||||||
<!DOCTYPE html>
|
|
||||||
<html>
|
|
||||||
<head>
|
|
||||||
<meta charset="UTF-8">
|
|
||||||
<title>Lean Game Server</title>
|
|
||||||
<link rel="stylesheet" href="frontpage.css">
|
|
||||||
|
|
||||||
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.16.7/dist/katex.min.css" integrity="sha384-3UiQGuEI4TTMaFmGIZumfRPtfKQ3trwQE2JgosJxCnGmQpL/lJdjpcHkaaFwHlcI" crossorigin="anonymous">
|
|
||||||
|
|
||||||
<!-- The loading of KaTeX is deferred to speed up page rendering -->
|
|
||||||
<script defer src="https://cdn.jsdelivr.net/npm/katex@0.16.7/dist/katex.min.js" integrity="sha384-G0zcxDFp5LWZtDuRMnBkk3EphCK1lhEf4UEyEM693ka574TZGwo4IWwS6QLzM/2t" crossorigin="anonymous"></script>
|
|
||||||
|
|
||||||
<!-- To automatically render math in text elements, include the auto-render extension: -->
|
|
||||||
<script defer src="https://cdn.jsdelivr.net/npm/katex@0.16.7/dist/contrib/auto-render.min.js" integrity="sha384-+VBxd3r6XgURycqtZ117nYw44OOcIax56Z4dCRWbxyPt0Koah1uHoK0o4+/RRE05" crossorigin="anonymous"
|
|
||||||
onload="renderMathInElement(document.body);"></script>
|
|
||||||
</head>
|
|
||||||
<body>
|
|
||||||
|
|
||||||
<h1>Lean Game Server</h1>
|
|
||||||
|
|
||||||
<p>Welcome to the Lean Game Server where you can find interactive learning
|
|
||||||
games about <a target="_blank" href="https://leanprover-community.github.io/">Lean</a>.<p>
|
|
||||||
|
|
||||||
<div class="game-list">
|
|
||||||
|
|
||||||
<div class="game" onclick="location.href='#/g/hhu-adam/Robo';" style="cursor: pointer;">
|
|
||||||
<div class="wrapper">
|
|
||||||
<div class="title">Formaloversum</div>
|
|
||||||
<div class="short-description">Erkunde das Leansche Universum mit deinem Robo,
|
|
||||||
welcher dir bei der Verständigung mit den Formalosophen zur Seite steht.
|
|
||||||
</div>
|
|
||||||
<img class="image" src="data/formaloversum.png" alt="">
|
|
||||||
<div class="long description">
|
|
||||||
<p>Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet danach
|
|
||||||
verschiedene Bereiche des Bachelorstudiums an.</p>
|
|
||||||
|
|
||||||
<p>(Das Spiel befindet sich noch in der Entstehungsphase.)</p>
|
|
||||||
|
|
||||||
<p>Das Spiel wurde im Rahmen des Projekts <a target="_blank" href="https://hhu-adam.github.io/">ADAM</a>
|
|
||||||
an der HHU in Düsseldorf
|
|
||||||
entwickelt.</p>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
<table class="info">
|
|
||||||
<tr>
|
|
||||||
<td title="consider playing these games first.">Prerequisites</td>
|
|
||||||
<td>-</td>
|
|
||||||
<!-- <td>
|
|
||||||
<ul>
|
|
||||||
<li>-</li>
|
|
||||||
</ul>
|
|
||||||
</td> -->
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td>Worlds</td>
|
|
||||||
<td>?</td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td>Levels</td>
|
|
||||||
<td>?</td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td>Language</td>
|
|
||||||
<td title="in German">🇩🇪</td>
|
|
||||||
</tr>
|
|
||||||
</table>
|
|
||||||
</div>
|
|
||||||
|
|
||||||
<div class="game" onclick="location.href='#/g/hhu-adam/NNG4';" style="cursor: pointer;">
|
|
||||||
<div class="wrapper">
|
|
||||||
<div class="title">Natural Number Game</div>
|
|
||||||
<div class="short-description">
|
|
||||||
The classical introduction game for Lean.
|
|
||||||
</div>
|
|
||||||
<div class="image" src="data/formaloversum.png" alt=""></div>
|
|
||||||
<div class="long description">
|
|
||||||
<p>In this game you recreate the natural numbers
|
|
||||||
\(\mathbb{N}\) from the Peano axioms, learning the basics
|
|
||||||
about theorem proving in Lean.</p>
|
|
||||||
|
|
||||||
<p>This is a good first introduction to Lean!
|
|
||||||
</p>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
<table class="info">
|
|
||||||
<tr>
|
|
||||||
<td title="consider playing these games first.">Prerequisites</td>
|
|
||||||
<td>-</td>
|
|
||||||
<!-- <td>
|
|
||||||
<ul>
|
|
||||||
<li>-</li>
|
|
||||||
</ul>
|
|
||||||
</td> -->
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td>Worlds</td>
|
|
||||||
<td>9</td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td>Levels</td>
|
|
||||||
<td>72</td>
|
|
||||||
</tr>
|
|
||||||
<tr>
|
|
||||||
<td>Language</td>
|
|
||||||
<td title="in English">🇬🇧</td>
|
|
||||||
</tr>
|
|
||||||
</table>
|
|
||||||
</div>
|
|
||||||
</div>
|
|
||||||
|
|
||||||
<h2>Adding new games</h2>
|
|
||||||
<p>
|
|
||||||
If you consider 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 will be an option to load and run games through the server
|
|
||||||
directly by specifying a URL, but this is still in development.
|
|
||||||
</p>
|
|
||||||
<p>
|
|
||||||
To add games to this page, you should get in contact as
|
|
||||||
games will need to be added manually.
|
|
||||||
</p>
|
|
||||||
|
|
||||||
<h2>Impressum</h2>
|
|
||||||
|
|
||||||
<p>
|
|
||||||
When running a game, our server collects metadata
|
|
||||||
(such as IP address, browser, operating system)
|
|
||||||
and the data that the user enters into the editor.
|
|
||||||
|
|
||||||
The data is used to compute the Lean output and display it to the user.
|
|
||||||
The information will be stored as long as the user stays on our
|
|
||||||
website and will be deleted immediately afterwards.
|
|
||||||
We keep logs to improve our software, but the contained
|
|
||||||
data is anonymized.
|
|
||||||
</p>
|
|
||||||
<p>
|
|
||||||
We do not use cookies, but the game progress is stored in the
|
|
||||||
browser as site data. The game progress is not saved on the server;
|
|
||||||
if you delete your browser storage, it will be completely gone.
|
|
||||||
</p>
|
|
||||||
<p>Our server is located in Germany.</p>
|
|
||||||
|
|
||||||
<h3>Contact information</h3>
|
|
||||||
<p>
|
|
||||||
Jon Eugster<br>
|
|
||||||
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br>
|
|
||||||
Universitätsstr. 1<br>
|
|
||||||
40225 Düsseldorf<br>
|
|
||||||
Germany<br>
|
|
||||||
<a target="_blank" href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Contact Details</a>
|
|
||||||
<p>
|
|
||||||
<div class="github-link">
|
|
||||||
<a target="_blank" href="https://github.com/leanprover-community/lean4game"
|
|
||||||
title="View the lean game server on github">
|
|
||||||
<svg height="32" aria-hidden="true" viewBox="0 0 16 16" version="1.1" width="24" data-view-component="true" class="octicon octicon-mark-github v-align-middle">
|
|
||||||
<path 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>
|
|
||||||
</body>
|
|
||||||
</html>
|
|
||||||
Loading…
Reference in New Issue