landing page
Jon Eugster
3 years ago
parent
a0a3438bee
commit
dd7f1a8e20
@ -0,0 +1,202 @@
|
||||
|
||||
Apache License
|
||||
Version 2.0, January 2004
|
||||
http://www.apache.org/licenses/
|
||||
|
||||
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
|
||||
|
||||
1. Definitions.
|
||||
|
||||
"License" shall mean the terms and conditions for use, reproduction,
|
||||
and distribution as defined by Sections 1 through 9 of this document.
|
||||
|
||||
"Licensor" shall mean the copyright owner or entity authorized by
|
||||
the copyright owner that is granting the License.
|
||||
|
||||
"Legal Entity" shall mean the union of the acting entity and all
|
||||
other entities that control, are controlled by, or are under common
|
||||
control with that entity. For the purposes of this definition,
|
||||
"control" means (i) the power, direct or indirect, to cause the
|
||||
direction or management of such entity, whether by contract or
|
||||
otherwise, or (ii) ownership of fifty percent (50%) or more of the
|
||||
outstanding shares, or (iii) beneficial ownership of such entity.
|
||||
|
||||
"You" (or "Your") shall mean an individual or Legal Entity
|
||||
exercising permissions granted by this License.
|
||||
|
||||
"Source" form shall mean the preferred form for making modifications,
|
||||
including but not limited to software source code, documentation
|
||||
source, and configuration files.
|
||||
|
||||
"Object" form shall mean any form resulting from mechanical
|
||||
transformation or translation of a Source form, including but
|
||||
not limited to compiled object code, generated documentation,
|
||||
and conversions to other media types.
|
||||
|
||||
"Work" shall mean the work of authorship, whether in Source or
|
||||
Object form, made available under the License, as indicated by a
|
||||
copyright notice that is included in or attached to the work
|
||||
(an example is provided in the Appendix below).
|
||||
|
||||
"Derivative Works" shall mean any work, whether in Source or Object
|
||||
form, that is based on (or derived from) the Work and for which the
|
||||
editorial revisions, annotations, elaborations, or other modifications
|
||||
represent, as a whole, an original work of authorship. For the purposes
|
||||
of this License, Derivative Works shall not include works that remain
|
||||
separable from, or merely link (or bind by name) to the interfaces of,
|
||||
the Work and Derivative Works thereof.
|
||||
|
||||
"Contribution" shall mean any work of authorship, including
|
||||
the original version of the Work and any modifications or additions
|
||||
to that Work or Derivative Works thereof, that is intentionally
|
||||
submitted to Licensor for inclusion in the Work by the copyright owner
|
||||
or by an individual or Legal Entity authorized to submit on behalf of
|
||||
the copyright owner. For the purposes of this definition, "submitted"
|
||||
means any form of electronic, verbal, or written communication sent
|
||||
to the Licensor or its representatives, including but not limited to
|
||||
communication on electronic mailing lists, source code control systems,
|
||||
and issue tracking systems that are managed by, or on behalf of, the
|
||||
Licensor for the purpose of discussing and improving the Work, but
|
||||
excluding communication that is conspicuously marked or otherwise
|
||||
designated in writing by the copyright owner as "Not a Contribution."
|
||||
|
||||
"Contributor" shall mean Licensor and any individual or Legal Entity
|
||||
on behalf of whom a Contribution has been received by Licensor and
|
||||
subsequently incorporated within the Work.
|
||||
|
||||
2. Grant of Copyright License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
copyright license to reproduce, prepare Derivative Works of,
|
||||
publicly display, publicly perform, sublicense, and distribute the
|
||||
Work and such Derivative Works in Source or Object form.
|
||||
|
||||
3. Grant of Patent License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
(except as stated in this section) patent license to make, have made,
|
||||
use, offer to sell, sell, import, and otherwise transfer the Work,
|
||||
where such license applies only to those patent claims licensable
|
||||
by such Contributor that are necessarily infringed by their
|
||||
Contribution(s) alone or by combination of their Contribution(s)
|
||||
with the Work to which such Contribution(s) was submitted. If You
|
||||
institute patent litigation against any entity (including a
|
||||
cross-claim or counterclaim in a lawsuit) alleging that the Work
|
||||
or a Contribution incorporated within the Work constitutes direct
|
||||
or contributory patent infringement, then any patent licenses
|
||||
granted to You under this License for that Work shall terminate
|
||||
as of the date such litigation is filed.
|
||||
|
||||
4. Redistribution. You may reproduce and distribute copies of the
|
||||
Work or Derivative Works thereof in any medium, with or without
|
||||
modifications, and in Source or Object form, provided that You
|
||||
meet the following conditions:
|
||||
|
||||
(a) You must give any other recipients of the Work or
|
||||
Derivative Works a copy of this License; and
|
||||
|
||||
(b) You must cause any modified files to carry prominent notices
|
||||
stating that You changed the files; and
|
||||
|
||||
(c) You must retain, in the Source form of any Derivative Works
|
||||
that You distribute, all copyright, patent, trademark, and
|
||||
attribution notices from the Source form of the Work,
|
||||
excluding those notices that do not pertain to any part of
|
||||
the Derivative Works; and
|
||||
|
||||
(d) If the Work includes a "NOTICE" text file as part of its
|
||||
distribution, then any Derivative Works that You distribute must
|
||||
include a readable copy of the attribution notices contained
|
||||
within such NOTICE file, excluding those notices that do not
|
||||
pertain to any part of the Derivative Works, in at least one
|
||||
of the following places: within a NOTICE text file distributed
|
||||
as part of the Derivative Works; within the Source form or
|
||||
documentation, if provided along with the Derivative Works; or,
|
||||
within a display generated by the Derivative Works, if and
|
||||
wherever such third-party notices normally appear. The contents
|
||||
of the NOTICE file are for informational purposes only and
|
||||
do not modify the License. You may add Your own attribution
|
||||
notices within Derivative Works that You distribute, alongside
|
||||
or as an addendum to the NOTICE text from the Work, provided
|
||||
that such additional attribution notices cannot be construed
|
||||
as modifying the License.
|
||||
|
||||
You may add Your own copyright statement to Your modifications and
|
||||
may provide additional or different license terms and conditions
|
||||
for use, reproduction, or distribution of Your modifications, or
|
||||
for any such Derivative Works as a whole, provided Your use,
|
||||
reproduction, and distribution of the Work otherwise complies with
|
||||
the conditions stated in this License.
|
||||
|
||||
5. Submission of Contributions. Unless You explicitly state otherwise,
|
||||
any Contribution intentionally submitted for inclusion in the Work
|
||||
by You to the Licensor shall be under the terms and conditions of
|
||||
this License, without any additional terms or conditions.
|
||||
Notwithstanding the above, nothing herein shall supersede or modify
|
||||
the terms of any separate license agreement you may have executed
|
||||
with Licensor regarding such Contributions.
|
||||
|
||||
6. Trademarks. This License does not grant permission to use the trade
|
||||
names, trademarks, service marks, or product names of the Licensor,
|
||||
except as required for reasonable and customary use in describing the
|
||||
origin of the Work and reproducing the content of the NOTICE file.
|
||||
|
||||
7. Disclaimer of Warranty. Unless required by applicable law or
|
||||
agreed to in writing, Licensor provides the Work (and each
|
||||
Contributor provides its Contributions) on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
|
||||
implied, including, without limitation, any warranties or conditions
|
||||
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
|
||||
PARTICULAR PURPOSE. You are solely responsible for determining the
|
||||
appropriateness of using or redistributing the Work and assume any
|
||||
risks associated with Your exercise of permissions under this License.
|
||||
|
||||
8. Limitation of Liability. In no event and under no legal theory,
|
||||
whether in tort (including negligence), contract, or otherwise,
|
||||
unless required by applicable law (such as deliberate and grossly
|
||||
negligent acts) or agreed to in writing, shall any Contributor be
|
||||
liable to You for damages, including any direct, indirect, special,
|
||||
incidental, or consequential damages of any character arising as a
|
||||
result of this License or out of the use or inability to use the
|
||||
Work (including but not limited to damages for loss of goodwill,
|
||||
work stoppage, computer failure or malfunction, or any and all
|
||||
other commercial damages or losses), even if such Contributor
|
||||
has been advised of the possibility of such damages.
|
||||
|
||||
9. Accepting Warranty or Additional Liability. While redistributing
|
||||
the Work or Derivative Works thereof, You may choose to offer,
|
||||
and charge a fee for, acceptance of support, warranty, indemnity,
|
||||
or other liability obligations and/or rights consistent with this
|
||||
License. However, in accepting such obligations, You may act only
|
||||
on Your own behalf and on Your sole responsibility, not on behalf
|
||||
of any other Contributor, and only if You agree to indemnify,
|
||||
defend, and hold each Contributor harmless for any liability
|
||||
incurred by, or claims asserted against, such Contributor by reason
|
||||
of your accepting any such warranty or additional liability.
|
||||
|
||||
END OF TERMS AND CONDITIONS
|
||||
|
||||
APPENDIX: How to apply the Apache License to your work.
|
||||
|
||||
To apply the Apache License to your work, attach the following
|
||||
boilerplate notice, with the fields enclosed by brackets "[]"
|
||||
replaced with your own identifying information. (Don't include
|
||||
the brackets!) The text should be enclosed in the appropriate
|
||||
comment syntax for the file format. We also recommend that a
|
||||
file or class name and description of purpose be included on the
|
||||
same "printed page" as the copyright notice for easier
|
||||
identification within third-party archives.
|
||||
|
||||
Copyright [yyyy] [name of copyright owner]
|
||||
|
||||
Licensed under the Apache License, Version 2.0 (the "License");
|
||||
you may not use this file except in compliance with the License.
|
||||
You may obtain a copy of the License at
|
||||
|
||||
http://www.apache.org/licenses/LICENSE-2.0
|
||||
|
||||
Unless required by applicable law or agreed to in writing, software
|
||||
distributed under the License is distributed on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
See the License for the specific language governing permissions and
|
||||
limitations under the License.
|
||||
Binary file not shown.
Binary file not shown.
@ -0,0 +1,164 @@
|
||||
<!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='#/game/adam';" 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='#/game/nng';" 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>
|
||||
Binary file not shown.
|
After Width: | Height: | Size: 398 KiB |
@ -0,0 +1,113 @@
|
||||
/* @font-face {
|
||||
font-family: 'Roboto Slab';
|
||||
src: url('data/font/RobotoSlab.woff2') format('woff2');
|
||||
font-weight: normal;
|
||||
font-style: normal;
|
||||
} */
|
||||
|
||||
.landing-page {
|
||||
position: relative;
|
||||
margin: 20px;
|
||||
}
|
||||
|
||||
.short-description p, .info p {
|
||||
margin-block-start: 0;
|
||||
margin-block-end: 0;
|
||||
}
|
||||
|
||||
/* p {
|
||||
margin-top: 10px;
|
||||
margin-bottom: 10px;
|
||||
}
|
||||
|
||||
h1 {
|
||||
margin-top: 20px;
|
||||
margin-bottom: 20px;
|
||||
}
|
||||
|
||||
h2 {
|
||||
margin-top: 40px;
|
||||
margin-bottom: 20px;
|
||||
}
|
||||
|
||||
*/
|
||||
|
||||
.title {
|
||||
font-size: 24px;
|
||||
font-weight: bold;
|
||||
padding-top: 15px;
|
||||
padding-bottom: 5px;
|
||||
}
|
||||
|
||||
.game-list {
|
||||
display: grid;
|
||||
grid-gap: 25px;
|
||||
grid-template-columns: repeat(auto-fit, minmax(300px, 1fr));
|
||||
/* padding-left: 20px; */
|
||||
/* padding-right: 20px; */
|
||||
padding-top: 20px;
|
||||
padding-bottom: 80px;
|
||||
}
|
||||
|
||||
.game {
|
||||
cursor: pointer;
|
||||
border: 1px solid rgb(140, 140, 140);
|
||||
border-radius: 20px;
|
||||
box-shadow: 5px 5px 8px rgb(140, 140, 140);
|
||||
max-width: 500px;
|
||||
display: flex;
|
||||
flex-direction: column;
|
||||
justify-content: space-between;
|
||||
}
|
||||
|
||||
.image {
|
||||
width: 100%;
|
||||
height: 200px;
|
||||
object-fit: cover;
|
||||
}
|
||||
|
||||
div.image {
|
||||
background: rgb(29,0,36);
|
||||
background: linear-gradient(137deg, rgba(97,9,121,1) 0%, rgba(0,212,255,1) 100%);
|
||||
}
|
||||
|
||||
.game .wrapper > :not(.image), .game .info {
|
||||
margin-left: 10px;
|
||||
margin-right: 10px;
|
||||
}
|
||||
|
||||
.short-description {
|
||||
padding-top: 5px;
|
||||
padding-bottom: 5px;
|
||||
}
|
||||
|
||||
.game-stats {
|
||||
display: block;
|
||||
}
|
||||
|
||||
.info {
|
||||
margin-top: 5px;
|
||||
margin-bottom: 15px;
|
||||
width: calc(100% - 20px);
|
||||
border-collapse: collapse;
|
||||
}
|
||||
|
||||
.info tr {
|
||||
border-top: 1px solid rgb(200, 200, 200);
|
||||
border-bottom: 1px solid rgb(200, 200, 200);
|
||||
}
|
||||
|
||||
.info td {
|
||||
padding-top: 5px;
|
||||
padding-bottom: 5px;
|
||||
}
|
||||
|
||||
.info td:nth-child(even) {
|
||||
text-align: right;
|
||||
}
|
||||
|
||||
.github-link {
|
||||
position: absolute;
|
||||
top : 0;
|
||||
right: 0;
|
||||
}
|
||||
@ -0,0 +1,144 @@
|
||||
import * as React from 'react';
|
||||
import { useNavigate } from "react-router-dom";
|
||||
import { Link } from 'react-router-dom';
|
||||
import Markdown from './Markdown';
|
||||
|
||||
import '@fontsource/roboto/300.css';
|
||||
import '@fontsource/roboto/400.css';
|
||||
import '@fontsource/roboto/500.css';
|
||||
import '@fontsource/roboto/700.css';
|
||||
|
||||
import './LandingPage.css'
|
||||
import PrivacyPolicy from './PrivacyPolicy'
|
||||
|
||||
import coverRobo from '../assets/covers/formaloversum.png'
|
||||
|
||||
const flag = {
|
||||
'Dutch': '🇳🇱',
|
||||
'English': '🇬🇧',
|
||||
'French': '🇫🇷',
|
||||
'German': '🇩🇪',
|
||||
'Italian': '🇮🇹',
|
||||
}
|
||||
|
||||
function GithubIcon({url='https://github.com'}) {
|
||||
|
||||
return <div className="github-link">
|
||||
<a target="_blank" href={url}
|
||||
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" className="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>
|
||||
}
|
||||
|
||||
function GameTile({
|
||||
title,
|
||||
gameId,
|
||||
intro, // Catchy intro phrase.
|
||||
image=null,
|
||||
worlds='?',
|
||||
levels='?',
|
||||
prereq='–', // Optional list of games that this game builds on. Use markdown.
|
||||
description, // Longer description. Supports Markdown.
|
||||
language}) {
|
||||
|
||||
let navigate = useNavigate();
|
||||
const routeChange = () =>{
|
||||
let path = `game/${gameId}`;
|
||||
navigate(path);
|
||||
}
|
||||
|
||||
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();
|
||||
|
||||
return <div className="landing-page">
|
||||
|
||||
<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 className="game-list">
|
||||
|
||||
<GameTile
|
||||
title="Formaloversum"
|
||||
gameId="adam"
|
||||
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.)
|
||||
|
||||
Das Spiel wurde im Rahmen des Projekts [ADAM](https://hhu-adam.github.io) an der HHU in Düsseldorf entwickelt."
|
||||
image={coverRobo}
|
||||
language="German"
|
||||
/>
|
||||
|
||||
<GameTile
|
||||
title="Natural Number Game"
|
||||
gameId="nng"
|
||||
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="9"
|
||||
levels="72"
|
||||
language="English"
|
||||
/>
|
||||
</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>
|
||||
|
||||
<GithubIcon url="https://github.com/leanprover-community/lean4game"/>
|
||||
<PrivacyPolicy/>
|
||||
|
||||
</div>
|
||||
|
||||
}
|
||||
|
||||
export default LandingPage
|
||||
@ -0,0 +1,2 @@
|
||||
declare module '*.jpg';
|
||||
declare module '*.png';
|
||||
Loading…
Reference in New Issue