Compare commits
71 Commits
| Author | SHA1 | Date |
|---|---|---|
|
|
61ed224788 | 1 year ago |
|
|
39137f6d0b | 1 year ago |
|
|
cd5870347b | 1 year ago |
|
|
50bf73a0c5 | 1 year ago |
|
|
39d7af9d3e | 1 year ago |
|
|
49062cc3d5 | 1 year ago |
|
|
f75389e93f | 1 year ago |
|
|
92665b7521 | 1 year ago |
|
|
1845644e86 | 1 year ago |
|
|
341a9ae14b | 1 year ago |
|
|
0895821baa | 1 year ago |
|
|
5b0715629a | 1 year ago |
|
|
39e08194f6 | 1 year ago |
|
|
451dc262b2 | 1 year ago |
|
|
52898d93e7 | 1 year ago |
|
|
5f30572741 | 1 year ago |
|
|
76f2414bd5 | 1 year ago |
|
|
f1f9325c54 | 2 years ago |
|
|
bd3375ada7 | 2 years ago |
|
|
64f34acd7a | 2 years ago |
|
|
ae38ad977a | 2 years ago |
|
|
a191c47b8e | 2 years ago |
|
|
0e58e81875 | 2 years ago |
|
|
f0aa6b58ed | 2 years ago |
|
|
045b1ea3fb | 2 years ago |
|
|
dc6f7b2822 | 2 years ago |
|
|
db5ac7ed15 | 2 years ago |
|
|
6a0e739301 | 2 years ago |
|
|
ed96cf9534 | 2 years ago |
|
|
64670d1579 | 2 years ago |
|
|
25141b9613 | 2 years ago |
|
|
ab9d0d0679 | 2 years ago |
|
|
6dca770dbf | 2 years ago |
|
|
2022fa9a44 | 2 years ago |
|
|
b77afebe0a | 2 years ago |
|
|
4ac38ef7dd | 2 years ago |
|
|
6a8abf41bd | 2 years ago |
|
|
1466a41169 | 2 years ago |
|
|
3cdb9a026b | 2 years ago |
|
|
ebd7268421 | 2 years ago |
|
|
af15982804 | 2 years ago |
|
|
5a404a9a58 | 2 years ago |
|
|
cebea6a6aa | 2 years ago |
|
|
36499c0257 | 2 years ago |
|
|
8c5e47dd7b | 2 years ago |
|
|
a46840d327 | 2 years ago |
|
|
f518efc81c | 2 years ago |
|
|
9b93e3817d | 2 years ago |
|
|
54c1e0dcaf | 2 years ago |
|
|
2c1e69611b | 2 years ago |
|
|
2c22c445b1 | 2 years ago |
|
|
b6b31a06ac | 2 years ago |
|
|
255839fea7 | 2 years ago |
|
|
b961030db2 | 2 years ago |
|
|
c20d807d5c | 2 years ago |
|
|
23c8099401 | 2 years ago |
|
|
6bd9e95db9 | 2 years ago |
|
|
1febc51791 | 2 years ago |
|
|
d53b57a764 | 2 years ago |
|
|
020b4f7803 | 2 years ago |
|
|
0ae099414c | 2 years ago |
|
|
b091ec579b | 2 years ago |
|
|
2a14f48f45 | 2 years ago |
|
|
4ed0753bb0 | 2 years ago |
|
|
6b5fc80896 | 2 years ago |
|
|
e56c7a0670 | 2 years ago |
|
|
5b710da197 | 2 years ago |
|
|
b275bbb94f | 2 years ago |
|
|
29eb90e6c8 | 2 years ago |
|
|
4e9ac54cde | 2 years ago |
|
|
18f21fa324 | 2 years ago |
@ -0,0 +1,8 @@
|
||||
node_modules
|
||||
client/dist
|
||||
games/
|
||||
server/.lake
|
||||
**/.DS_Store
|
||||
logs/
|
||||
relay/prev_cpu_metric
|
||||
test.ecosystem.config.cjs
|
||||
@ -0,0 +1,29 @@
|
||||
FROM node:23-bookworm
|
||||
|
||||
RUN apt update && apt upgrade -y
|
||||
RUN apt install -y bubblewrap
|
||||
|
||||
WORKDIR /app
|
||||
|
||||
# Install elan
|
||||
RUN curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz && \
|
||||
./elan-init -y
|
||||
|
||||
ENV PATH="/root/.elan/bin:${PATH}"
|
||||
|
||||
# Copy package files
|
||||
COPY package.json package-lock.json ./
|
||||
|
||||
# Install dependencies
|
||||
RUN npm install
|
||||
|
||||
# Copy project files
|
||||
COPY . .
|
||||
|
||||
# Build the project
|
||||
RUN npm run build
|
||||
|
||||
EXPOSE 8080
|
||||
|
||||
# Set the entrypoint
|
||||
CMD ["npm", "run", "production"]
|
||||
Binary file not shown.
|
Before Width: | Height: | Size: 607 KiB |
Binary file not shown.
@ -1,93 +0,0 @@
|
||||
Copyright (c) 2020 - 2023, cormullion
|
||||
with Reserved Font Name JuliaMono.
|
||||
|
||||
This Font Software is licensed under the SIL Open Font License, Version 1.1.
|
||||
This license is copied below, and is also available with a FAQ at:
|
||||
http://scripts.sil.org/OFL
|
||||
|
||||
-----------------------------------------------------------
|
||||
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
|
||||
-----------------------------------------------------------
|
||||
|
||||
PREAMBLE
|
||||
The goals of the Open Font License (OFL) are to stimulate worldwide
|
||||
development of collaborative font projects, to support the font creation
|
||||
efforts of academic and linguistic communities, and to provide a free and
|
||||
open framework in which fonts may be shared and improved in partnership
|
||||
with others.
|
||||
|
||||
The OFL allows the licensed fonts to be used, studied, modified and
|
||||
redistributed freely as long as they are not sold by themselves. The
|
||||
fonts, including any derivative works, can be bundled, embedded,
|
||||
redistributed and/or sold with any software provided that any reserved
|
||||
names are not used by derivative works. The fonts and derivatives,
|
||||
however, cannot be released under any other type of license. The
|
||||
requirement for fonts to remain under this license does not apply
|
||||
to any document created using the fonts or their derivatives.
|
||||
|
||||
DEFINITIONS
|
||||
"Font Software" refers to the set of files released by the Copyright
|
||||
Holder(s) under this license and clearly marked as such. This may
|
||||
include source files, build scripts and documentation.
|
||||
|
||||
"Reserved Font Name" refers to any names specified as such after the
|
||||
copyright statement(s).
|
||||
|
||||
"Original Version" refers to the collection of Font Software components as
|
||||
distributed by the Copyright Holder(s).
|
||||
|
||||
"Modified Version" refers to any derivative made by adding to, deleting,
|
||||
or substituting -- in part or in whole -- any of the components of the
|
||||
Original Version, by changing formats or by porting the Font Software to a
|
||||
new environment.
|
||||
|
||||
"Author" refers to any designer, engineer, programmer, technical
|
||||
writer or other person who contributed to the Font Software.
|
||||
|
||||
PERMISSION & CONDITIONS
|
||||
Permission is hereby granted, free of charge, to any person obtaining
|
||||
a copy of the Font Software, to use, study, copy, merge, embed, modify,
|
||||
redistribute, and sell modified and unmodified copies of the Font
|
||||
Software, subject to the following conditions:
|
||||
|
||||
1) Neither the Font Software nor any of its individual components,
|
||||
in Original or Modified Versions, may be sold by itself.
|
||||
|
||||
2) Original or Modified Versions of the Font Software may be bundled,
|
||||
redistributed and/or sold with any software, provided that each copy
|
||||
contains the above copyright notice and this license. These can be
|
||||
included either as stand-alone text files, human-readable headers or
|
||||
in the appropriate machine-readable metadata fields within text or
|
||||
binary files as long as those fields can be easily viewed by the user.
|
||||
|
||||
3) No Modified Version of the Font Software may use the Reserved Font
|
||||
Name(s) unless explicit written permission is granted by the corresponding
|
||||
Copyright Holder. This restriction only applies to the primary font name as
|
||||
presented to the users.
|
||||
|
||||
4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
|
||||
Software shall not be used to promote, endorse or advertise any
|
||||
Modified Version, except to acknowledge the contribution(s) of the
|
||||
Copyright Holder(s) and the Author(s) or with their explicit written
|
||||
permission.
|
||||
|
||||
5) The Font Software, modified or unmodified, in part or in whole,
|
||||
must be distributed entirely under this license, and must not be
|
||||
distributed under any other license. The requirement for fonts to
|
||||
remain under this license does not apply to any document created
|
||||
using the Font Software.
|
||||
|
||||
TERMINATION
|
||||
This license becomes null and void if any of the above conditions are
|
||||
not met.
|
||||
|
||||
DISCLAIMER
|
||||
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
|
||||
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
|
||||
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
|
||||
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
|
||||
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
|
||||
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
|
||||
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
|
||||
OTHER DEALINGS IN THE FONT SOFTWARE.
|
||||
@ -1,93 +0,0 @@
|
||||
Copyright 2021 Google Inc. All Rights Reserved.
|
||||
|
||||
This Font Software is licensed under the SIL Open Font License, Version 1.1.
|
||||
This license is copied below, and is also available with a FAQ at:
|
||||
https://openfontlicense.org
|
||||
|
||||
|
||||
-----------------------------------------------------------
|
||||
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
|
||||
-----------------------------------------------------------
|
||||
|
||||
PREAMBLE
|
||||
The goals of the Open Font License (OFL) are to stimulate worldwide
|
||||
development of collaborative font projects, to support the font creation
|
||||
efforts of academic and linguistic communities, and to provide a free and
|
||||
open framework in which fonts may be shared and improved in partnership
|
||||
with others.
|
||||
|
||||
The OFL allows the licensed fonts to be used, studied, modified and
|
||||
redistributed freely as long as they are not sold by themselves. The
|
||||
fonts, including any derivative works, can be bundled, embedded,
|
||||
redistributed and/or sold with any software provided that any reserved
|
||||
names are not used by derivative works. The fonts and derivatives,
|
||||
however, cannot be released under any other type of license. The
|
||||
requirement for fonts to remain under this license does not apply
|
||||
to any document created using the fonts or their derivatives.
|
||||
|
||||
DEFINITIONS
|
||||
"Font Software" refers to the set of files released by the Copyright
|
||||
Holder(s) under this license and clearly marked as such. This may
|
||||
include source files, build scripts and documentation.
|
||||
|
||||
"Reserved Font Name" refers to any names specified as such after the
|
||||
copyright statement(s).
|
||||
|
||||
"Original Version" refers to the collection of Font Software components as
|
||||
distributed by the Copyright Holder(s).
|
||||
|
||||
"Modified Version" refers to any derivative made by adding to, deleting,
|
||||
or substituting -- in part or in whole -- any of the components of the
|
||||
Original Version, by changing formats or by porting the Font Software to a
|
||||
new environment.
|
||||
|
||||
"Author" refers to any designer, engineer, programmer, technical
|
||||
writer or other person who contributed to the Font Software.
|
||||
|
||||
PERMISSION & CONDITIONS
|
||||
Permission is hereby granted, free of charge, to any person obtaining
|
||||
a copy of the Font Software, to use, study, copy, merge, embed, modify,
|
||||
redistribute, and sell modified and unmodified copies of the Font
|
||||
Software, subject to the following conditions:
|
||||
|
||||
1) Neither the Font Software nor any of its individual components,
|
||||
in Original or Modified Versions, may be sold by itself.
|
||||
|
||||
2) Original or Modified Versions of the Font Software may be bundled,
|
||||
redistributed and/or sold with any software, provided that each copy
|
||||
contains the above copyright notice and this license. These can be
|
||||
included either as stand-alone text files, human-readable headers or
|
||||
in the appropriate machine-readable metadata fields within text or
|
||||
binary files as long as those fields can be easily viewed by the user.
|
||||
|
||||
3) No Modified Version of the Font Software may use the Reserved Font
|
||||
Name(s) unless explicit written permission is granted by the corresponding
|
||||
Copyright Holder. This restriction only applies to the primary font name as
|
||||
presented to the users.
|
||||
|
||||
4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
|
||||
Software shall not be used to promote, endorse or advertise any
|
||||
Modified Version, except to acknowledge the contribution(s) of the
|
||||
Copyright Holder(s) and the Author(s) or with their explicit written
|
||||
permission.
|
||||
|
||||
5) The Font Software, modified or unmodified, in part or in whole,
|
||||
must be distributed entirely under this license, and must not be
|
||||
distributed under any other license. The requirement for fonts to
|
||||
remain under this license does not apply to any document created
|
||||
using the Font Software.
|
||||
|
||||
TERMINATION
|
||||
This license becomes null and void if any of the above conditions are
|
||||
not met.
|
||||
|
||||
DISCLAIMER
|
||||
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
|
||||
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
|
||||
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
|
||||
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
|
||||
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
|
||||
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
|
||||
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
|
||||
OTHER DEALINGS IN THE FONT SOFTWARE.
|
||||
@ -1,202 +0,0 @@
|
||||
|
||||
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.
@ -1,94 +1,99 @@
|
||||
{
|
||||
"Tactics": "Taktiken",
|
||||
"Lean Game Server": "Lean-Spielserver",
|
||||
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>Die Spielregeln bestimmen ob es erlaubt ist, Levels zu überspringen und ob das Spiel überprüft welche Taktiken und Theoreme freigeschaltet sind und nur diese im Beweis akzeptiert.</p><1>Bemerkung: \"Freigeschaltete\" Taktiken (und Theoreme) werden durch zwei Faktoren bestimmt: The Menge der Taktiken die minimal notwendig sind um den Level zu lösen und dazu die Menge aller Taktiken, die in einem anderen Level freigeschaltet wurden. Das bedeutet wenn <1>simp</1> in einem Level freigeschaltet wird, kann diese Taktik danach in jeglichen Levels verwendet werden.",
|
||||
"Lean Game Server": "Lean-Lern-Spiel-Server",
|
||||
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>Die Spielregeln bestimmen ob es erlaubt ist, Levels zu überspringen und ob das Spiel überprüft welche Taktiken und Theoreme freigeschaltet sind und nur diese im Beweis akzeptiert.</p><1>Bemerkung: \"Freigeschaltete\" Taktiken (und Theoreme) werden durch zwei Faktoren bestimmt: The Menge der Taktiken die minimal notwending sind um den Level zu lösen und dazu die Menge aller Taktiken, die in einem anderen Level freigeschaltet wurden. Das bedeutet wenn <1>simp</1> in einem Level freigeschaltet wird, kann diese Taktik danach in jeglichen Levels verwendet werden.",
|
||||
"Game Rules": "Spielregeln",
|
||||
"levels": "Levels",
|
||||
"levels": "Level",
|
||||
"tactics": "Taktiken",
|
||||
"regular": "regulär",
|
||||
"relaxed": "relaxed",
|
||||
"none": "keine",
|
||||
"Rules": "Regeln",
|
||||
"Intro": "Einführung",
|
||||
"Intro": "Prolog",
|
||||
"Game Introduction": "Prolog",
|
||||
"World selection": "Übersicht",
|
||||
"Start": "Start",
|
||||
"Inventory": "Inventar",
|
||||
"next level": "nächstes Level",
|
||||
"Next": "Weiter",
|
||||
"back to world selection": "Zurück zur Übersicht",
|
||||
"Leave World": "Welt verlassen",
|
||||
"previous level": "voheriges Level",
|
||||
"Previous": "Zurück",
|
||||
"Editor mode is enforced!": "Editor kann nicht verlassen werden!",
|
||||
"Editor mode": "Editor",
|
||||
"Typewriter mode": "Schreibmaschine",
|
||||
"information, Impressum, privacy policy": "Informationen, Impressum, Privacy Policy",
|
||||
"Preferences": "Einstellungen",
|
||||
"Game Info & Credits": "Spielinfo & Credits",
|
||||
"Game Info": "Spielinfo",
|
||||
"Clear Progress": "Spielstand löschen",
|
||||
"Erase": "Löschen",
|
||||
"Download Progress": "Spielstand herunterladen",
|
||||
"Download": "Herunterladen",
|
||||
"Load Progress from JSON": "Spielstand aus JSON laden",
|
||||
"Upload": "Laden",
|
||||
"Home": "Home",
|
||||
"back to games selection": "Zurück zur Spielauswahl",
|
||||
"close inventory": "Inventar schließen",
|
||||
"show inventory": "Inventar öffnen",
|
||||
"World": "Welt",
|
||||
"Show more help!": "Mehr Hilfe",
|
||||
"Goal": "Goal",
|
||||
"Current Goal": "Aktuelles Goal",
|
||||
"Goal": "Beweisziel",
|
||||
"Current Goal": "Aktuelles Beweisziel",
|
||||
"Objects": "Objekte",
|
||||
"Assumptions": "Annahmen",
|
||||
"Further Goals": "Weitere Goals",
|
||||
"No Goals": "Keine Goals",
|
||||
"Loading goal…": "Goal wird geladen…",
|
||||
"Further Goals": "Weitere Ziele",
|
||||
"No Goals": "Keine Beweisziele",
|
||||
"Loading goal…": "Beweisziel wird geladen…",
|
||||
"Click somewhere in the Lean file to enable the infoview.": "Ein Klick in den Lean-Code aktiviert den Infoview.",
|
||||
"Waiting for Lean server to start…": "Warte auf das Starten des Lean-Servers…",
|
||||
"Waiting for Lean server to start…": "Warte auf den Lean-Server …",
|
||||
"Level completed! 🎉": "Level gelöst! 🎉",
|
||||
"Level completed with warnings 🎭": "Level mit Warnungen abgeschlossen 🎭",
|
||||
"Active Goal": "Aktuelles Goal",
|
||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "",
|
||||
"Active Goal": "Aktuelles Ziel",
|
||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "Abgestürzt! Wechsle in den Editor-Modus, um deinen Beweis zu repariaeren. Letzte Meldung vom Server:",
|
||||
"Line": "Zeile",
|
||||
"Character": "Charakter",
|
||||
"Loading messages…": "",
|
||||
"Loading messages…": "Lade Meldungen …",
|
||||
"Execute": "Ausführen",
|
||||
"Definitions": "Definitionen",
|
||||
"Theorems": "Theoreme",
|
||||
"Not unlocked yet": "Noch nicht verfügbar",
|
||||
"Not available in this level": "In diesem Level nicht verfügbar",
|
||||
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Eine Sammlung von Lernspielen für den Beweisassistenten <1>Lean</1> <i>(Lean 4)</i> und dessen mathematische Bibliothek <5>mathlib</5>",
|
||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "Kein Spiel geladen. öffne <1>http://localhost:3000/#/g/local/FOLDER</1> um ein Spiel direkt von einem lokalen Ordner zu laden.",
|
||||
"<p>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.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "",
|
||||
"This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "",
|
||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "Kein Spiel geladen. Öffne <1>http://localhost:3000/#/g/local/FOLDER</1> um ein Spiel direkt aus einem lokalen Ordner zu laden.",
|
||||
"Prerequisites": "Voraussetzungen",
|
||||
"Worlds": "Welten",
|
||||
"Levels": "Levels",
|
||||
"Language": "Sprachen",
|
||||
"Development notes": "Entwicklungshinweis",
|
||||
"Levels": "Level",
|
||||
"Language": "Sprache",
|
||||
"Development notes": "Entwicklungsstand",
|
||||
"Adding new games": "Neue Spiele hinzufügen",
|
||||
"Funding": "Finanzierung",
|
||||
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>Soll der Spielstand unwiderruflich gelöscht werden?</p><p>(Dies löscht sämtliche Beweise und das gesammelte Inventar. Spielstände anderer Spiele werden nicht gelöscht.)</p>",
|
||||
"Delete Progress?": "Spielstand löschen?",
|
||||
"Delete": "Löschen",
|
||||
"Download & Delete": "Herunterladen & Löschen",
|
||||
"Download & Delete": "Herunterladen & löschen",
|
||||
"Cancel": "Abbrechen",
|
||||
"Layout": "Seitenlayout",
|
||||
"Always visible": "Immer sichtbar",
|
||||
"Save my settings (in the browser store)": "Einstellungen im Browser speichern.",
|
||||
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>Wähle eine JSON-Datei mit dem Spielstand um diesen zu laden.</p><1><0>Achtung:</0> Diese Aktion überschreibt den aktuellen Spielstand! Es wird empfohlen zuerst den <2>aktuellen Spielstand herunterzuladen</2>!</1>",
|
||||
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>Wähle eine JSON-Datei mit einem Spielstand, um diesen zu laden.</p><1><0>Achtung:</0> Deraktuelle Spielstand wird dabei überschrieben! Wenn du noch einmal zum aktuellen Spielstand zurückkehren möchtest, solltest du zunächst den <2>aktuellen Spielstand herunterladen</2>!</1>",
|
||||
"Upload Saved Progress": "Spielstand hochladen",
|
||||
"Load selected file": "Ausgewählte Datei hochladen",
|
||||
"Mobile": "Mobil",
|
||||
"Auto": "Auto",
|
||||
"Desktop": "Desktop",
|
||||
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "",
|
||||
"Level": "",
|
||||
"Introduction": "Einführung",
|
||||
"Retry proof from here": "Ab hier erneut versuchen",
|
||||
"Retry": "",
|
||||
"Failed command": "Befehl fehlgeschlagen",
|
||||
"view the Lean game server on Github": "Lean game Server auf Github ansehen",
|
||||
"Theorem": "Theorem",
|
||||
"Impressum": "Impressum",
|
||||
"Privacy Policy": "Datenschutzerklärung",
|
||||
"<0>Impressum</0><1><strong>Contact:</strong><br/>Marcus Zibrowius, Jon Eugster<br/>Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br/>Universitätsstr. 1<br/>40225 Düsseldorf<br/>Germany<br/>+49 211 81-14690<br/><14>Contact Details</14></1><2><strong>Legal form:</strong><br/>The Heinrich Heine University Düsseldorf is a corporation under public law. It is legally represented by the Rector Prof. Dr. Anja Steinbeck. The responsible supervisory authority is the Ministry of Culture and Science of North Rhine-Westphalia, Völklinger Straße 49, 40221 Düsseldorf.</2><3><strong>VAT identification number:</strong><br/>according to §27a Sales Tax Act<br/>DE 811222416</3><4><0>Impressum HHU</0></4>": "<0>Impressum</0><1><strong>Kontakt:</strong><br/>Marcus Zibrowius, Jon Eugster<br/>Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br/>Universitätsstr. 1<br/>40225 Düsseldorf<br/>Deutschland<br/>+49 211 81-14690<br/><14>Kontaktinformationen</14></1><2><strong>Rechtsform:</strong><br />Die Heinrich-Heine Universität Düsseldorf ist eine Körperschaft des Öffentlichen Rechts. Sie wird durch die Rektorin Prof. Dr. Anja Steinbeck gesetzlich vertreten. Zuständige Aufsichtsbehörde ist das Ministerium für Kultur und Wissenschaft des Landes Nordrhein-Westfalen, Völklinger Straße 49, 40221 Düsseldorf.</2><3><strong>Umsatzsteuer-Identifikationsnummer:</strong><br />gemäß §27a Umsatzsteuergesetz<br />DE 811222416</3><4><0>Impressum der HHU</0></4>",
|
||||
"<0>Progress saving</0><1>The game stores your progress in your local browser storage. If you delete it, your progress will be lost!<br/>Warning: In most browsers, deleting cookies will also clear the local storage (or \"local site data\"). Make sure to download your game progress first!</1><2>Development</2><3>The game engine has been created by <strong>Alexander Bentkamp</strong>, <strong>Jon Eugster</strong>. On a prototype by <strong>Patrick Massot</strong>.</3><4>The source code of this Lean game engine is <1>available on Github</1>. If you experience any problems, please file an <3>Issue on Github</3> or get directly in contact.</4><5>Funding</5><6>The game engine has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität Düsseldorf. It is funded by the <i>Stiftung Innovation in der Hochschullehre</i> as part of project <i>Freiraum 2022</i>.</6>": "<0>Spielstandspeicherung</0><1>Das Spiel speichert den Spielstand im lokalen Browserspeicher. Wird dieser gelöscht, ist der Spielstand nicht wiederherstellbar!<br/>Achtung: In üblichen Browsern bewirkt ein löschen von Cookies auch ein löschen des lokalen Browserspeichers (z.B. \"local site data\"). Der Spielstand sollte vorgehend heruntergeladen werden!</1><2>Entwicklung</2><3>Der Spieleserver wurde entwickelt von <strong>Alexander Bentkamp</strong>, <strong>Jon Eugster</strong>. Basierend auf einem Prototyp von <strong>Patrick Massot</strong>.</3><4>Der Sourcecode dieses Lean-Game-Engine ist <1>auf Github verfügbar</1>. Bei Problemen, bitte einen <3>Github-Issue</3> ausfüllen oder direkt mit uns Kontakt aufnehmen.</4><5>Funding</5><6>Dieser Spielserver wurde im Rahmen des Projekts <1>ADAM: Anticipating the Digital Age of Mathematics</1> an der Heinrich-Heine-Universität Düsseldorf entwickelt. Es wird finanziell durch das Projekt <i>Freiraum 2022</i> der <i>Stiftung Innovation in der Hochschullehre</i> unterstützt.</6>",
|
||||
"<0>Privacy Policy</0><p>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 your game progress is stored in the browser as site data. Your game progress is not saved on the server; if you delete your browser storage, it is completely gone.</p><p>Our server is located in Germany.</p><4><strong>Contact:</strong><br/>Marcus Zibrowius, Jon Eugster<br/>Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br/>Universitätsstr. 1<br/>40225 Düsseldorf<br/>Germany<br/>+49 211 81-14690<br/><14>Contact Details</14></4>": "<0>Datenschutzerklärung</0><p>Unser Server verarbeitet Benutzer-Metadaten (zum Beispiel IP-Addresse, Browser-Version, Betriebssystem) sowie die Benutzereingaben in den Editor. Diese Daten werden verwendet um die Lean-Ausgabe zu berechnen und dem Benutzer darzustellen. Die Informationen werden nur gespeichert, solange der Benutzer auf unserer Webseite bleibt und anschliessend sofort gelöscht. Wir führen Log-Dateien um die Software zu verbessern, aber die enthaltenen Daten sind anonymisiert.</p><p>Wir verwenden keine Cookies, aber der Spielstand wird im Browser als \"Site Data\" gespeichert. Der Spielstand wird nicht auf dem Server gespeichert; wird er lokal gelöscht, kann er nicht wiederhergestellt werden.</p><p>Unser Server ist in Deutschland stationiert.</p><4><strong>Kontakt:</strong><br/>Markus Zibrowius, Jon Eugster<br/>Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br/>Universitätsstr. 1<br/>40225 Düsseldorf<br/>Deutschland<br/>+49 211 81-14690<br/><14>Kontaktdetails</14></4>",
|
||||
"home": "",
|
||||
"close language menu": "Sprachmenü schließen",
|
||||
"open language menu": "Sprachmenü öffnen",
|
||||
"close menu": "Menü schließen",
|
||||
"open menu": "Menü öffnen",
|
||||
"Editor Mode": "",
|
||||
"Typewriter Mode": ""
|
||||
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>Für alle, die selbst Spiel entwickeln möchten, gibt es ein <1>GameSkeleton Github Repo</1> als Vorlage und die Anleitung <3>How to Create a Game</3>.</0><1>Die <1>Anleitung</1> erklärt auch, wie ein solches Spiel mittels einer passenden URL auf den Sever geladen und gespiel werden kann. Fragen dazu beantworten wir gern.</1><p>Als Kacheln sichtbar ist auf dieser Seite nur eine kuratierte Auswahl an existierenden Spielen. Wir erweitern diese Auswahl auf Anfrage sehr gerne.</p>",
|
||||
"Level": "Level",
|
||||
"Introduction": "Prolog",
|
||||
"Retry proof from here": "Ab hier neu ansetzen",
|
||||
"Retry": "Noch einmal",
|
||||
"Failed command": "Gescheiterter Befehl",
|
||||
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "Diese Server läuft auf universitäter Infrastruktur mit begrenzten Kapazitäten. Wir schätzen, dass die Belastungsgrenze bei rund 70 gleichzeitig laufenden Spielen besteht.",
|
||||
"<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "Der Spieleserver und die alle Spiele befinden sich in fortlaufender Entwicklung. Wir bitten darum, Fehler und Ungereimtheiten als <1>GitHub Issue</1> zu melden.",
|
||||
"This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "Die Lean-Spiele-Software und dieser Spiele-Server werden als Teils der Projekts <1>ADAM: Anticipating the Digital Age of Mathematics</1> an der Heinrich-Heine-Universität Düsseldorf entwickelt.",
|
||||
"Server capacity": "Server-Auslastung",
|
||||
"RAM": "RAM",
|
||||
" used": "",
|
||||
"CPU": "CPU"
|
||||
}
|
||||
|
||||
@ -1,95 +1,99 @@
|
||||
{
|
||||
"Intro": "",
|
||||
"Game Introduction": "",
|
||||
"World selection": "",
|
||||
"Start": "",
|
||||
"Inventory": "",
|
||||
"next level": "",
|
||||
"Next": "",
|
||||
"back to world selection": "",
|
||||
"Leave World": "",
|
||||
"previous level": "",
|
||||
"Previous": "",
|
||||
"Editor mode is enforced!": "",
|
||||
"Editor mode": "",
|
||||
"Typewriter mode": "",
|
||||
"information, Impressum, privacy policy": "",
|
||||
"Preferences": "",
|
||||
"Game Info & Credits": "",
|
||||
"Game Info": "",
|
||||
"Clear Progress": "",
|
||||
"Erase": "",
|
||||
"Download Progress": "",
|
||||
"Download": "",
|
||||
"Load Progress from JSON": "",
|
||||
"Upload": "",
|
||||
"Home": "",
|
||||
"back to games selection": "",
|
||||
"close inventory": "",
|
||||
"show inventory": "",
|
||||
"World": "",
|
||||
"Show more help!": "",
|
||||
"Goal": "",
|
||||
"Objects": "",
|
||||
"Assumptions": "",
|
||||
"Current Goal": "",
|
||||
"Further Goals": "",
|
||||
"No Goals": "",
|
||||
"Loading goal…": "",
|
||||
"Click somewhere in the Lean file to enable the infoview.": "",
|
||||
"Waiting for Lean server to start…": "",
|
||||
"Level completed! 🎉": "",
|
||||
"Level completed with warnings 🎭": "",
|
||||
"Failed command": "",
|
||||
"Retry proof from here": "",
|
||||
"Retry": "",
|
||||
"Active Goal": "",
|
||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "",
|
||||
"Line": "",
|
||||
"Character": "",
|
||||
"Loading messages…": "",
|
||||
"Execute": "",
|
||||
"Tactics": "",
|
||||
"Definitions": "",
|
||||
"Theorems": "",
|
||||
"Not unlocked yet": "",
|
||||
"Not available in this level": "",
|
||||
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "",
|
||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "",
|
||||
"<p>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.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "",
|
||||
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "",
|
||||
"This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "",
|
||||
"view the Lean game server on Github": "",
|
||||
"Prerequisites": "",
|
||||
"Worlds": "",
|
||||
"Levels": "",
|
||||
"Language": "",
|
||||
"Lean Game Server": "",
|
||||
"Development notes": "",
|
||||
"Adding new games": "",
|
||||
"Funding": "",
|
||||
"Level": "",
|
||||
"Introduction": "",
|
||||
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "",
|
||||
"Delete Progress?": "",
|
||||
"Delete": "",
|
||||
"Download & Delete": "",
|
||||
"Cancel": "",
|
||||
"Mobile": "",
|
||||
"Auto": "",
|
||||
"Desktop": "",
|
||||
"Layout": "",
|
||||
"Always visible": "",
|
||||
"Save my settings (in the browser store)": "",
|
||||
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "",
|
||||
"Game Rules": "",
|
||||
"levels": "",
|
||||
"tactics": "",
|
||||
"regular": "",
|
||||
"relaxed": "",
|
||||
"none": "",
|
||||
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "",
|
||||
"Upload Saved Progress": "",
|
||||
"Load selected file": "",
|
||||
"Rules": ""
|
||||
"Intro": "Introducción",
|
||||
"Game Introduction": "Introducción del juego",
|
||||
"World selection": "Seleccionar mundo",
|
||||
"Start": "Empezar",
|
||||
"Inventory": "Inventario",
|
||||
"next level": "siguiente nivel",
|
||||
"Next": "Siguiente",
|
||||
"back to world selection": "volver a la selección de mundos",
|
||||
"Leave World": "Abandonar mundo",
|
||||
"previous level": "nivel anterior",
|
||||
"Previous": "Anterior",
|
||||
"Editor mode is enforced!": "¡El modo editor es obligatorio!",
|
||||
"Editor mode": "Modo editor",
|
||||
"Typewriter mode": "Modo línea a línea",
|
||||
"information, Impressum, privacy policy": "información, Impressum, política de privacidad",
|
||||
"Preferences": "Preferencias",
|
||||
"Game Info & Credits": "Información del juego y reconocimientos",
|
||||
"Game Info": "Información del juego",
|
||||
"Clear Progress": "Limpiar el progreso",
|
||||
"Erase": "Borrar",
|
||||
"Download Progress": "Descargar progreso",
|
||||
"Download": "Descargar",
|
||||
"Load Progress from JSON": "Cargar progreso desde JSON",
|
||||
"Upload": "Subir",
|
||||
"Home": "Inicio",
|
||||
"back to games selection": "volver a la selección de juegos",
|
||||
"close inventory": "cerrar inventario",
|
||||
"show inventory": "mostrar inventario",
|
||||
"World": "Mundo",
|
||||
"Show more help!": "¡Mostrar más ayuda!",
|
||||
"Goal": "Objetivo",
|
||||
"Objects": "Objetos",
|
||||
"Assumptions": "Hipótesis",
|
||||
"Current Goal": "Objetivo actual",
|
||||
"Further Goals": "Objetivos pendientes",
|
||||
"No Goals": "Sin objetivos",
|
||||
"Loading goal…": "Cargando objetivo…",
|
||||
"Click somewhere in the Lean file to enable the infoview.": "Pulsa en algún lugar del archivo Lean para habilitar la vista de información.",
|
||||
"Waiting for Lean server to start…": "Esperando a que el servidor Lean se inicie…",
|
||||
"Level completed! 🎉": "Nivel completado 🎉",
|
||||
"Level completed with warnings 🎭": "Nivel completado con advertencias 🎭",
|
||||
"Failed command": "Comando fallido",
|
||||
"Retry proof from here": "Reintentar la prueba desde aquí",
|
||||
"Retry": "Reintentar",
|
||||
"Active Goal": "Objetivo activo",
|
||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "¡Error! Vaya al modo editor y corrija su prueba. Última respuesta del servidor:",
|
||||
"Line": "Línea",
|
||||
"Character": "Carácter",
|
||||
"Loading messages…": "Cargando mensajes…",
|
||||
"Execute": "Ejecutar",
|
||||
"Tactics": "Tácticas",
|
||||
"Definitions": "Definiciones",
|
||||
"Theorems": "Teoremas",
|
||||
"Not unlocked yet": "No desbloqueado aún",
|
||||
"Not available in this level": "No disponible en este nivel",
|
||||
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "Un repositorio de juegos para aprender el asistente de demostración <1>Lean</1>, <i>(Lean 4)</i> y su biblioteca matemática <5>mathlib</5> ",
|
||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "No se ha cargado ningún juego. Use <1>http://localhost:3000/#/g/local/FOLDER</1> para abrir un juego directamente desde una carpeta local",
|
||||
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>Si está considerando escribir su propio juego, use el <1>GameSkeleton Github Repo</1> como plantilla y lea <3>How to Create a Game</3>.</0><1>Puede cargar directamente los juegos en el servidor y jugarlo usando la URL adecuada. Las <1>instrucciones anteriores</1> también explican los detalles sobre cómo cargar su juego en el servidor. Le animamos a ponerse en contacto con nosotros si tiene preguntas.</1><p>Los juegos incluidos en esta página son añadidos manualmente. Por favor, contactenos y añadiremos el suyo encantados.</p>",
|
||||
"Prerequisites": "Requisitos previos",
|
||||
"Worlds": "Mundos",
|
||||
"Levels": "Niveles",
|
||||
"Language": "Idioma",
|
||||
"Lean Game Server": "Servidor de Juegos de Lean",
|
||||
"Development notes": "Notas de desarrollo",
|
||||
"Adding new games": "Añadir nuevos juegos",
|
||||
"Funding": "Financiación",
|
||||
"Level": "Nivel",
|
||||
"Introduction": "Introducción",
|
||||
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>¿Desea eliminar su progreso guardado definitivamente?</p><p>(Esto elimina sus pruebas y su inventario recopilado. Los progresos guardados de otros juegos no se eliminan.)</p>",
|
||||
"Delete Progress?": "¿Borrar Progreso?",
|
||||
"Delete": "Borrar",
|
||||
"Download & Delete": "Descargar y Borrar",
|
||||
"Cancel": "Cancelar",
|
||||
"Mobile": "Móvil",
|
||||
"Auto": "Automático",
|
||||
"Desktop": "Escritorio",
|
||||
"Layout": "Diseño",
|
||||
"Always visible": "Siempre visible",
|
||||
"Save my settings (in the browser store)": "Guardar mis ajustes (en el almacenamiento del navegador)",
|
||||
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>Las reglas del juego determinan si se permite saltarse niveles y si el juego realiza comprobaciones para permitir únicamente tácticas y teoremas desbloqueados en las pruebas.</p><1>Nota: las tácticas (o teoremas) \"Desbloqueadas\" está determinadas por dos cosas: el conjunto mínimo de tácticas necesarias para resolver un nivel, más cualquier táctica que hayas desbloqueado en otro nivel. Esto significa que si desbloqueas <1>simp</1> en un nivel, puedes usarlo a partir de entonces en cualquier nivel.</1><p>Las opciones son:</p>",
|
||||
"Game Rules": "Reglas del juego",
|
||||
"levels": "niveles",
|
||||
"tactics": "tácticas",
|
||||
"regular": "normal",
|
||||
"relaxed": "relajado",
|
||||
"none": "ninguno",
|
||||
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>Seleccione un archivo JSON con el progreso del juego guardado para cargar su progreso.</p><1><0>Advertencia:</0> Esto borrará su progreso actual en el juego. Considere <2>descargar su progreso actual</2> antes</1>",
|
||||
"Upload Saved Progress": "Subir progreso guardado",
|
||||
"Load selected file": "Cargar archivo seleccionado",
|
||||
"Rules": "Reglas",
|
||||
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "<p>Como este servidor corre en máquinas de nuestra universidad, tiene una capacidad limitada. Nuestra estimación actual es de unos 70 juegos simultaneos.</p>.",
|
||||
"<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "<1>Muchos aspectos de los juegos y la infrastructura están aún en desarrollo. No dude en abrir una <1>GitHub Issue</1> sobre cualquier problema que experimente.</1>",
|
||||
"This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "Este servidor se ha desarrollado como parte del proyecto <1>ADAM: Anticipating the Digital Age of Mathematics</1> en la Heinrich-Heine-Universität de Düsseldorf.",
|
||||
"Server capacity": "",
|
||||
"RAM": "",
|
||||
" used": "",
|
||||
"CPU": ""
|
||||
}
|
||||
|
||||
@ -0,0 +1,8 @@
|
||||
/ko-level1.tmx
|
||||
/ko-level2.tmx
|
||||
/ko-omegat.tmx
|
||||
/**/*.bak
|
||||
/omegat/last_entry.properties
|
||||
/omegat/files_order.txt
|
||||
/omegat/project_stats.txt
|
||||
/tm/*.tmx
|
||||
@ -0,0 +1,15 @@
|
||||
# 린 4 게임
|
||||
|
||||
[English (영어)](./README.md) | 한국어
|
||||
|
||||
## 기여하기
|
||||
|
||||
`lean4game`의 한국어 번역에 기여하는 활동은 언제든지 환영합니다!
|
||||
|
||||
### 한국어 번역
|
||||
|
||||
저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
|
||||
|
||||
[bc]: https://github.com/chabulhwi
|
||||
[omt]: https://omegat.org/
|
||||
[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
|
||||
@ -0,0 +1,18 @@
|
||||
# Lean 4 Game
|
||||
|
||||
English | [한국어[Korean]](./README.ko.md)
|
||||
|
||||
## Contributing
|
||||
|
||||
Contributions to the Korean translation of `lean4game` are always welcome!
|
||||
|
||||
### Korean Translation
|
||||
|
||||
I ([Bulhwi Cha][bc]) use [OmegaT][omt] to translate English documentation into
|
||||
Korean. The OmegaT project is in this directory, that is,
|
||||
`client/public/locales/ko`. You need to install the [Okapi filters plugin for
|
||||
OmegaT][okapi] to make OmegaT parse JSON files.
|
||||
|
||||
[bc]: https://github.com/chabulhwi
|
||||
[omt]: https://omegat.org/
|
||||
[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
|
||||
@ -0,0 +1,167 @@
|
||||
# Glossary in tab-separated format -*- coding: utf-8 -*-
|
||||
St. Anselm 안셀무스
|
||||
ontological 존재론적
|
||||
argument 논증
|
||||
argument 인수
|
||||
Lean 린
|
||||
Lean community 린 커뮤니티
|
||||
God 신
|
||||
Alvin Plantinga 앨빈 플랜팅아
|
||||
exist 존재하다
|
||||
existence 존재
|
||||
the understanding 지성
|
||||
reality 현실
|
||||
assumption 가정
|
||||
reductio 귀류법
|
||||
great 큰
|
||||
premise 전제
|
||||
being 존재자
|
||||
conceive 생각하다
|
||||
definition 정의
|
||||
true 참
|
||||
true 참인
|
||||
false 거짓
|
||||
false 거짓인
|
||||
formulate 정식화하다
|
||||
formulation 정식화
|
||||
formalize 형식화하다
|
||||
formalization 형식화
|
||||
property 속성
|
||||
redundant 불필요한
|
||||
sentence 문장
|
||||
state 진술하다
|
||||
statement 진술
|
||||
proposition 명제
|
||||
negation 부정
|
||||
axiom 공리
|
||||
theorem 정리
|
||||
theory 이론
|
||||
conclude 결론하다
|
||||
prove 증명하다
|
||||
SEP 스탠퍼드 철학 백과사전
|
||||
Eric Wieser 에릭 비저
|
||||
Alistair Tucker 앨리스터 터커
|
||||
philosophy 철학
|
||||
Owl of Sogang 서강올빼미
|
||||
type theory 유형론
|
||||
universe level 유형 세계 변수
|
||||
type 유형
|
||||
type 입력하다
|
||||
type check 유형을 확인하다
|
||||
type check 유형이 확인되다
|
||||
type check 유형 확인이 잘되다
|
||||
type class 유형 클래스
|
||||
instance 사례
|
||||
category mistake 범주 실수
|
||||
class 클래스
|
||||
example 보기
|
||||
example 예
|
||||
inductive type 귀납형
|
||||
define 정의하다
|
||||
constructor 구성자
|
||||
Apache License, Version 2.0 아파치 라이선스, 버전 2.0
|
||||
under the terms of 의 조건에 따라
|
||||
OmegaT 오메가T
|
||||
symbolic link 심벌릭 링크
|
||||
directory 디렉터리
|
||||
root directory 최상위 디렉터리
|
||||
documentation 문서
|
||||
English 영어
|
||||
Korean 한국어
|
||||
chapter 장
|
||||
quiz 퀴즈
|
||||
question 문제
|
||||
command 명령어
|
||||
error 오류
|
||||
code 코드
|
||||
evaluate 계산하다
|
||||
keyword 핵심어
|
||||
declare 선언하다
|
||||
constant 상수
|
||||
reference 참고 문헌
|
||||
universe-polymorphic 세계 다형적
|
||||
parametrically polymorphic 매개 변수 다형적
|
||||
function 함수
|
||||
identifier 식별자
|
||||
definitionally equal 정의상 같은
|
||||
natural number 자연수
|
||||
input 입력값
|
||||
return 반환하다
|
||||
non-zero 영이 아닌
|
||||
zero 영
|
||||
alpha-equivalent 알파 동등한
|
||||
less-than-or-equal-to sign 작거나 같음 부호
|
||||
dependent function 의존 함수
|
||||
dependent function type 의존 함수형
|
||||
dependent product 의존곱
|
||||
dependent product type 의존곱형
|
||||
underscore 밑줄
|
||||
implicit 암시적
|
||||
explicit 명시적
|
||||
sigma type 시그마
|
||||
propositional logic 명제 논리
|
||||
term 항
|
||||
contemporary 동시대
|
||||
term 용어
|
||||
truth-value 진릿값
|
||||
bearer 담지자
|
||||
propositional attitudes 명제적 태도
|
||||
believe 믿다
|
||||
doubt 의심하다
|
||||
South Korea 한국
|
||||
school mathematics 학교 수학
|
||||
sentence 문장
|
||||
high school mathematics 고등학교 수학
|
||||
teacher 교사
|
||||
Stanford Encyclopedia of Philosophy 스탠퍼드 철학 백과사전
|
||||
ordered triple 순서세짝
|
||||
conjecture 추측
|
||||
Goldbach's conjecture 골드바흐의 추측
|
||||
interactive theorem prover 상호 작용 정리 증명기
|
||||
truth 참
|
||||
falsity 거짓
|
||||
rule of inference 추론 규칙
|
||||
introduction rule 도입 규칙
|
||||
elimination rule 제거 규칙
|
||||
ex falso quodlibet 엑스 팔소 세퀴투르 쿠오들리베트
|
||||
principle of explosion 폭발 원리
|
||||
propositional connective 명제 연결사
|
||||
symbol 기호
|
||||
refutation by contradiction 모순에 따른 부인
|
||||
contradiction 모순
|
||||
conjunction 연언
|
||||
disjunction 선언(選言)
|
||||
implication 함의
|
||||
material implication 내용적 함의
|
||||
conditional 조건문
|
||||
modus ponens 긍정 논법[모더스 포넨스]
|
||||
necessary condition 필요조건
|
||||
conversion 역
|
||||
inversion 이(裏)
|
||||
contraposition 대우(對偶)
|
||||
equivalence 동등
|
||||
biconditional 쌍조건문
|
||||
abbreviation 준말
|
||||
if and only if …일 때 그리고 그럴 때만
|
||||
editor 편집기
|
||||
shortcut 단축키
|
||||
Theorem Proving in Lean 4 린 4로 하는 정리 증명
|
||||
exercise 연습 문제
|
||||
repository 저장소
|
||||
Jeremy Avigad 제러미 아비가드
|
||||
Leonardo de Moura 레오나르두 지 모라
|
||||
Soonho Kong 공순호
|
||||
Sebastian Ullrich 제바스티안 울리히
|
||||
file 파일
|
||||
Markdown 마크다운
|
||||
quiz 퀴즈
|
||||
translation 번역
|
||||
contribute 기여하다
|
||||
progress 진도
|
||||
capacity 이용량
|
||||
GitHub 깃허브
|
||||
repo 저장소
|
||||
game rule 게임 규칙
|
||||
unlocked 잠금 해제가 된
|
||||
unlock 잠금 해제를 하다
|
||||
Markdown 마크다운
|
||||
@ -0,0 +1,33 @@
|
||||
<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
|
||||
<omegat>
|
||||
<project version="1.0">
|
||||
<source_dir>__DEFAULT__</source_dir>
|
||||
<source_dir_excludes>
|
||||
<mask>**/.svn/**</mask>
|
||||
<mask>**/CVS/**</mask>
|
||||
<mask>**/.cvs/**</mask>
|
||||
<mask>**/.git/**</mask>
|
||||
<mask>**/.hg/**</mask>
|
||||
<mask>**/.repositories/**</mask>
|
||||
<mask>**/desktop.ini</mask>
|
||||
<mask>**/Thumbs.db</mask>
|
||||
<mask>**/.DS_Store</mask>
|
||||
<mask>**/~$*</mask>
|
||||
</source_dir_excludes>
|
||||
<target_dir>__DEFAULT__</target_dir>
|
||||
<tm_dir>__DEFAULT__</tm_dir>
|
||||
<glossary_dir>__DEFAULT__</glossary_dir>
|
||||
<glossary_file>__DEFAULT__</glossary_file>
|
||||
<dictionary_dir>__DEFAULT__</dictionary_dir>
|
||||
<export_tm_dir>__DEFAULT__</export_tm_dir>
|
||||
<export_tm_levels>omegat level1 level2</export_tm_levels>
|
||||
<source_lang>en</source_lang>
|
||||
<target_lang>ko</target_lang>
|
||||
<source_tok>org.omegat.tokenizer.LuceneEnglishTokenizer</source_tok>
|
||||
<target_tok>org.omegat.tokenizer.HunspellTokenizer</target_tok>
|
||||
<sentence_seg>true</sentence_seg>
|
||||
<support_default_translations>true</support_default_translations>
|
||||
<remove_tags>false</remove_tags>
|
||||
<external_command></external_command>
|
||||
</project>
|
||||
</omegat>
|
||||
File diff suppressed because it is too large
Load Diff
@ -0,0 +1 @@
|
||||
../README.md
|
||||
@ -0,0 +1 @@
|
||||
../../en/translation.json
|
||||
@ -0,0 +1,15 @@
|
||||
# 린 4 게임
|
||||
|
||||
[English (영어)](./README.md) | 한국어
|
||||
|
||||
## 기여하기
|
||||
|
||||
`lean4game`의 한국어 번역에 기여하는 활동은 언제든지 환영합니다!
|
||||
|
||||
### 한국어 번역
|
||||
|
||||
저([차불휘][bc])는 [오메가T(OmegaT)][omt]를 이용해 영어 문서를 한국어로 번역합니다. 오메가T 프로젝트는 이 디렉터리, 다시 말해 `client/public/locales/ko`에 있습니다. 오메가T로 JSON 파일을 구문 분석 하려면 [오메가T를 위한 오카피(Okapi) 필터 플러그인][okapi]을 설치해야 됩니다.
|
||||
|
||||
[bc]: https://github.com/chabulhwi
|
||||
[omt]: https://omegat.org/
|
||||
[okapi]: https://okapiframework.org/wiki/index.php/Okapi_Filters_Plugin_for_OmegaT
|
||||
@ -0,0 +1,99 @@
|
||||
{
|
||||
"Tactics": "전략",
|
||||
"Lean Game Server": "린 게임 서버",
|
||||
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>게임 규칙에 따라, 단계들을 건너뛰어도 되는지 그리고 증명을 작성할 때 잠금 해제가 된 전략과 정리만 이용할 수 있는지가 정해집니다.</p><1>\n\n참고: '잠금 해제'가 된 전략이나 정리는 다음 두 부류로 정해집니다. (1) 해당 단계를 푸는 데 필요한 최소한의 전략이나 정리의 모임, (2) 다른 단계에서 잠금 해제를 한 전략이나 정리. 따라서 여러분이 <1>simp</1> 전략을 잠금 해제 하면, 그 뒤로 어느 단계에서든 이 전략을 이용할 수 있습니다.</1><p>선택할 수 있는 게임 규칙은 다음과 같습니다.</p>",
|
||||
"Game Rules": "게임 규칙",
|
||||
"levels": "단계",
|
||||
"tactics": "전략",
|
||||
"regular": "일반",
|
||||
"relaxed": "완화됨",
|
||||
"none": "없음",
|
||||
"Rules": "규칙",
|
||||
"Intro": "소개",
|
||||
"Game Introduction": "게임 소개",
|
||||
"World selection": "세계 선택",
|
||||
"Start": "시작하기",
|
||||
"Inventory": "인벤토리",
|
||||
"next level": "다음 단계",
|
||||
"Next": "다음",
|
||||
"back to world selection": "세계 선택하러 돌아가기",
|
||||
"Leave World": "세계에서 나가기",
|
||||
"previous level": "이전 단계",
|
||||
"Previous": "이전",
|
||||
"Editor mode is enforced!": "편집기 모드가 강제됐습니다!",
|
||||
"Editor mode": "편집기 모드",
|
||||
"Typewriter mode": "타자기 모드",
|
||||
"information, Impressum, privacy policy": "정보, 관리자 정보, 사생활 정책",
|
||||
"Preferences": "기본 설정",
|
||||
"Game Info & Credits": "게임 정보 및 제작자 명단",
|
||||
"Game Info": "게임 정보",
|
||||
"Clear Progress": "진도 없애기",
|
||||
"Erase": "지우기",
|
||||
"Download Progress": "진도 내려받기",
|
||||
"Download": "내려받기",
|
||||
"Load Progress from JSON": "JSON에서 진도 불러오기",
|
||||
"Upload": "업로드",
|
||||
"Home": "홈",
|
||||
"back to games selection": "게임 선택하러 돌아가기",
|
||||
"close inventory": "인벤토리 닫기",
|
||||
"show inventory": "인벤토리 보기",
|
||||
"World": "세계",
|
||||
"Show more help!": "도움말 더 보기!",
|
||||
"Goal": "목표",
|
||||
"Current Goal": "현재 목표",
|
||||
"Objects": "객체",
|
||||
"Assumptions": "가정",
|
||||
"Further Goals": "이후 목표",
|
||||
"No Goals": "목표 없음",
|
||||
"Loading goal…": "목표 불러오는 중…",
|
||||
"Click somewhere in the Lean file to enable the infoview.": "린 파일의 아무 곳이나 눌러 정보창을 여십시오.",
|
||||
"Waiting for Lean server to start…": "린 서버가 시작하기를 기다리는 중…",
|
||||
"Level completed! 🎉": "단계 완료! 🎉",
|
||||
"Level completed with warnings 🎭": "경고 있는 채로 단계 완료 🎭",
|
||||
"Active Goal": "활성화된 목표",
|
||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "시스템 다운됨! 편집기 모드에서 증명을 고치십시오! 마지막 서버 응답:",
|
||||
"Line": "줄",
|
||||
"Character": "문자",
|
||||
"Loading messages…": "메시지 불러오는 중…",
|
||||
"Execute": "실행하기",
|
||||
"Definitions": "정의",
|
||||
"Theorems": "정리",
|
||||
"Not unlocked yet": "아직 잠금 해제가 안 됨",
|
||||
"Not available in this level": "이 단계에서 쓸 수 없음",
|
||||
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "<1>린(Lean 4)</1> 증명 보조기와 그 수학 라이브러리 <5>매스리브(mathlib)</5>를 학습하기 위한 게임들의 저장소",
|
||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "불러온 게임 없음. <1>http://localhost:3000/#/g/local/FOLDER</1>를 이용해 지역[로컬] 폴더에서 게임을 직접 여십시오.",
|
||||
"Prerequisites": "선행 요건",
|
||||
"Worlds": "세계",
|
||||
"Levels": "단계",
|
||||
"Language": "언어",
|
||||
"Server capacity": "서버 이용량",
|
||||
"RAM": "램",
|
||||
"CPU": "CPU",
|
||||
"Development notes": "개발 노트",
|
||||
"Adding new games": "새 게임 추가하기",
|
||||
"Funding": "재정 지원",
|
||||
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>저장된 진도를 불가역적으로 삭제하시겠습니까?</p><p>(이를 선택하시면 증명과 인벤토리 안의 수집 항목들이 삭제됩니다. 다른 게임에 저장된 정보는 삭제되지 않습니다.)</p>",
|
||||
"Delete Progress?": "진도를 삭제하시겠습니까?",
|
||||
"Delete": "삭제하기",
|
||||
"Download & Delete": "내려받고 삭제하기",
|
||||
"Cancel": "취소하기",
|
||||
"Layout": "레이아웃",
|
||||
"Always visible": "항상 보임",
|
||||
"Save my settings (in the browser store)": "(브라우저에) 설정 저장하기",
|
||||
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>저장된 게임 진도가 있는 JSON 파일을 선택해 진도를 불러오십시오.</p><1><0>경고:</0> 이를 실행하면 현재의 게임 진도가 삭제됩니다! <2>현재의 게임 진도</2>를 먼저 내려받을지 판단하십시오!</1>",
|
||||
"Upload Saved Progress": "저장된 진도 업로드",
|
||||
"Load selected file": "선택한 파일 열기",
|
||||
"Mobile": "모바일",
|
||||
"Auto": "자동",
|
||||
"Desktop": "데스크톱",
|
||||
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> 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.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>여러분이 직접 게임을 작성할 생각이 있다면, <1>GameSkeleton 깃허브 저장소</1>를 양식[템플릿]으로 이용하고 <3>'게임 만들기(Creating a Game)'</3> 문서를 읽으십시오.</0><1>여러분이 작성한 게임을 직접 서버에서 불러오고, 정확한 URL을 이용해 그 게임을 하실 수 있습니다. 여러분의 게임을 서버에서 불러오는 방법에 관한 세부 사항도 위의 <1>설명서</1>에 나와 있습니다. 궁금한 점이 있으면 저희에게 연락해 주십시오.</1><p>이 페이지에 실린 게임들은 수동으로 추가됐습니다. 저희에게 연락하시면 여러분의 게임을 기꺼이 추가하겠습니다.",
|
||||
"Level": "단계",
|
||||
"Introduction": "소개",
|
||||
"Retry proof from here": "여기부터 증명 다시 시도하기",
|
||||
"Retry": "다시 시도하기",
|
||||
"Failed command": "실패한 명령",
|
||||
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games.</p>": "",
|
||||
"<0>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</0>": "",
|
||||
"This server has been developed as part of the project <1>ADAM: Anticipating the Digital Age of Mathematics</1> at Heinrich Heine University Düsseldorf.": "",
|
||||
" used": ""
|
||||
}
|
||||
@ -0,0 +1 @@
|
||||
target/translation.json
|
||||
@ -0,0 +1,311 @@
|
||||
/**
|
||||
* @file contains the navigation bars of the app.
|
||||
*/
|
||||
import * as React from 'react'
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
|
||||
import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
|
||||
faArrowRight, faArrowLeft, faXmark, faBars, faCode,
|
||||
faCircleInfo, faTerminal, faGear } from '@fortawesome/free-solid-svg-icons'
|
||||
import { GameIdContext } from "../app"
|
||||
import { InputModeContext, PreferencesContext, WorldLevelIdContext } from "./infoview/context"
|
||||
import { GameInfo, useGetGameInfoQuery } from '../state/api'
|
||||
import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress } from '../state/progress'
|
||||
import { useAppDispatch, useAppSelector } from '../hooks'
|
||||
import { Button } from './button'
|
||||
import { downloadProgress } from './popup/erase'
|
||||
import { useTranslation } from 'react-i18next'
|
||||
|
||||
/** navigation buttons for mobile welcome page to switch between intro/tree/inventory. */
|
||||
function MobileNavButtons({pageNumber, setPageNumber}:
|
||||
{ pageNumber: number,
|
||||
setPageNumber: any}) {
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const { t } = useTranslation()
|
||||
const dispatch = useAppDispatch()
|
||||
|
||||
// if `prevText` or `prevIcon` is set, show a button to go back
|
||||
let prevText = {0: null, 1: t("Intro"), 2: null}[pageNumber]
|
||||
let prevIcon = {0: null, 1: null, 2: faBookOpen}[pageNumber]
|
||||
let prevTitle = {0: null, 1: t("Game Introduction"), 2: t("World selection")}[pageNumber]
|
||||
// if `nextText` or `nextIcon` is set, show a button to go forward
|
||||
let nextText = {0: t("Start"), 1: null, 2: null}[pageNumber]
|
||||
let nextIcon = {0: null, 1: faBook, 2: null}[pageNumber]
|
||||
let nextTitle = {0: t("World selection"), 1: t("Inventory"), 2: null}[pageNumber]
|
||||
|
||||
return <>
|
||||
{(prevText || prevIcon) &&
|
||||
<Button className="btn btn-inverted toggle-width" to={pageNumber == 0 ? "/" : ""}
|
||||
inverted="true" title={prevTitle}
|
||||
onClick={() => {pageNumber == 0 ? null : setPageNumber(pageNumber - 1)}}>
|
||||
{prevIcon && <FontAwesomeIcon icon={prevIcon} />}
|
||||
{prevText && `${prevText}`}
|
||||
</Button>
|
||||
}
|
||||
{(nextText || nextIcon) &&
|
||||
<Button className="btn btn-inverted toggle-width" to="" inverted="true"
|
||||
title={nextTitle} onClick={() => {
|
||||
console.log(`page number: ${pageNumber}`)
|
||||
setPageNumber(pageNumber+1);
|
||||
dispatch(changedOpenedIntro({game: gameId, openedIntro: true}))}}>
|
||||
{nextText && `${nextText}`}
|
||||
{nextIcon && <FontAwesomeIcon icon={nextIcon} />}
|
||||
</Button>
|
||||
}
|
||||
</>
|
||||
}
|
||||
|
||||
/** button to toggle dropdown menu. */
|
||||
export function MenuButton({navOpen, setNavOpen}) {
|
||||
return <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}}>
|
||||
{navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
|
||||
</Button>
|
||||
}
|
||||
|
||||
/** button to go one level futher.
|
||||
* for the last level, this button turns into a button going back to the welcome page.
|
||||
*/
|
||||
function NextButton({worldSize, difficulty, completed, setNavOpen}) {
|
||||
const { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const {worldId, levelId} = React.useContext(WorldLevelIdContext)
|
||||
return (levelId < worldSize ?
|
||||
<Button inverted="true"
|
||||
to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title={t("next level")}
|
||||
disabled={difficulty >= 2 && !(completed || levelId == 0)}
|
||||
onClick={() => setNavOpen(false)}>
|
||||
<FontAwesomeIcon icon={faArrowRight} /> {levelId ? t("Next") : t("Start")}
|
||||
</Button>
|
||||
:
|
||||
<Button to={`/${gameId}`} inverted="true" title={t("back to world selection")} id="home-btn">
|
||||
<FontAwesomeIcon icon={faHome} /> {t("Leave World")}
|
||||
</Button>
|
||||
)
|
||||
}
|
||||
|
||||
/** button to go one level back.
|
||||
* only renders if the current level id is > 0.
|
||||
*/
|
||||
function PreviousButton({setNavOpen}) {
|
||||
const { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const {worldId, levelId} = React.useContext(WorldLevelIdContext)
|
||||
return (levelId > 0 && <>
|
||||
<Button disabled={levelId <= 0} inverted="true"
|
||||
to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
|
||||
title={t("previous level")}
|
||||
onClick={() => setNavOpen(false)}>
|
||||
<FontAwesomeIcon icon={faArrowLeft} /> {t("Previous")}
|
||||
</Button>
|
||||
</>)
|
||||
}
|
||||
|
||||
/** button to toggle between editor and typewriter */
|
||||
function InputModeButton({setNavOpen, isDropdown}) {
|
||||
const { t } = useTranslation()
|
||||
const {levelId} = React.useContext(WorldLevelIdContext)
|
||||
const {typewriterMode, setTypewriterMode, lockEditorMode} = React.useContext(InputModeContext)
|
||||
|
||||
/** toggle input mode if allowed */
|
||||
function toggleInputMode(ev: React.MouseEvent) {
|
||||
if (!lockEditorMode){
|
||||
setTypewriterMode(!typewriterMode)
|
||||
setNavOpen(false)
|
||||
}
|
||||
}
|
||||
|
||||
return <Button
|
||||
className={`btn btn-inverted ${isDropdown? '' : 'toggle-width'}`} disabled={levelId <= 0 || lockEditorMode}
|
||||
inverted="true" to=""
|
||||
onClick={(ev) => toggleInputMode(ev)}
|
||||
title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")}>
|
||||
<FontAwesomeIcon icon={(typewriterMode && !lockEditorMode) ? faCode : faTerminal} />
|
||||
{isDropdown && ((typewriterMode && !lockEditorMode) ? <> {t("Editor mode")}</> : <> {t("Typewriter mode")}</>)}
|
||||
</Button>
|
||||
}
|
||||
|
||||
/** button to toggle iimpressum popup
|
||||
*
|
||||
* Note: Do not translate the word "Impressum"! German GDPR needs this.
|
||||
*/
|
||||
export function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button className="btn btn-inverted"
|
||||
title={t("information, Impressum, privacy policy")} inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faCircleInfo} />
|
||||
{isDropdown && <> Impressum</>}
|
||||
</Button>
|
||||
}
|
||||
|
||||
export function PreferencesButton({setNavOpen, togglePreferencesPopup}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button title={t("Preferences")} inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faGear} /> {t("Preferences")}
|
||||
</Button>
|
||||
}
|
||||
|
||||
function GameInfoButton({setNavOpen, toggleInfo}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button className="btn btn-inverted"
|
||||
title={t("Game Info & Credits")} inverted="true" to="" onClick={() => {toggleInfo(); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faCircleInfo} /> {t("Game Info")}
|
||||
</Button>
|
||||
}
|
||||
|
||||
function EraseButton ({setNavOpen, toggleEraseMenu}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button title={t("Clear Progress")} inverted="true" to="" onClick={() => {toggleEraseMenu(); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faEraser} /> {t("Erase")}
|
||||
</Button>
|
||||
}
|
||||
|
||||
function DownloadButton ({setNavOpen, gameId, gameProgress}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button title={t("Download Progress")} inverted="true" to="" onClick={(ev) => {downloadProgress(gameId, gameProgress, ev); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faDownload} /> {t("Download")}
|
||||
</Button>
|
||||
}
|
||||
|
||||
function UploadButton ({setNavOpen, toggleUploadMenu}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button title={t("Load Progress from JSON")} inverted="true" to="" onClick={() => {toggleUploadMenu(); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faUpload} /> {t("Upload")}
|
||||
</Button>
|
||||
}
|
||||
|
||||
/** button to go back to welcome page */
|
||||
function HomeButton({isDropdown}) {
|
||||
const { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
return <Button to={`/${gameId}`} inverted="true" title={t("back to world selection")} id="home-btn">
|
||||
<FontAwesomeIcon icon={faHome} />
|
||||
{isDropdown && <> {t("Home")}</>}
|
||||
</Button>
|
||||
}
|
||||
|
||||
function LandingPageButton() {
|
||||
const { t } = useTranslation()
|
||||
return <Button inverted="false" title={t("back to games selection")} to="/">
|
||||
<FontAwesomeIcon icon={faArrowLeft} /> <FontAwesomeIcon icon={faGlobe} />
|
||||
</Button>
|
||||
}
|
||||
|
||||
/** button in mobile level to toggle inventory.
|
||||
* only displays a button if `setPageNumber` is set.
|
||||
*/
|
||||
function InventoryButton({pageNumber, setPageNumber}) {
|
||||
const { t } = useTranslation()
|
||||
return (setPageNumber &&
|
||||
<Button to="" className="btn btn-inverted toggle-width"
|
||||
title={pageNumber ? t("close inventory") : t("show inventory")}
|
||||
inverted="true" onClick={() => {setPageNumber(pageNumber ? 0 : 1)}}>
|
||||
<FontAwesomeIcon icon={pageNumber ? faBookOpen : faBook} />
|
||||
</Button>
|
||||
)
|
||||
}
|
||||
|
||||
/** the navigation bar on the welcome page */
|
||||
export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo, togglePreferencesPopup} : {
|
||||
pageNumber: number,
|
||||
setPageNumber: any,
|
||||
gameInfo: GameInfo,
|
||||
toggleImpressum: any,
|
||||
toggleEraseMenu: any,
|
||||
toggleUploadMenu: any,
|
||||
toggleInfo: any,
|
||||
togglePreferencesPopup: () => void;
|
||||
}) {
|
||||
const { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const gameProgress = useAppSelector(selectProgress(gameId))
|
||||
const {mobile} = React.useContext(PreferencesContext)
|
||||
const [navOpen, setNavOpen] = React.useState(false)
|
||||
|
||||
return <div className="app-bar">
|
||||
<div className='app-bar-left'>
|
||||
<LandingPageButton />
|
||||
<span className="app-bar-title"></span>
|
||||
</div>
|
||||
<div>
|
||||
{!mobile && <span className="app-bar-title">{t(gameInfo?.title, {ns: gameId})}</span>}
|
||||
</div>
|
||||
<div className="nav-btns">
|
||||
{mobile && <MobileNavButtons pageNumber={pageNumber} setPageNumber={setPageNumber} />}
|
||||
<MenuButton navOpen={navOpen} setNavOpen={setNavOpen} />
|
||||
</div>
|
||||
<div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
|
||||
<GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
|
||||
<EraseButton setNavOpen={setNavOpen} toggleEraseMenu={toggleEraseMenu}/>
|
||||
<DownloadButton setNavOpen={setNavOpen} gameId={gameId} gameProgress={gameProgress}/>
|
||||
<UploadButton setNavOpen={setNavOpen} toggleUploadMenu={toggleUploadMenu}/>
|
||||
<ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
|
||||
<PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** the navigation bar in a level */
|
||||
export function LevelAppBar({isLoading, levelTitle, toggleImpressum, toggleInfo, togglePreferencesPopup, pageNumber=undefined, setPageNumber=undefined} : {
|
||||
isLoading: boolean,
|
||||
levelTitle: string,
|
||||
toggleImpressum: any,
|
||||
toggleInfo: any,
|
||||
togglePreferencesPopup: any,
|
||||
pageNumber?: number,
|
||||
setPageNumber?: any,
|
||||
}) {
|
||||
const { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const {worldId, levelId} = React.useContext(WorldLevelIdContext)
|
||||
const {mobile} = React.useContext(PreferencesContext)
|
||||
const [navOpen, setNavOpen] = React.useState(false)
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
|
||||
const difficulty = useAppSelector(selectDifficulty(gameId))
|
||||
|
||||
let worldTitle = gameInfo.data?.worlds.nodes[worldId].title
|
||||
|
||||
return <div className="app-bar" style={isLoading ? {display: "none"} : null} >
|
||||
{mobile ?
|
||||
<>
|
||||
{/* MOBILE VERSION */}
|
||||
<div>
|
||||
<span className="app-bar-title">{levelTitle}</span>
|
||||
</div>
|
||||
<div className="nav-btns">
|
||||
<InventoryButton pageNumber={pageNumber} setPageNumber={setPageNumber}/>
|
||||
<MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
|
||||
</div>
|
||||
<div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
|
||||
<NextButton worldSize={gameInfo.data?.worldSize[worldId]} difficulty={difficulty} completed={completed} setNavOpen={setNavOpen} />
|
||||
<PreviousButton setNavOpen={setNavOpen} />
|
||||
<HomeButton isDropdown={true} />
|
||||
<InputModeButton setNavOpen={setNavOpen} isDropdown={true}/>
|
||||
<GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
|
||||
<ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
|
||||
<PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
|
||||
</div>
|
||||
</> :
|
||||
<>
|
||||
{/* DESKTOP VERSION */}
|
||||
<div className='app-bar-left'>
|
||||
<HomeButton isDropdown={false} />
|
||||
<span className="app-bar-title">{worldTitle && `${t("World")}: ${t(worldTitle, {ns: gameId})}`}</span>
|
||||
</div>
|
||||
<div>
|
||||
<span className="app-bar-title">{levelTitle}</span>
|
||||
</div>
|
||||
<div className="nav-btns">
|
||||
<PreviousButton setNavOpen={setNavOpen} />
|
||||
<NextButton worldSize={gameInfo.data?.worldSize[worldId]} difficulty={difficulty} completed={completed} setNavOpen={setNavOpen} />
|
||||
<InputModeButton setNavOpen={setNavOpen} isDropdown={false}/>
|
||||
<MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
|
||||
</div>
|
||||
<div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
|
||||
<GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
|
||||
<ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
|
||||
<PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
|
||||
</div>
|
||||
</>
|
||||
}
|
||||
</div>
|
||||
}
|
||||
@ -0,0 +1,15 @@
|
||||
import * as React from 'react';
|
||||
import { Link, LinkProps } from "react-router-dom";
|
||||
|
||||
export interface ButtonProps extends LinkProps {
|
||||
disabled?: boolean
|
||||
inverted?: string // Apparently "inverted" in DOM cannot be `boolean` but must be `inverted`
|
||||
}
|
||||
|
||||
export function Button(props: ButtonProps) {
|
||||
if (props.disabled) {
|
||||
return <span className={`btn btn-disabled ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</span>
|
||||
} else {
|
||||
return <Link className={`btn ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</Link>
|
||||
}
|
||||
}
|
||||
@ -1,450 +0,0 @@
|
||||
import * as React from 'react'
|
||||
import { useContext, useEffect, useRef, useState } from 'react'
|
||||
import { useSelector } from 'react-redux'
|
||||
import { useTranslation } from 'react-i18next'
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
|
||||
import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
|
||||
|
||||
import { changedReadIntro, selectCompleted, selectReadIntro } from '../state/progress'
|
||||
import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'
|
||||
import { useAppDispatch, useAppSelector } from '../hooks'
|
||||
import { Button, Markdown } from './utils'
|
||||
import { ChatContext, GameIdContext, PageContext, PreferencesContext, ProofContext } from '../state/context'
|
||||
import { GameHint, InteractiveGoalsWithHints } from './infoview/rpc_api'
|
||||
// import { lastStepHasErrors } from './infoview/goals'
|
||||
// import { AllMessages } from '../../../node_modules/@leanprover/infoview/dist/infoview/messages'
|
||||
// import { LeanDiagnostic, RpcErrorCode, getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api'
|
||||
import { Location, DocumentUri, Diagnostic, DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol'
|
||||
// import { InteractiveMessage } from '../../../node_modules/lean4-infoview/src/infoview/traceExplorer'
|
||||
|
||||
import '../css/chat.css'
|
||||
import { faHome } from '@fortawesome/free-solid-svg-icons'
|
||||
|
||||
|
||||
/** Split a string by double newlines and filters out empty segments. */
|
||||
function splitIntro (intro : string) {
|
||||
return intro.split(/\n(\s*\n)+/).filter(t => t.trim())
|
||||
}
|
||||
|
||||
/** Helper to check if a step has any hidden hints. */
|
||||
function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
|
||||
return step?.goals[0]?.hints.some((hint) => hint.hidden)
|
||||
}
|
||||
|
||||
/** Button which only appears if the current step has hidden hints that are not shown yet. */
|
||||
export function MoreHelpButton({selected=null} : {selected?: number}) {
|
||||
|
||||
const { t } = useTranslation()
|
||||
|
||||
const { proof } = React.useContext(ProofContext)
|
||||
const { showHelp, setShowHelp } = React.useContext(ChatContext)
|
||||
|
||||
let k = 0
|
||||
// let k = proof?.steps.length ?
|
||||
// ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected)
|
||||
// : 0
|
||||
|
||||
const activateHiddenHints = (ev) => {
|
||||
// If the last step (`k`) has errors, we want the hidden hints from the
|
||||
// second-to-last step to be affected
|
||||
if (!(proof?.steps.length)) {return <></>}
|
||||
|
||||
// state must not be mutated, therefore we need to clone the set
|
||||
let tmp = new Set(showHelp)
|
||||
if (tmp.has(k)) {
|
||||
tmp.delete(k)
|
||||
} else {
|
||||
tmp.add(k)
|
||||
}
|
||||
setShowHelp(tmp)
|
||||
console.debug(`help: ${Array.from(tmp.values())}`)
|
||||
}
|
||||
|
||||
if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
|
||||
return <Button to="" onClick={activateHiddenHints}>
|
||||
{t("Show more help!")}
|
||||
</Button>
|
||||
}
|
||||
return <></>
|
||||
}
|
||||
|
||||
/** Placeholder that takes the same space as a button. */
|
||||
function ButtonPlaceholder() {
|
||||
return <div className='btn-placeholder'/>
|
||||
}
|
||||
|
||||
/** The buttons at the bottom of chat. */
|
||||
export function ChatButtons ({counter=undefined, setCounter=()=>{}, introMessages=[]} : {
|
||||
counter?: number
|
||||
setCounter?: React.Dispatch<React.SetStateAction<number>>
|
||||
introMessages?: GameHintWithStep[]
|
||||
}) {
|
||||
let { t } = useTranslation()
|
||||
|
||||
const { mobile } = useContext(PreferencesContext)
|
||||
const { gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
const {setPage} = useContext(PageContext)
|
||||
const dispatch = useAppDispatch()
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const { proof } = useContext(ProofContext)
|
||||
|
||||
const readIntro = useSelector(selectReadIntro(gameId, worldId))
|
||||
|
||||
return <div className="button-row">
|
||||
{!levelId && (readIntro || (counter >= introMessages.length) ?
|
||||
((worldId || mobile) &&
|
||||
<>
|
||||
<ButtonPlaceholder />
|
||||
<Button className="btn"
|
||||
title=""
|
||||
to={worldId ? `/${gameId}/world/${worldId}/level/1` : ''}
|
||||
onClick={() => {
|
||||
if (!worldId) {
|
||||
console.log('setting `readIntro` to true')
|
||||
setPage(1)
|
||||
}
|
||||
}} >
|
||||
Start <FontAwesomeIcon icon={faArrowRight}/>
|
||||
</Button>
|
||||
</>
|
||||
)
|
||||
:
|
||||
<>
|
||||
<Button className="btn"
|
||||
title=""
|
||||
to=""
|
||||
onClick={() => {
|
||||
if (counter + 1 >= introMessages.length) {
|
||||
dispatch(changedReadIntro({game: gameId, world: worldId, readIntro: true}))
|
||||
}
|
||||
setCounter(counter + 1)
|
||||
}} >
|
||||
{"Read"}
|
||||
</Button>
|
||||
<Button className="btn"
|
||||
title=""
|
||||
to=""
|
||||
onClick={() => {
|
||||
dispatch(changedReadIntro({game: gameId, world: worldId, readIntro: true}))
|
||||
setCounter(introMessages.length)
|
||||
}} >
|
||||
Skip all
|
||||
</Button>
|
||||
</>
|
||||
)}
|
||||
{ (worldId && levelId) ? <MoreHelpButton /> : <></> }
|
||||
{ (worldId && levelId && proof?.completed) ?
|
||||
(levelId == gameInfo.data?.worldSize[worldId] ?
|
||||
<Button className="btn"
|
||||
title=""
|
||||
to={`/${gameId}`} >
|
||||
<FontAwesomeIcon icon={faHome} /> {t("Home")}
|
||||
</Button> :
|
||||
<Button className="btn"
|
||||
title=""
|
||||
to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} >
|
||||
{t("Next")} <FontAwesomeIcon icon={faArrowRight} />
|
||||
|
||||
</Button>
|
||||
) : <></> }
|
||||
</div>
|
||||
}
|
||||
|
||||
/** Insert the variable names in a hint. We do this client-side to prepare
|
||||
* for i18n in the future. i.e. one should be able translate the `rawText`
|
||||
* and have the variables substituted just before displaying.
|
||||
*/
|
||||
function getHintText(hint: GameHint): string {
|
||||
const {gameId} = React.useContext(GameIdContext)
|
||||
let { t } = useTranslation()
|
||||
if (hint.rawText) {
|
||||
// Replace the variable names used in the hint with the ones used by the player
|
||||
// variable names are marked like `«{g}»` inside the text.
|
||||
return t(hint.rawText, {ns: gameId}).replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
|
||||
// `hint.varNames` contains tuples `[oldName, newName]`
|
||||
(hint.varNames.find(x => x[0] == v))[1]))
|
||||
} else {
|
||||
// hints created in the frontend do not have a `rawText`
|
||||
// TODO: `hint.text` could be removed in theory.
|
||||
return t(hint.text, {ns: gameId})
|
||||
}
|
||||
}
|
||||
|
||||
/** Hint kinds. Note that number 1-4 are matching the numbers from `DiagnosticSeverity`
|
||||
* from the vscode language server protocol.
|
||||
*/
|
||||
enum HintKind {
|
||||
Error = 1,
|
||||
Warning = 2,
|
||||
Information = 3,
|
||||
Hint = 4,
|
||||
GameHint = 5,
|
||||
Conclusion = 7,
|
||||
}
|
||||
|
||||
/** Bundling a hint with the proof-step it comes from. */
|
||||
type GameHintWithStep = {
|
||||
hint: GameHint
|
||||
kind: HintKind
|
||||
step?: number
|
||||
}
|
||||
|
||||
/** Filter hints to not show consequtive identical hints twice.
|
||||
* Hidden hints are not filtered.
|
||||
*/
|
||||
export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
|
||||
if (!hints) {
|
||||
return []
|
||||
} else if (!prevHints) {
|
||||
return [...hints.filter((hint) => !hint.hidden), ...hints.filter((hint) => hint.hidden)]
|
||||
} else {
|
||||
return [...hints.filter((hint) => !hint.hidden &&
|
||||
(prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
|
||||
), ...hints.filter((hint) => hint.hidden)]
|
||||
}
|
||||
}
|
||||
|
||||
// TODO
|
||||
// function helper(step, proof, kind, typewriterMode, selectedStep) {
|
||||
// return (step == proof?.steps?.length - (lastStepHasErrors(proof) ? 2 : 1) ? ' recent' : '') +
|
||||
// (!(kind == HintKind.Conclusion) && step >= (typewriterMode ? proof?.steps?.length : selectedStep+1) ? ' deleted-hint' : '')
|
||||
// }
|
||||
|
||||
/** A hint as it is displayed in the chat. */
|
||||
export function Hint({hint, kind, step=null} : GameHintWithStep) {
|
||||
const { levelId } = useContext(GameIdContext)
|
||||
const { selectedStep, setSelectedStep } = useContext(ChatContext)
|
||||
|
||||
const { proof } = useContext(ProofContext)
|
||||
const { typewriterMode } = useContext(PageContext)
|
||||
|
||||
function toggleSelection () {
|
||||
if (!levelId) {return}
|
||||
|
||||
if (selectedStep !== null && selectedStep == step) {
|
||||
setSelectedStep(null)
|
||||
} else if (step < proof?.steps?.length) {
|
||||
setSelectedStep(step)
|
||||
}
|
||||
}
|
||||
|
||||
// "Deleted hints" are marked in grey. They are used two-fold:
|
||||
// In typewriter, deleting parts of the proof stores the removed hints as `deletedChat`
|
||||
// until the next command is submitted; in editor, moving the cursor through the proof will
|
||||
// render all hints
|
||||
return <div className={`message kind-${kind} step-${step}` +
|
||||
((selectedStep !== null && step == selectedStep) ? ' selected' : '') //+ helper(step, proof, kind, typewriterMode, selectedStep)
|
||||
} onClick={toggleSelection}>
|
||||
<Markdown>{getHintText(hint)}</Markdown>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** A collection of hints. If the `counter` is defined, only the first elements will be
|
||||
* shown up to the value of the `counter`.
|
||||
*
|
||||
* Set `conclusion` to true to trigger different style and disable selecting/deleting.
|
||||
*/
|
||||
export function Hints({ hints, counter=undefined } : {
|
||||
hints: GameHintWithStep[],
|
||||
counter?: number
|
||||
}) {
|
||||
|
||||
const { showHelp } = useContext(ChatContext)
|
||||
|
||||
if (!hints) {
|
||||
return <></>
|
||||
}
|
||||
|
||||
// NOTE: This builds on the fact that `.slice(0, undefined)` returns the whole array!
|
||||
// TODO: Should not use index as key.
|
||||
return <>
|
||||
{ hints.slice(0, counter).map((hint, j) =>
|
||||
((!hint.hint.hidden || showHelp.has(hint.step)) &&
|
||||
<Hint key={`hint-${hint.step}-${j}`} hint={hint.hint} kind={hint.kind} step={hint.step} />
|
||||
)
|
||||
)}
|
||||
{/* { //showHelp.has(hint.step) &&
|
||||
hints.filter(hint => hint.hint.hidden).map((hint, j) =>
|
||||
<Hint
|
||||
key={`hidden-hint-${hint.step}-${j}`}
|
||||
hint={hint.hint}
|
||||
step={hint.step}
|
||||
conclusion={hint.conclusion} />
|
||||
)} */}
|
||||
</>
|
||||
}
|
||||
|
||||
/** the panel showing the game's introduction text */
|
||||
export function ChatPanel ({visible = true}) {
|
||||
|
||||
let { t } = useTranslation()
|
||||
|
||||
const { mobile } = useContext(PreferencesContext)
|
||||
const { gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
|
||||
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
|
||||
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
|
||||
const [counter, setCounter] = useState(1)
|
||||
|
||||
const [introText, setIntroText] = useState<Array<GameHintWithStep>>([])
|
||||
const { chatRef, deletedChat, showHelp, selectedStep } = useContext(ChatContext)
|
||||
const { proof } = useContext(ProofContext)
|
||||
|
||||
const readIntro = useSelector(selectReadIntro(gameId, worldId))
|
||||
|
||||
useEffect(() => {
|
||||
setCounter(1)
|
||||
}, [gameId, worldId, levelId])
|
||||
|
||||
// load and display the correct intro text
|
||||
useEffect(() => {
|
||||
if (levelId > 0) {
|
||||
let introText = t(levelInfo.data?.introduction, {ns : gameId}).trim()
|
||||
let introHint: GameHintWithStep = {hint: {text: introText, hidden: false, rawText: introText }, kind: HintKind.GameHint, step: 0}
|
||||
|
||||
// playable level: show the level's intro
|
||||
if (levelInfo.data?.introduction) {
|
||||
setIntroText([introHint])
|
||||
// messages = messages.concat([introHint])
|
||||
}
|
||||
else {
|
||||
setIntroText([])
|
||||
}
|
||||
} else {
|
||||
if (worldId) {
|
||||
let introText = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).trim()
|
||||
let introHints: GameHintWithStep[] = splitIntro(introText).map( txt => ({hint: {text: txt, hidden: false, rawText: txt }, kind: HintKind.GameHint, step: 0}))
|
||||
|
||||
// Level 0: show the world's intro
|
||||
if (gameInfo.data?.worlds.nodes[worldId].introduction) {
|
||||
// messages = messages.concat(introHints)
|
||||
setIntroText(introHints)
|
||||
} else {
|
||||
setIntroText([])
|
||||
}
|
||||
} else {
|
||||
let introText = t(gameInfo.data?.introduction, {ns : gameId}).trim()
|
||||
let introHints: GameHintWithStep[] = splitIntro(introText).map( txt => ({hint: {text: txt, hidden: false, rawText: txt }, kind: HintKind.GameHint, step: 0}))
|
||||
|
||||
// world overview: show the game's intro
|
||||
if (gameInfo.data?.introduction) {
|
||||
// messages = messages.concat(introHints)
|
||||
setIntroText(introHints)
|
||||
} else {
|
||||
setIntroText([])
|
||||
}
|
||||
}
|
||||
}
|
||||
}, [gameInfo, levelInfo, gameId, worldId, levelId, proof])
|
||||
|
||||
// Scroll the chat
|
||||
useEffect(() => {
|
||||
if (levelId > 0) {
|
||||
|
||||
if (proof) {
|
||||
if (proof?.completed) {
|
||||
// proof currently completed: scroll down
|
||||
console.debug('scroll chat: down to conclusion')
|
||||
chatRef.current!.lastElementChild?.scrollIntoView({block: "center"})
|
||||
} else {
|
||||
// proof currently not completed: first message of last step
|
||||
let lastStep = proof?.steps.length //- (lastStepHasErrors(proof) ? 2 : 1)
|
||||
console.debug(`scroll chat: first message of step ${lastStep}`)
|
||||
chatRef.current?.getElementsByClassName(`step-${lastStep}`)[0]?.scrollIntoView({block: "center"})
|
||||
}
|
||||
} else {
|
||||
// no proof available: scroll to top.
|
||||
console.debug(`scroll chat: top`)
|
||||
chatRef.current!.scrollTo(0,0)
|
||||
}
|
||||
} else {
|
||||
// introduction: scroll to last message
|
||||
console.debug('scroll chat: down')
|
||||
chatRef.current!.lastElementChild?.scrollIntoView({block: "center"})
|
||||
}
|
||||
}, [counter, introText, gameId, worldId, levelId])
|
||||
|
||||
// Scroll down when new hidden hints are triggered
|
||||
useEffect(() => {
|
||||
if (levelId > 0) {
|
||||
let lastStep = proof?.steps.length //- (lastStepHasErrors(proof) ? 2 : 1)
|
||||
if (showHelp.has(lastStep)) {
|
||||
console.debug('scroll chat: down to hidden hints')
|
||||
// TODO: last element of hidden hints?
|
||||
chatRef.current!.lastElementChild?.scrollIntoView({block: "center"})
|
||||
}
|
||||
}
|
||||
}, [showHelp, gameId, worldId, levelId])
|
||||
|
||||
// Scroll to corresponding messages if selected step changes
|
||||
useEffect(() => {
|
||||
if (levelId > 0 && selectedStep !== null) {
|
||||
console.debug(`scroll chat: first message of selected step ${selectedStep}`)
|
||||
chatRef.current?.getElementsByClassName(`step-${selectedStep}`)[0]?.scrollIntoView({block: "center"})
|
||||
// Array.from(chatRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => {
|
||||
// elem.scrollIntoView({block: "center"})
|
||||
// })
|
||||
}
|
||||
}, [selectedStep, gameId, worldId, levelId])
|
||||
|
||||
/** TODO: What's the magic here? Only needed if diags are displayed in chat. */
|
||||
function diagToString (diag) {
|
||||
// Hide "unsolved goals" messages
|
||||
let message;
|
||||
if ("append" in diag.message && "text" in diag.message.append[0] &&
|
||||
diag.message?.append[0].text === "unsolved goals") {
|
||||
message = diag.message.append[0]
|
||||
} else {
|
||||
message = diag.message
|
||||
}
|
||||
return message
|
||||
}
|
||||
|
||||
return <div className={`column chat-panel${visible ? '' : ' hidden'}`}>
|
||||
<div ref={chatRef} className="chat" >
|
||||
{ gameInfo.error &&
|
||||
<div className="message error">
|
||||
Could not find the game!
|
||||
</div>
|
||||
}
|
||||
<Hints hints={introText} counter={readIntro ? undefined : counter}/>
|
||||
{proof?.steps.map((step, i) => {
|
||||
let x = [].concat(
|
||||
filterHints(step.goals[0]?.hints, proof.steps[i-1]?.goals[0]?.hints).map(hint => ({hint: hint, kind: HintKind.GameHint, step: i})),
|
||||
// // TODO: Uncomment this if you want to see the diags in chat
|
||||
// step.diags.map(diag => ({hint: diagToString(diag), kind: diag.severity, step: i}))
|
||||
)
|
||||
|
||||
return <Hints key={`hints-step-${i}`} hints={x}/>
|
||||
})}
|
||||
|
||||
{/* <Hints hints={chatMessages}/> */}
|
||||
{/* {proof?.steps.map((step, i) =>
|
||||
<Hints hints={step.goals[0]?.hints.map(hint => ({hint: hint, step: i}))}/>
|
||||
)} */}
|
||||
{/* <Hints hints={proof?.steps[proof?.steps?.length - 1]?.goals[0].hints.map(hint => ({hint: hint, step: proof?.steps?.length - 1}))} /> */}
|
||||
|
||||
{ deletedChat &&
|
||||
<Hints hints={deletedChat.map(hint => ({hint: hint, kind: HintKind.GameHint, step: proof?.steps?.length}))} />
|
||||
}
|
||||
{ completed && levelInfo.data?.conclusion &&
|
||||
<Hints hints={[
|
||||
{hint: {text: t("Level completed! 🎉"), rawText: t("Level completed! 🎉"), hidden: false}, kind: HintKind.Conclusion, step: proof?.steps?.length},
|
||||
{hint: {text: levelInfo.data?.conclusion, rawText: levelInfo.data?.conclusion, hidden: false}, kind: HintKind.GameHint, step: proof?.steps?.length}
|
||||
]} />
|
||||
}
|
||||
|
||||
{/* {chatMessages.map(((t, i) =>
|
||||
t.trim() ?
|
||||
<Hint key={`intro-p-${i}`}
|
||||
hint={{text: t, hidden: false, rawText: t, varNames: []}}
|
||||
step={0} />
|
||||
: <></>
|
||||
))} */}
|
||||
</div>
|
||||
{ <ChatButtons counter={counter} setCounter={setCounter} introMessages={introText}/> }
|
||||
</div>
|
||||
}
|
||||
@ -1,104 +0,0 @@
|
||||
import * as React from 'react';
|
||||
import Split from 'react-split'
|
||||
import { useContext, useEffect, useRef, useState } from 'react'
|
||||
import { useTranslation } from "react-i18next"
|
||||
import { GameIdContext, MonacoEditorContext } from '../../state/context';
|
||||
import { useLoadLevelQuery } from '../../state/api';
|
||||
import { Markdown } from '../utils';
|
||||
import * as monaco from 'monaco-editor'
|
||||
import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'
|
||||
|
||||
import '../../css/editor.css'
|
||||
import { useSelector } from 'react-redux';
|
||||
import { selectTypewriterMode } from '../../state/progress';
|
||||
import { TypewriterInterFace } from './Typewriter';
|
||||
|
||||
export function Editor() {
|
||||
let { t } = useTranslation()
|
||||
const {gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
|
||||
const typewriterMode = useSelector(selectTypewriterMode(gameId))
|
||||
|
||||
const editorRef = useRef<HTMLDivElement>(null)
|
||||
const infoviewRef = useRef<HTMLDivElement>(null)
|
||||
const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor>()
|
||||
const [leanMonaco, setLeanMonaco] = useState<LeanMonaco>()
|
||||
const [code, setCode] = useState<string>('')
|
||||
|
||||
const [options, setOptions] = useState<LeanMonacoOptions>({
|
||||
// placeholder. gets set below
|
||||
websocket: {
|
||||
url: ''
|
||||
}
|
||||
})
|
||||
|
||||
// Update LeanMonaco options when preferences are loaded or change
|
||||
useEffect(() => {
|
||||
var socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") +
|
||||
window.location.host + `/websocket/${gameId}`
|
||||
console.log(`[LeanGame] socket url: ${socketUrl}`)
|
||||
var _options: LeanMonacoOptions = {
|
||||
websocket: {
|
||||
url: socketUrl,
|
||||
// @ts-ignore
|
||||
difficulty: 1,
|
||||
inventory: []
|
||||
},
|
||||
// Restrict monaco's extend (e.g. context menu) to the editor itself
|
||||
htmlElement: editorRef.current ?? undefined,
|
||||
vscode: {
|
||||
/* To add settings here, you can open your settings in VSCode (Ctrl+,), search
|
||||
* for the desired setting, select "Copy Setting as JSON" from the "More Actions"
|
||||
* menu next to the selected setting, and paste the copied string here.
|
||||
*/
|
||||
// "workbench.colorTheme": preferences.theme,
|
||||
"editor.tabSize": 2,
|
||||
// "editor.rulers": [100],
|
||||
"editor.lightbulb.enabled": "on",
|
||||
"editor.wordWrap": "on",
|
||||
"editor.wrappingStrategy": "advanced",
|
||||
"editor.semanticHighlighting.enabled": true,
|
||||
"editor.acceptSuggestionOnEnter": "off",
|
||||
"lean4.input.eagerReplacementEnabled": true,
|
||||
// "lean4.input.leader": preferences.abbreviationCharacter
|
||||
}
|
||||
}
|
||||
setOptions(_options)
|
||||
}, [editorRef])
|
||||
|
||||
// Setting up the editor and infoview
|
||||
useEffect(() => {
|
||||
console.debug('[LeanGame] Restarting Editor!')
|
||||
var _leanMonaco = new LeanMonaco()
|
||||
var leanMonacoEditor = new LeanMonacoEditor()
|
||||
|
||||
_leanMonaco.setInfoviewElement(infoviewRef.current!)
|
||||
;(async () => {
|
||||
await _leanMonaco.start(options)
|
||||
console.warn('gameId', gameId)
|
||||
await leanMonacoEditor.start(editorRef.current!, `/${worldId}/L_${levelId}.lean`, code)
|
||||
|
||||
setEditor(leanMonacoEditor.editor)
|
||||
setLeanMonaco(_leanMonaco)
|
||||
|
||||
// Keeping the `code` state up-to-date with the changes in the editor
|
||||
leanMonacoEditor.editor?.onDidChangeModelContent(() => {
|
||||
setCode(leanMonacoEditor.editor?.getModel()?.getValue()!)
|
||||
})
|
||||
})()
|
||||
return () => {
|
||||
leanMonacoEditor.dispose()
|
||||
_leanMonaco.dispose()
|
||||
}
|
||||
}, [options, infoviewRef, editorRef, gameId, worldId, levelId])
|
||||
|
||||
return <MonacoEditorContext.Provider value={editor}>
|
||||
<div className="editor-wrapper"><Split direction='vertical' minSize={200} sizes={[50, 50]}
|
||||
className={`editor-split ${typewriterMode ? 'hidden' : ''}`} >
|
||||
<div ref={editorRef} id="editor" />
|
||||
<div ref={infoviewRef} id="infoview" />
|
||||
</Split>
|
||||
{typewriterMode && <TypewriterInterFace />}
|
||||
</div>
|
||||
</MonacoEditorContext.Provider>
|
||||
}
|
||||
@ -1,37 +0,0 @@
|
||||
import * as React from 'react';
|
||||
import { useContext, useEffect, useRef, useState } from 'react'
|
||||
import { useTranslation } from "react-i18next"
|
||||
import { GameIdContext } from '../../state/context';
|
||||
import { useLoadLevelQuery } from '../../state/api';
|
||||
import { Markdown } from '../utils';
|
||||
|
||||
/** The mathematical formulation of the statement, supporting e.g. Latex
|
||||
* It takes three forms, depending on the precence of name and description:
|
||||
* - Theorem xyz: description
|
||||
* - Theorem xyz
|
||||
* - Exercises: description
|
||||
*
|
||||
* If `showLeanStatement` is true, it will additionally display the lean code.
|
||||
*/
|
||||
export function ExerciseStatement({ showLeanStatement = false }) {
|
||||
let { t } = useTranslation()
|
||||
const {gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
|
||||
if (!(levelInfo.data?.descrText || levelInfo.data?.descrFormat)) { return <></> }
|
||||
return <>
|
||||
<div className="exercise-statement">
|
||||
{levelInfo.data?.descrText ?
|
||||
<Markdown>
|
||||
{(levelInfo.data?.displayName ? `**${t("Theorem")}** \`${levelInfo.data?.displayName}\`: ` : '') + t(levelInfo.data?.descrText, {ns: gameId})}
|
||||
</Markdown> : levelInfo.data?.displayName &&
|
||||
<Markdown>
|
||||
{`**${t("Theorem")}** \`${levelInfo.data?.displayName}\``}
|
||||
</Markdown>
|
||||
}
|
||||
{levelInfo.data?.descrFormat && showLeanStatement &&
|
||||
<p><code className="lean-code">{levelInfo.data?.descrFormat}</code></p>
|
||||
}
|
||||
</div>
|
||||
</>
|
||||
}
|
||||
@ -1,443 +0,0 @@
|
||||
import * as React from 'react'
|
||||
import { useContext } from 'react'
|
||||
import { useRef, useState, useEffect } from 'react'
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
|
||||
import { faArrowRight, faHome, faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
|
||||
import { DiagnosticSeverity, PublishDiagnosticsParams, DocumentUri } from 'vscode-languageserver-protocol';
|
||||
import { useTranslation } from 'react-i18next'
|
||||
import * as monaco from 'monaco-editor'
|
||||
import { ChatContext, GameIdContext, InputModeContext, MonacoEditorContext, PageContext, PreferencesContext, ProofContext } from '../../state/context';
|
||||
|
||||
import { RpcContext, WithRpcSessions, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
|
||||
import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
|
||||
|
||||
import '../../css/infoview.css'
|
||||
import { useGetGameInfoQuery } from '../../state/api'
|
||||
import { GameHint } from './Defs'
|
||||
import { MoreHelpButton, filterHints } from '../chat'
|
||||
import { isLastStepWithErrors, lastStepHasErrors, loadGoals } from '../infoview/goals'
|
||||
import { getInteractiveDiagsAt, hasInteractiveErrors } from '../infoview/typewriter'
|
||||
import { Errors } from '../infoview/messages'
|
||||
import { Button, Markdown } from '../utils'
|
||||
import { Command, GoalsTabs } from '../infoview/main'
|
||||
import { CircularProgress } from '@mui/material'
|
||||
|
||||
/** The input field */
|
||||
export function TypewriterInput({disabled}: {disabled?: boolean}) {
|
||||
let { t } = useTranslation()
|
||||
|
||||
/** Reference to the hidden multi-line editor */
|
||||
// const editor = React.useContext(MonacoEditorContext)
|
||||
// const model = editor.getModel()
|
||||
// const uri = model.uri.toString()
|
||||
|
||||
const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
|
||||
const [processing, setProcessing] = useState(false)
|
||||
|
||||
// const {typewriterInput, setTypewriterInput} = React.useContext(InputModeContext)
|
||||
|
||||
const inputRef = useRef()
|
||||
|
||||
// // The context storing all information about the current proof
|
||||
const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext)
|
||||
|
||||
// // state to store the last batch of deleted messages
|
||||
// const {setDeletedChat} = React.useContext(DeletedChatContext)
|
||||
|
||||
// const rpcSess = React.useContext(RpcContext)
|
||||
|
||||
// // Run the command
|
||||
// const runCommand = React.useCallback(() => {
|
||||
// if (processing) {return}
|
||||
|
||||
// // TODO: Desired logic is to only reset this after a new *error-free* command has been entered
|
||||
// setDeletedChat([])
|
||||
|
||||
// const pos = editor.getPosition()
|
||||
// if (typewriterInput) {
|
||||
// setProcessing(true)
|
||||
// editor.executeEdits("typewriter", [{
|
||||
// range: monaco.Selection.fromPositions(
|
||||
// pos,
|
||||
// editor.getModel().getFullModelRange().getEndPosition()
|
||||
// ),
|
||||
// text: typewriterInput.trim() + "\n",
|
||||
// forceMoveMarkers: false
|
||||
// }])
|
||||
// setTypewriterInput('')
|
||||
// // Load proof after executing edits
|
||||
// loadGoals(rpcSess, uri, setProof, setCrashed)
|
||||
// }
|
||||
|
||||
// editor.setPosition(pos)
|
||||
// }, [typewriterInput, editor])
|
||||
|
||||
// useEffect(() => {
|
||||
// if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) {
|
||||
// oneLineEditor.setValue(typewriterInput)
|
||||
// }
|
||||
// }, [typewriterInput])
|
||||
|
||||
// /* Load proof on start/switching to typewriter */
|
||||
// useEffect(() => {
|
||||
// loadGoals(rpcSess, uri, setProof, setCrashed)
|
||||
// }, [])
|
||||
|
||||
// /** If the last step has an error, add the command to the typewriter. */
|
||||
// useEffect(() => {
|
||||
// if (lastStepHasErrors(proof)) {
|
||||
// setTypewriterInput(proof?.steps[proof?.steps.length - 1].command)
|
||||
// }
|
||||
// }, [proof])
|
||||
|
||||
// // React when answer from the server comes back
|
||||
// useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
|
||||
// if (params.uri == uri) {
|
||||
// setProcessing(false)
|
||||
|
||||
// console.log('Received lean diagnostics')
|
||||
// console.log(params.diagnostics)
|
||||
// setInterimDiags(params.diagnostics)
|
||||
|
||||
// //loadGoals(rpcSess, uri, setProof)
|
||||
|
||||
// // TODO: loadAllGoals()
|
||||
// if (!hasErrors(params.diagnostics)) {
|
||||
// //setTypewriterInput("")
|
||||
// editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
|
||||
// }
|
||||
// } else {
|
||||
// // console.debug(`expected uri: ${uri}, got: ${params.uri}`)
|
||||
// // console.debug(params)
|
||||
// }
|
||||
// // TODO: This is the wrong place apparently. Where do wee need to load them?
|
||||
// // TODO: instead of loading all goals every time, we could only load the last one
|
||||
// // loadAllGoals()
|
||||
// }, [uri]);
|
||||
|
||||
// // // React when answer from the server comes back
|
||||
// // useServerNotificationEffect('$/game/publishDiagnostics', (params: GameDiagnosticsParams) => {
|
||||
// // console.log('Received game diagnostics')
|
||||
// // console.log(`diag. uri : ${params.uri}`)
|
||||
// // console.log(params.diagnostics)
|
||||
|
||||
// // }, [uri]);
|
||||
|
||||
|
||||
// useEffect(() => {
|
||||
// const myEditor = monaco.editor.create(inputRef.current!, {
|
||||
// value: typewriterInput,
|
||||
// language: "lean4cmd",
|
||||
// quickSuggestions: false,
|
||||
// lightbulb: {
|
||||
// enabled: true
|
||||
// },
|
||||
// unicodeHighlight: {
|
||||
// ambiguousCharacters: false,
|
||||
// },
|
||||
// automaticLayout: true,
|
||||
// minimap: {
|
||||
// enabled: false
|
||||
// },
|
||||
// lineNumbers: 'off',
|
||||
// tabSize: 2,
|
||||
// glyphMargin: false,
|
||||
// folding: false,
|
||||
// lineDecorationsWidth: 0,
|
||||
// lineNumbersMinChars: 0,
|
||||
// 'semanticHighlighting.enabled': true,
|
||||
// overviewRulerLanes: 0,
|
||||
// hideCursorInOverviewRuler: true,
|
||||
// scrollbar: {
|
||||
// vertical: 'hidden',
|
||||
// horizontalScrollbarSize: 3
|
||||
// },
|
||||
// overviewRulerBorder: false,
|
||||
// theme: 'vs-code-theme-converted',
|
||||
// contextmenu: false
|
||||
// })
|
||||
|
||||
// setOneLineEditor(myEditor)
|
||||
|
||||
// const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), myEditor.getModel(), myEditor)
|
||||
|
||||
// return () => {abbrevRewriter.dispose(); myEditor.dispose()}
|
||||
// }, [])
|
||||
|
||||
// useEffect(() => {
|
||||
// if (!oneLineEditor) return
|
||||
// // Ensure that our one-line editor can only have a single line
|
||||
// const l = oneLineEditor.getModel().onDidChangeContent((e) => {
|
||||
// const value = oneLineEditor.getValue()
|
||||
// setTypewriterInput(value)
|
||||
// const newValue = value.replace(/[\n\r]/g, '')
|
||||
// if (value != newValue) {
|
||||
// oneLineEditor.setValue(newValue)
|
||||
// }
|
||||
// })
|
||||
// return () => { l.dispose() }
|
||||
// }, [oneLineEditor, setTypewriterInput])
|
||||
|
||||
// useEffect(() => {
|
||||
// if (!oneLineEditor) return
|
||||
// // Run command when pressing enter
|
||||
// const l = oneLineEditor.onKeyUp((ev) => {
|
||||
// if (ev.code === "Enter") {
|
||||
// runCommand()
|
||||
// }
|
||||
// })
|
||||
// return () => { l.dispose() }
|
||||
// }, [oneLineEditor, runCommand])
|
||||
|
||||
// // BUG: Causes `file closed` error
|
||||
// //TODO: Intention is to run once when loading, does that work?
|
||||
// useEffect(() => {
|
||||
// console.debug(`time to update: ${uri} \n ${rpcSess}`)
|
||||
// console.debug(rpcSess)
|
||||
// // console.debug('LOAD ALL GOALS')
|
||||
// // TODO: loadAllGoals()
|
||||
// }, [rpcSess])
|
||||
|
||||
/** Process the entered command */
|
||||
const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
|
||||
// ev.preventDefault()
|
||||
// runCommand()
|
||||
}
|
||||
|
||||
// do not display if the proof is completed (with potential warnings still present)
|
||||
return <div className={`typewriter-cmd${proof?.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
|
||||
<form onSubmit={handleSubmit}>
|
||||
<div className="typewriter-input-wrapper">
|
||||
<div ref={inputRef} className="typewriter-input" />
|
||||
</div>
|
||||
<button type="submit" disabled={processing} className="btn btn-inverted">
|
||||
<FontAwesomeIcon icon={faWandMagicSparkles} /> {t("Execute")}
|
||||
</button>
|
||||
</form>
|
||||
</div>
|
||||
}
|
||||
|
||||
export function TypewriterInterFace() {
|
||||
let { t } = useTranslation()
|
||||
const {gameId, worldId, levelId} = useContext(GameIdContext)
|
||||
const editor = useContext(MonacoEditorContext)
|
||||
const model = editor.getModel()
|
||||
const uri = model.uri.toString()
|
||||
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
let image: string = gameInfo.data?.worlds.nodes[worldId].image
|
||||
|
||||
|
||||
const [disableInput, setDisableInput] = useState<boolean>(false)
|
||||
const [loadingProgress, setLoadingProgress] = useState<number>(0)
|
||||
const { selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp } = useContext(ChatContext)
|
||||
const {mobile} = useContext(PreferencesContext)
|
||||
const { proof, setProof, crashed, setCrashed, interimDiags } = useContext(ProofContext)
|
||||
const { setTypewriterInput } = useContext(PageContext)
|
||||
|
||||
const proofPanelRef = React.useRef<HTMLDivElement>(null)
|
||||
// const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
|
||||
// const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
|
||||
|
||||
const rpcSess = useRpcSessionAtPos({uri: uri, line: 0, character: 0})
|
||||
|
||||
/** Delete all proof lines starting from a given line.
|
||||
* Note that the first line (i.e. deleting everything) is `1`!
|
||||
*/
|
||||
function deleteProof(line: number) {
|
||||
return (ev) => {
|
||||
let deletedChat: Array<GameHint> = []
|
||||
proof?.steps.slice(line).map((step, i) => {
|
||||
let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
|
||||
|
||||
// Only add these hidden hints to the deletion stack which were visible
|
||||
deletedChat = [...deletedChat, ...filteredHints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
|
||||
})
|
||||
setDeletedChat(deletedChat)
|
||||
|
||||
// delete showHelp for deleted steps
|
||||
setShowHelp(new Set(Array.from(showHelp).filter(i => i < line - 1)))
|
||||
|
||||
editor.executeEdits("typewriter", [{
|
||||
range: monaco.Selection.fromPositions(
|
||||
{ lineNumber: line, column: 1 },
|
||||
editor.getModel().getFullModelRange().getEndPosition()
|
||||
),
|
||||
text: '',
|
||||
forceMoveMarkers: false
|
||||
}])
|
||||
setSelectedStep(null)
|
||||
setTypewriterInput(proof?.steps[line].command)
|
||||
// Reload proof on deleting
|
||||
loadGoals(rpcSess, uri, setProof, setCrashed)
|
||||
ev.stopPropagation()
|
||||
}
|
||||
}
|
||||
|
||||
function toggleSelectStep(line: number) {
|
||||
return (ev) => {
|
||||
if (mobile) {return}
|
||||
if (selectedStep == line) {
|
||||
setSelectedStep(null)
|
||||
console.debug(`unselected step`)
|
||||
} else {
|
||||
setSelectedStep(line)
|
||||
console.debug(`step ${line} selected`)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Scroll to the end of the proof if it is updated.
|
||||
React.useEffect(() => {
|
||||
if (proof?.steps.length > 1) {
|
||||
proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
|
||||
} else {
|
||||
proofPanelRef.current?.scrollTo(0,0)
|
||||
}
|
||||
// also reenable the commandline when the proof changes
|
||||
|
||||
// BUG: If selecting 2nd goal on a intermediate proofstep and then delete proof to there,
|
||||
// the commandline is not displaying disabled even though it should.
|
||||
setDisableInput(false)
|
||||
}, [proof])
|
||||
|
||||
// Scroll to element if selection changes
|
||||
React.useEffect(() => {
|
||||
if (typeof selectedStep !== 'undefined') {
|
||||
Array.from(proofPanelRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => {
|
||||
elem.scrollIntoView({ block: "center" })
|
||||
})
|
||||
}
|
||||
}, [selectedStep])
|
||||
|
||||
// TODO: superfluous, can be replaced with `withErr` from above
|
||||
let lastStepErrors = proof?.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof?.steps.length)) : false
|
||||
|
||||
|
||||
useServerNotificationEffect("$/game/loading", (params : any) => {
|
||||
if (params.kind == "loadConstants") {
|
||||
setLoadingProgress(params.counter/100*50)
|
||||
} else if (params.kind == "finalizeExtensions") {
|
||||
setLoadingProgress(50 + params.counter/150*50)
|
||||
} else {
|
||||
console.error(`Unknown loading kind: ${params.kind}`)
|
||||
}
|
||||
})
|
||||
|
||||
return <div className="typewriter-interface">
|
||||
<RpcContext.Provider value={rpcSess}>
|
||||
<div className="content">
|
||||
{/* <div className='world-image-container empty'>
|
||||
{image &&
|
||||
<img className="contain" src={path.join("data", gameId, image)} alt="" />
|
||||
}
|
||||
|
||||
</div> */}
|
||||
{/* <div className="tmp-pusher">
|
||||
<div className="world-image-container empty">
|
||||
|
||||
</div>
|
||||
</div> */}
|
||||
<div className='proof' ref={proofPanelRef}>
|
||||
{/* <ExerciseStatement /> */}
|
||||
{crashed ? <div>
|
||||
<p className="crashed_message">{t("Crashed! Go to editor mode and fix your proof! Last server response:")}</p>
|
||||
{interimDiags.map(diag => {
|
||||
const severityClass = diag.severity ? {
|
||||
[DiagnosticSeverity.Error]: 'error',
|
||||
[DiagnosticSeverity.Warning]: 'warning',
|
||||
[DiagnosticSeverity.Information]: 'information',
|
||||
[DiagnosticSeverity.Hint]: 'hint',
|
||||
}[diag.severity] : '';
|
||||
|
||||
return <div key={diag.message} >
|
||||
<div className={`${severityClass} ml1 message`}>
|
||||
<p className="mv2">{t("Line")} {diag.range.start.line}, {t("Character")} {diag.range.start.character}</p>
|
||||
<pre className="font-code pre-wrap">
|
||||
{diag.message}as React
|
||||
</pre>
|
||||
</div>
|
||||
</div>
|
||||
})}
|
||||
|
||||
</div> : proof?.steps.length ?
|
||||
<>
|
||||
{proof?.steps.map((step, i) => {
|
||||
let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
|
||||
|
||||
// if (i == proof?.steps.length - 1 && hasInteractiveErrors(step.diags)) {
|
||||
// // if the last command contains an error, we only display the errors but not the
|
||||
// // entered command as it is still present in the command line.
|
||||
// // TODO: Should not use index as key.
|
||||
// return <div key={`proof-step-${i}`} className={`step step-${i}`}>
|
||||
// <Errors errors={step.diags} typewriterMode={true} />
|
||||
// </div>
|
||||
// } else {
|
||||
return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')}>
|
||||
{i > 0 && <>
|
||||
<Command proof={proof} i={i} deleteProof={deleteProof(i)} />
|
||||
<Errors errors={step.diags} typewriterMode={true} />
|
||||
</>}
|
||||
{/* {mobile && i == 0 && props.data?.introduction &&
|
||||
<div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
|
||||
<Markdown>{props.data?.introduction}</Markdown>
|
||||
</div>
|
||||
}
|
||||
{mobile &&
|
||||
<Hints key={`hints-${i}`}
|
||||
hints={filteredHints.map(hint => ({hint: hint, step: i}))} />
|
||||
} */}
|
||||
{/* <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
|
||||
{!(isLastStepWithErrors(proof, i)) &&
|
||||
<GoalsTabs goals={step.goals} last={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
|
||||
}
|
||||
{mobile && i == proof?.steps.length - 1 &&
|
||||
<MoreHelpButton />
|
||||
}
|
||||
|
||||
{/* Show a message that there are no goals left */}
|
||||
{/* {!step.goals.length && (
|
||||
<div className="message information">
|
||||
{proof?.completed ?
|
||||
<p>Level completed! 🎉</p> :
|
||||
<p>
|
||||
<b>no goals left</b><br />
|
||||
<i>This probably means you solved the level with warnings or Lean encountered a parsing error.</i>
|
||||
</p>
|
||||
}
|
||||
</div>
|
||||
)} */}
|
||||
</div>
|
||||
}
|
||||
//}
|
||||
)}
|
||||
{proof?.diagnostics.length > 0 &&
|
||||
<div key={`proof-step-remaining`} className="step step-remaining">
|
||||
<Errors errors={proof?.diagnostics} typewriterMode={true} />
|
||||
</div>
|
||||
}
|
||||
{mobile && proof?.completed &&
|
||||
<div className="button-row mobile">
|
||||
{/* {props.level >= props.worldSize ?
|
||||
<Button to={`/${gameId}`}>
|
||||
<FontAwesomeIcon icon={faHome} /> {t("Home")}
|
||||
</Button>
|
||||
:
|
||||
<Button to={`/${gameId}/world/${props.world}/level/${props.level + 1}`}>
|
||||
Next <FontAwesomeIcon icon={faArrowRight} />
|
||||
</Button>
|
||||
} */}
|
||||
</div>
|
||||
}
|
||||
</> : <CircularProgress variant="determinate" value={100*(1 - 1.024 ** (- loadingProgress))} />
|
||||
// note: since we don't know the total number of files,
|
||||
// we use a function which strictly monotonely increases towards `100` as `x → ∞`
|
||||
// The base is chosen at random s.t. we get roughly 91% for `x = 100`.
|
||||
}
|
||||
</div>
|
||||
</div>
|
||||
{/* <Typewriter disabled={disableInput || !proof?.steps.length}/> */}
|
||||
<TypewriterInput />
|
||||
</RpcContext.Provider>
|
||||
</div>
|
||||
}
|
||||
@ -1,24 +1,17 @@
|
||||
import * as React from 'react'
|
||||
import { useRouteError } from "react-router-dom";
|
||||
import '../css/error_page.css'
|
||||
|
||||
/** The fallback error page */
|
||||
export default function ErrorPage() {
|
||||
const error: any = useRouteError()
|
||||
console.error(error)
|
||||
const error: any = useRouteError();
|
||||
console.error(error);
|
||||
|
||||
return (
|
||||
<div id="error-page">
|
||||
<div className="error-message">
|
||||
<h1>Oops!</h1>
|
||||
<p>Something unexpected happened:</p>
|
||||
<p><code>({error.status}) {error.statusText || error.message}<br/>{error.data}</code></p>
|
||||
<p>Please create an issue at the <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">lean4game repo</a>.</p>
|
||||
<div className="thought-bubble" />
|
||||
<div className="thought-bubble" />
|
||||
<div className="thought-bubble" />
|
||||
<div className="thought-bubble" />
|
||||
</div>
|
||||
<h1>Oops!</h1>
|
||||
<p>Sorry, an unexpected error has occurred.</p>
|
||||
<p>
|
||||
<i>{error.statusText || error.message}</i>
|
||||
</p>
|
||||
</div>
|
||||
)
|
||||
);
|
||||
}
|
||||
|
||||
@ -1,14 +0,0 @@
|
||||
import * as React from 'react'
|
||||
import ReactCountryFlag from 'react-country-flag'
|
||||
import lean4gameConfig from '../config.json'
|
||||
|
||||
/** Displays either a flag or the language-code, depending on the settings.
|
||||
* The argument `iso` is an ISO-language code.
|
||||
*/
|
||||
export const Flag : React.FC<{ iso: string, showTitle?: boolean}> = ({iso, showTitle=false}) => {
|
||||
let lang = lean4gameConfig.newLanguages[iso]
|
||||
if (lean4gameConfig.useFlags && lang) {
|
||||
return <ReactCountryFlag countryCode={lang.flag} title={showTitle ? lang.name : null} />
|
||||
}
|
||||
return <span>{iso}</span>
|
||||
}
|
||||
@ -1,112 +0,0 @@
|
||||
import * as React from 'react'
|
||||
import { useContext, useEffect, useRef, useState } from 'react'
|
||||
import Split from 'react-split'
|
||||
|
||||
import { useAppDispatch, useAppSelector } from '../hooks'
|
||||
import { changeTypewriterMode, selectCode, selectSelections, selectTypewriterMode } from '../state/progress'
|
||||
import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'
|
||||
import { ChatContext, GameIdContext, PageContext, PreferencesContext, ProofContext } from '../state/context'
|
||||
import { InventoryPanel } from './inventory'
|
||||
import { WorldTreePanel } from './world_tree'
|
||||
|
||||
import i18next from 'i18next'
|
||||
import { ChatPanel } from './chat'
|
||||
import { NewLevel } from './level'
|
||||
import { GameHint, ProofState } from './editor/Defs'
|
||||
import { useSelector } from 'react-redux'
|
||||
import { Diagnostic } from 'vscode-languageserver-types'
|
||||
|
||||
import '../css/game.css'
|
||||
import '../css/welcome.css'
|
||||
import '../css/level.css'
|
||||
|
||||
/** main page of the game showing among others the tree of worlds/levels */
|
||||
function Game() {
|
||||
|
||||
const dispatch = useAppDispatch()
|
||||
const { gameId, worldId, levelId } = React.useContext(GameIdContext)
|
||||
|
||||
// Load the namespace of the game
|
||||
i18next.loadNamespaces(gameId)
|
||||
|
||||
const {mobile} = useContext(PreferencesContext)
|
||||
const {isSavePreferences, language, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
|
||||
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
const inventory = useLoadInventoryOverviewQuery({game: gameId})
|
||||
|
||||
const {page, setPage} = useContext(PageContext)
|
||||
|
||||
const chatRef = useRef<HTMLDivElement>(null)
|
||||
// When deleting the proof, we want to keep to old messages around until
|
||||
// a new proof has been entered. e.g. to consult messages coming from dead ends
|
||||
const [deletedChat, setDeletedChat] = useState<Array<GameHint>>([])
|
||||
// A set of row numbers where help is displayed
|
||||
const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
|
||||
// Select and highlight proof steps and corresponding hints
|
||||
// TODO: with the new design, there is no difference between the introduction and
|
||||
// a hint at the beginning of the proof...
|
||||
const [selectedStep, setSelectedStep] = useState<number>(null)
|
||||
|
||||
// The state variables for the `ProofContext`
|
||||
const [proof, setProof] = useState<ProofState>({steps: [], diagnostics: [], completed: false, completedWithWarnings: false})
|
||||
const [interimDiags, setInterimDiags] = useState<Array<Diagnostic>>([])
|
||||
const [isCrashed, setIsCrashed] = useState<Boolean>(false)
|
||||
|
||||
const typewriterMode = useSelector(selectTypewriterMode(gameId))
|
||||
const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
|
||||
|
||||
const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
|
||||
const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
|
||||
|
||||
// set the window title
|
||||
useEffect(() => {
|
||||
if (gameInfo.data?.title) {
|
||||
window.document.title = gameInfo.data.title
|
||||
}
|
||||
}, [gameInfo.data?.title])
|
||||
|
||||
// Delete the current proof on changing level
|
||||
useEffect(() => {
|
||||
setProof(null)
|
||||
setSelectedStep(null)
|
||||
setDeletedChat([])
|
||||
setShowHelp(new Set())
|
||||
}, [gameId, worldId, levelId])
|
||||
|
||||
return <ChatContext.Provider value={{selectedStep, setSelectedStep, deletedChat, setDeletedChat, showHelp, setShowHelp, chatRef}}>
|
||||
<ProofContext.Provider value={{proof, setProof, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
|
||||
{ mobile ?
|
||||
<div className="app-content mobile">
|
||||
{<>
|
||||
<ChatPanel visible={worldId ? (levelId == 0 && page == 1) :(page == 0)} />
|
||||
{ worldId ?
|
||||
<NewLevel visible={page == 1} /> :
|
||||
<WorldTreePanel visible={page == 1} />
|
||||
}
|
||||
<InventoryPanel visible={page == 2} />
|
||||
</>
|
||||
}
|
||||
</div>
|
||||
:
|
||||
<Split className="app-content" minSize={0} snapOffset={200} sizes={[25, 50, 25]}>
|
||||
<ChatPanel />
|
||||
<div className="column">
|
||||
{/* Note: apparently without this `div` the split panel bugs out. */}
|
||||
{worldId ?
|
||||
<NewLevel />
|
||||
: <WorldTreePanel /> }
|
||||
</div>
|
||||
<InventoryPanel />
|
||||
</Split>
|
||||
}
|
||||
</ProofContext.Provider>
|
||||
</ChatContext.Provider>
|
||||
|
||||
}
|
||||
|
||||
export default Game
|
||||
function useLevelEditor(codeviewRef: React.MutableRefObject<HTMLDivElement>, initialCode: any, initialSelections: any, onDidChangeContent: any, onDidChangeSelection: any): { editor: any; infoProvider: any; editorConnection: any } {
|
||||
throw new Error('Function not implemented.')
|
||||
}
|
||||
@ -0,0 +1,125 @@
|
||||
import { GameHint, InteractiveGoalsWithHints, ProofState } from "./infoview/rpc_api";
|
||||
import * as React from 'react';
|
||||
import Markdown from './markdown';
|
||||
import { DeletedChatContext, ProofContext } from "./infoview/context";
|
||||
import { lastStepHasErrors } from "./infoview/goals";
|
||||
import { Button } from "./button";
|
||||
import { useTranslation } from "react-i18next";
|
||||
import { GameIdContext } from "../app";
|
||||
|
||||
/** Plug-in the variable names in a hint. We do this client-side to prepare
|
||||
* for i18n in the future. i.e. one should be able translate the `rawText`
|
||||
* and have the variables substituted just before displaying.
|
||||
*/
|
||||
function getHintText(hint: GameHint): string {
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
let { t } = useTranslation()
|
||||
if (hint.rawText) {
|
||||
// Replace the variable names used in the hint with the ones used by the player
|
||||
// variable names are marked like `«{g}»` inside the text.
|
||||
return t(hint.rawText, {ns: gameId}).replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
|
||||
// `hint.varNames` contains tuples `[oldName, newName]`
|
||||
(hint.varNames.find(x => x[0] == v))[1]))
|
||||
} else {
|
||||
// hints created in the frontend do not have a `rawText`
|
||||
// TODO: `hint.text` could be removed in theory.
|
||||
return t(hint.text, {ns: gameId})
|
||||
}
|
||||
}
|
||||
|
||||
export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
|
||||
return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
|
||||
<Markdown>{getHintText(hint)}</Markdown>
|
||||
</div>
|
||||
}
|
||||
|
||||
export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
|
||||
return <div className={`message warning step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
|
||||
<Markdown>{getHintText(hint)}</Markdown>
|
||||
</div>
|
||||
}
|
||||
|
||||
export function Hints({hints, showHidden, step, selected, toggleSelection, lastLevel} : {hints: GameHint[], showHidden: boolean, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
|
||||
if (!hints) {return <></>}
|
||||
const openHints = hints.filter(hint => !hint.hidden)
|
||||
const hiddenHints = hints.filter(hint => hint.hidden)
|
||||
|
||||
// TODO: Should not use index as key.
|
||||
return <>
|
||||
{openHints.map((hint, j) => <Hint key={`hint-${step}-${j}`} hint={hint} step={step} selected={selected} toggleSelection={toggleSelection} lastLevel={lastLevel} />)}
|
||||
{showHidden && hiddenHints.map((hint, j) => <HiddenHint key={`hidden-hint-${step}-${j}`} hint={hint} step={step} selected={selected} toggleSelection={toggleSelection} lastLevel={lastLevel} />)}
|
||||
</>
|
||||
}
|
||||
|
||||
export function DeletedHint({hint} : {hint: GameHint}) {
|
||||
return <div className="message information deleted-hint">
|
||||
<Markdown>{getHintText(hint)}</Markdown>
|
||||
</div>
|
||||
}
|
||||
|
||||
export function DeletedHints({hints} : {hints: GameHint[]}) {
|
||||
|
||||
const openHints = hints.filter(hint => !hint.hidden)
|
||||
const hiddenHints = hints.filter(hint => hint.hidden)
|
||||
|
||||
// TODO: Should not use index as key.
|
||||
return <>
|
||||
{openHints.map((hint, i) => <DeletedHint key={`deleted-hint-${i}`} hint={hint} />)}
|
||||
{hiddenHints.map((hint, i) => <DeletedHint key={`deleted-hidden-hint-${i}`} hint={hint}/>)}
|
||||
</>
|
||||
}
|
||||
|
||||
/** Filter hints to not show consequtive identical hints twice.
|
||||
* Hidden hints are not filtered.
|
||||
*/
|
||||
export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
|
||||
if (!hints) {
|
||||
return []}
|
||||
else if (!prevHints) {
|
||||
return hints }
|
||||
else {
|
||||
return hints.filter((hint) => hint.hidden ||
|
||||
(prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
|
||||
return step?.goals[0]?.hints.some((hint) => hint.hidden)
|
||||
}
|
||||
|
||||
|
||||
export function MoreHelpButton({selected=null} : {selected?: number}) {
|
||||
|
||||
const { t } = useTranslation()
|
||||
|
||||
const {proof, setProof} = React.useContext(ProofContext)
|
||||
const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
|
||||
|
||||
let k = proof?.steps.length ?
|
||||
((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected)
|
||||
: 0
|
||||
|
||||
const activateHiddenHints = (ev) => {
|
||||
// If the last step (`k`) has errors, we want the hidden hints from the
|
||||
// second-to-last step to be affected
|
||||
if (!(proof?.steps.length)) {return}
|
||||
|
||||
// state must not be mutated, therefore we need to clone the set
|
||||
let tmp = new Set(showHelp)
|
||||
if (tmp.has(k)) {
|
||||
tmp.delete(k)
|
||||
} else {
|
||||
tmp.add(k)
|
||||
}
|
||||
setShowHelp(tmp)
|
||||
console.debug(`help: ${Array.from(tmp.values())}`)
|
||||
}
|
||||
|
||||
if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
|
||||
return <Button to="" onClick={activateHiddenHints}>
|
||||
{t("Show more help!")}
|
||||
</Button>
|
||||
}
|
||||
}
|
||||
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,19 @@
|
||||
import * as React from 'react';
|
||||
import ReactMarkdown from 'react-markdown';
|
||||
import remarkMath from 'remark-math'
|
||||
import rehypeKatex from 'rehype-katex'
|
||||
import 'katex/dist/katex.min.css' // `rehype-katex` does not import the CSS for you
|
||||
import gfm from "remark-gfm";
|
||||
|
||||
function Markdown(props) {
|
||||
const newProps = {
|
||||
...props,
|
||||
remarkPlugins: [...props.remarkPlugins ?? [], remarkMath, gfm],
|
||||
rehypePlugins: [...props.remarkPlugins ?? [], rehypeKatex],
|
||||
};
|
||||
return (
|
||||
<ReactMarkdown {...newProps} className="markdown" />
|
||||
);
|
||||
}
|
||||
|
||||
export default Markdown
|
||||
@ -1,363 +0,0 @@
|
||||
import * as React from 'react'
|
||||
import { createContext, useContext, useState } from 'react'
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
|
||||
import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
|
||||
faArrowRight, faArrowLeft, faXmark, faBars, faCode,
|
||||
faCircleInfo, faTerminal, faGear, IconDefinition, faShield } from '@fortawesome/free-solid-svg-icons'
|
||||
import { GameIdContext, PageContext, PreferencesContext } from "../state/context"
|
||||
import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'
|
||||
import { downloadProgress } from './popup/erase'
|
||||
import { useTranslation } from 'react-i18next'
|
||||
import '../css/navigation.css'
|
||||
import { PopupContext } from './popup/popup'
|
||||
import { useSelector } from 'react-redux'
|
||||
import { selectCompleted, selectDifficulty, selectProgress, selectReadIntro } from '../state/progress'
|
||||
import lean4gameConfig from '../config.json'
|
||||
import { Flag } from './flag'
|
||||
import { useAppSelector } from '../hooks'
|
||||
|
||||
/** SVG github icon */
|
||||
function GithubIcon () {
|
||||
return <svg className="svg-inline--fa" height="24" aria-hidden="true" viewBox="0 0 16 16" version="1.1" width="24" >
|
||||
<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 button to appear in the navigation (both, top bar or dropdown). */
|
||||
export const NavButton: React.FC<{
|
||||
icon?: IconDefinition
|
||||
iconElement?: JSX.Element
|
||||
text?: string
|
||||
onClick?: React.MouseEventHandler<HTMLAnchorElement>
|
||||
title?: string
|
||||
href?: string
|
||||
inverted?: boolean
|
||||
disabled?: boolean
|
||||
className?: string
|
||||
}> = ({icon, iconElement, text, onClick=()=>{}, title, href=null, inverted=false, disabled=false, className=''}) => {
|
||||
return <a className={`${className} nav-button btn${inverted?' btn-inverted':''}${disabled?' btn-disabled':''}`} onClick={disabled?null:onClick} href={disabled?null:href} title={title}>
|
||||
{iconElement ?? (icon && <FontAwesomeIcon icon={icon} />)}{text && <> {text}</>}
|
||||
</a>
|
||||
}
|
||||
|
||||
/** Context which manages the dropdown navigation */
|
||||
const NavigationContext = createContext<{
|
||||
navOpen: boolean,
|
||||
setNavOpen: React.Dispatch<React.SetStateAction<boolean>>
|
||||
}>({navOpen: false, setNavOpen: () => {}})
|
||||
|
||||
/** Content of the navigation during game selection. */
|
||||
function NavigationLandingPage () {
|
||||
return <div className="nav-content">
|
||||
<div className="nav-title-left"></div>
|
||||
<div className="nav-title-middle"></div>
|
||||
<div className="nav-title-right"></div>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** Content of the navigation on Desktop during world selection. */
|
||||
function DesktopNavigationOverview () {
|
||||
const { t } = useTranslation()
|
||||
const { gameId } = useContext(GameIdContext)
|
||||
const { setPopupContent } = useContext(PopupContext)
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
|
||||
return <div className="nav-content">
|
||||
<div className="nav-title-left">
|
||||
<NavButton
|
||||
text={t("Rules")}
|
||||
onClick={() => {setPopupContent("rules")}}
|
||||
inverted={true} />
|
||||
</div>
|
||||
<div className="nav-title-middle">
|
||||
<span className="nav-title">{t(gameInfo.data?.title, {ns: gameId})}</span>
|
||||
</div>
|
||||
<div className="nav-title-right"></div>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** Content of the navigation on Mobile during world selection. */
|
||||
function MobileNavigationOverview () {
|
||||
const { t } = useTranslation()
|
||||
const {page, setPage} = useContext(PageContext)
|
||||
const { setPopupContent } = useContext(PopupContext)
|
||||
|
||||
const { gameId, worldId } = useContext(GameIdContext)
|
||||
const readIntro = useSelector(selectReadIntro(gameId, worldId))
|
||||
|
||||
return <div className="nav-content">
|
||||
<div className="nav-title-left">
|
||||
<NavButton
|
||||
text={t("Rules")}
|
||||
onClick={() => {setPopupContent("rules")}}
|
||||
inverted={true} />
|
||||
</div>
|
||||
<div className="nav-title-middle">
|
||||
<span className="nav-title">
|
||||
</span>
|
||||
</div>
|
||||
<div className="nav-title-right">
|
||||
{page > 0 &&
|
||||
<NavButton
|
||||
text={page == 1 ? t("Intro") : null}
|
||||
icon={page == 1 ? null : faBookOpen}
|
||||
onClick={() => setPage(page - 1)}
|
||||
inverted={true} />
|
||||
}
|
||||
{ page < 2 &&
|
||||
<NavButton
|
||||
text={(page==0) ? t("Start") : null}
|
||||
icon={(page==0) ? null : faBook}
|
||||
onClick={() => setPage(page+1)}
|
||||
disabled={!readIntro}
|
||||
inverted={true} />
|
||||
}
|
||||
</div>
|
||||
|
||||
</div>
|
||||
}
|
||||
|
||||
/** Content of the navigation on Desktop in a level. */
|
||||
function DesktopNavigationLevel () {
|
||||
const { t } = useTranslation()
|
||||
const { gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
const { typewriterMode, setTypewriterMode, lockEditorMode } = useContext(PageContext)
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
const difficulty = useSelector(selectDifficulty(gameId))
|
||||
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
|
||||
|
||||
const readIntro = useSelector(selectReadIntro(gameId, worldId))
|
||||
|
||||
const worldTitle = gameInfo.data?.worlds.nodes[worldId]?.title
|
||||
const levelTitle = ((levelId == 0) ?
|
||||
t("Introduction") :
|
||||
(
|
||||
t("Level") +
|
||||
` ${levelId}` +
|
||||
(gameInfo.data?.worldSize[worldId] ? ` / ${gameInfo.data?.worldSize[worldId]}` : '') +
|
||||
(levelInfo.data?.title ? ` : ${t(levelInfo?.data?.title, {ns: gameId})}` : '')
|
||||
)
|
||||
)
|
||||
|
||||
return <div className="nav-content">
|
||||
<div className="nav-title-left">
|
||||
<span className="nav-title">{worldTitle ? `${t(worldTitle, {ns: gameId})}` : '' /* ${t("World")}: */ }
|
||||
</span>
|
||||
</div>
|
||||
<div className="nav-title-middle">
|
||||
<span className="nav-title">
|
||||
{ levelTitle
|
||||
}
|
||||
</span>
|
||||
</div>
|
||||
<div className="nav-title-right" >
|
||||
{ levelId > 0 &&
|
||||
<NavButton
|
||||
icon={faArrowLeft}
|
||||
text={t("Previous")}
|
||||
inverted={true}
|
||||
href={`#/${gameId}/world/${worldId}/level/${levelId - 1}`} />
|
||||
}
|
||||
{ levelId == gameInfo.data?.worldSize[worldId] ?
|
||||
<NavButton
|
||||
icon={faHome}
|
||||
text={t("Home")}
|
||||
inverted={true}
|
||||
disabled={levelId > 0 && difficulty == 2 && !completed}
|
||||
href={`#/${gameId}`} /> :
|
||||
<NavButton
|
||||
icon={faArrowRight}
|
||||
text={levelId == 0 ? t("Start") : t("Next")} inverted={true}
|
||||
disabled={levelId == 0 ? !readIntro : (difficulty == 2 && !completed)}
|
||||
href={`#/${gameId}/world/${worldId}/level/${levelId + 1}`} />
|
||||
}
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** Content of the navigation on Mobile in a level. */
|
||||
function MobileNavigationLevel () {
|
||||
const { t } = useTranslation()
|
||||
const {gameId, worldId, levelId} = useContext(GameIdContext)
|
||||
const {page, setPage} = useContext(PageContext)
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
|
||||
let title = worldId ?
|
||||
` ${levelId} / ${gameInfo.data?.worldSize[worldId]}`+ (levelInfo?.data?.title && ` : ${t(levelInfo?.data?.title, {ns: gameId})}`)
|
||||
:
|
||||
''
|
||||
|
||||
return <div className="nav-content">
|
||||
<div className="nav-title-left"></div>
|
||||
<div className="nav-title-middle">
|
||||
<span className="nav-title">
|
||||
{title}
|
||||
</span>
|
||||
</div>
|
||||
<div className="nav-title-right">
|
||||
<NavButton
|
||||
icon={(page == 1) ? faBook : faBookOpen}
|
||||
onClick={() => setPage((page == 1) ? 2 : 1)}
|
||||
inverted={true} />
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** The skeleton of the navigation which is the same across all layouts. */
|
||||
export function Navigation () {
|
||||
const { t, i18n } = useTranslation()
|
||||
const { gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
const { mobile, language, setLanguage } = useContext(PreferencesContext)
|
||||
const { setPopupContent } = useContext(PopupContext)
|
||||
const { typewriterMode, setTypewriterMode, lockEditorMode } = useContext(PageContext)
|
||||
const gameProgress = useSelector(selectProgress(gameId))
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
const difficulty = useSelector(selectDifficulty(gameId))
|
||||
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
|
||||
|
||||
const readIntro = useSelector(selectReadIntro(gameId, worldId))
|
||||
|
||||
const [navOpen, setNavOpen] = useState(false)
|
||||
const [langNavOpen, setLangNavOpen] = useState(false)
|
||||
function toggleNav () {setNavOpen(!navOpen); setLangNavOpen(false)}
|
||||
function toggleLangNav () {setLangNavOpen(!langNavOpen); setNavOpen(false)}
|
||||
|
||||
/** toggle input mode if allowed */
|
||||
function toggleInputMode(ev: React.MouseEvent) {
|
||||
if (!lockEditorMode) {
|
||||
setTypewriterMode(!typewriterMode)
|
||||
console.log('test')
|
||||
}
|
||||
}
|
||||
|
||||
return <nav>
|
||||
<NavigationContext.Provider value={{navOpen, setNavOpen}}>
|
||||
{ gameId && <>
|
||||
<NavButton
|
||||
icon={worldId ? faHome : faGlobe}
|
||||
title={worldId ? t("home") : t("back to games selection")}
|
||||
href={worldId ? `#/${gameId}` : `#`} />
|
||||
</>}
|
||||
{ gameId ?
|
||||
worldId ?
|
||||
(mobile ? <MobileNavigationLevel /> : <DesktopNavigationLevel />) :
|
||||
(mobile ? <MobileNavigationOverview /> : <DesktopNavigationOverview />) :
|
||||
<NavigationLandingPage />
|
||||
}
|
||||
{ !gameId &&
|
||||
<NavButton
|
||||
iconElement={<GithubIcon />}
|
||||
title={t("view the Lean game server on Github")}
|
||||
href='https://github.com/leanprover-community/lean4game' />
|
||||
}
|
||||
{(!gameId || gameInfo.data?.tile?.languages.length > 1) &&
|
||||
// Language button only visible if the game exists in `>1` languages
|
||||
<NavButton
|
||||
iconElement={langNavOpen ? null : <Flag iso={i18n.language} />}
|
||||
icon={langNavOpen ? faXmark : null}
|
||||
title={langNavOpen ? t('close language menu') : t('open language menu')}
|
||||
onClick={toggleLangNav}
|
||||
/>
|
||||
}
|
||||
<NavButton
|
||||
icon={navOpen ? faXmark : faBars}
|
||||
title={navOpen ? t('close menu') : t('open menu')}
|
||||
onClick={toggleNav} />
|
||||
{ langNavOpen &&
|
||||
<div className='dropdown' onClick={toggleLangNav} >
|
||||
{gameId && gameInfo.data?.tile?.languages ?
|
||||
// Show all languages the game is available in
|
||||
gameInfo.data?.tile?.languages.map(iso =>
|
||||
<NavButton
|
||||
key={`lang-selection-${iso}`}
|
||||
iconElement={<Flag iso={iso} />}
|
||||
text={lean4gameConfig.newLanguages[iso]?.name}
|
||||
onClick={() => {setLanguage(iso)}}
|
||||
inverted={true} />) :
|
||||
// Show all languages the interface is available in (e.g. landing page)
|
||||
Object.entries(lean4gameConfig.newLanguages).map(([iso, val]) =>
|
||||
<NavButton
|
||||
key={`lang-selection-${iso}`}
|
||||
iconElement={<Flag iso={iso} />}
|
||||
text={lean4gameConfig.newLanguages[iso]?.name}
|
||||
onClick={() => {setLanguage(iso)}}
|
||||
inverted={true} />)
|
||||
}
|
||||
</div>
|
||||
}
|
||||
{ navOpen &&
|
||||
<div className='dropdown' onClick={toggleNav} >
|
||||
{ gameId && <>
|
||||
{ mobile && (levelId == gameInfo.data?.worldSize[worldId] ?
|
||||
<NavButton
|
||||
icon={faHome}
|
||||
text={t("Home")}
|
||||
inverted={true}
|
||||
disabled={levelId > 0 && difficulty == 2 && !completed}
|
||||
href={`#/${gameId}`} /> :
|
||||
<NavButton
|
||||
icon={faArrowRight}
|
||||
text={levelId == 0 ? t("Start") : t("Next")} inverted={true}
|
||||
disabled={levelId == 0 ? !readIntro : (difficulty == 2 && !completed)}
|
||||
href={`#/${gameId}/world/${worldId}/level/${levelId + 1}`} />
|
||||
)}
|
||||
{mobile && levelId > 0 &&
|
||||
<NavButton
|
||||
icon={faArrowLeft}
|
||||
text={t("Previous")}
|
||||
inverted={true}
|
||||
href={`#/${gameId}/world/${worldId}/level/${levelId - 1}`} />
|
||||
}
|
||||
{ mobile && levelId > 0 &&
|
||||
<NavButton
|
||||
icon={(typewriterMode && !lockEditorMode) ? faCode : faTerminal}
|
||||
inverted={true}
|
||||
text={typewriterMode ? t("Editor Mode") : t("Typewriter Mode")}
|
||||
disabled={levelId == 0 || lockEditorMode}
|
||||
onClick={(ev) => toggleInputMode(ev)}
|
||||
title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} />
|
||||
}
|
||||
<NavButton
|
||||
icon={faCircleInfo}
|
||||
text={t("Game Info")}
|
||||
onClick={() => {setPopupContent("info")}}
|
||||
inverted={true} />
|
||||
<NavButton
|
||||
icon={faEraser}
|
||||
text={t("Erase")}
|
||||
onClick={() => {setPopupContent("erase")}}
|
||||
inverted={true} />
|
||||
<NavButton
|
||||
icon={faDownload}
|
||||
text={t("Download")}
|
||||
onClick={() => {downloadProgress(gameId, gameProgress)}}
|
||||
inverted={true} />
|
||||
<NavButton
|
||||
icon={faUpload}
|
||||
text={t("Upload")}
|
||||
onClick={() => {setPopupContent("upload")}}
|
||||
inverted={true} />
|
||||
</>}
|
||||
<NavButton
|
||||
icon={faCircleInfo}
|
||||
text={t("Impressum")}
|
||||
onClick={() => {setPopupContent("impressum")}}
|
||||
inverted={true} />
|
||||
<NavButton
|
||||
icon={faShield}
|
||||
text={t("Privacy Policy")}
|
||||
onClick={() => {setPopupContent("privacy")}}
|
||||
inverted={true} />
|
||||
<NavButton
|
||||
icon={faGear}
|
||||
text={t("Preferences")}
|
||||
onClick={() => {setPopupContent("preferences")}}
|
||||
inverted={true} />
|
||||
</div>
|
||||
}
|
||||
</NavigationContext.Provider>
|
||||
</nav>
|
||||
}
|
||||
@ -0,0 +1,28 @@
|
||||
/**
|
||||
* @fileOverview
|
||||
*/
|
||||
import * as React from 'react'
|
||||
import { Typography } from '@mui/material'
|
||||
import Markdown from '../markdown'
|
||||
import { useTranslation } from 'react-i18next'
|
||||
import { GameIdContext } from '../../app'
|
||||
|
||||
/** Pop-up that is displaying the Game Info.
|
||||
*
|
||||
* `handleClose` is the function to close it again because it's open/closed state is
|
||||
* controlled by the containing element.
|
||||
*/
|
||||
export function InfoPopup ({info, handleClose}: {info: string, handleClose: () => void}) {
|
||||
let { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
|
||||
return <div className="modal-wrapper">
|
||||
<div className="modal-backdrop" onClick={handleClose} />
|
||||
<div className="modal">
|
||||
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
|
||||
<Typography variant="body1" component="div" className="welcome-text">
|
||||
<Markdown>{t(info, {ns: gameId})}</Markdown>
|
||||
</Typography>
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
@ -1,43 +0,0 @@
|
||||
import * as React from 'react'
|
||||
import { Trans, useTranslation } from 'react-i18next';
|
||||
|
||||
/** Pop-up that is displayed when opening the privacy policy. */
|
||||
export function ImpressumPopup () {
|
||||
let {t, i18n} = useTranslation()
|
||||
|
||||
function content (lng = i18n.language) {
|
||||
const tt = i18n.getFixedT(lng);
|
||||
return <Trans t={tt} >
|
||||
<h2>Impressum</h2>
|
||||
<p>
|
||||
<strong>Contact:</strong><br />
|
||||
Marcus Zibrowius, Jon Eugster<br />
|
||||
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
|
||||
Universitätsstr. 1<br />
|
||||
40225 Düsseldorf<br />
|
||||
Germany<br />
|
||||
+49 211 81-14690<br />
|
||||
<a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team">Contact Details</a>
|
||||
</p>
|
||||
<p>
|
||||
<strong>Legal form:</strong><br />
|
||||
The Heinrich Heine University Düsseldorf is a corporation under public law. It is legally represented by the Rector Prof. Dr. Anja Steinbeck. The responsible supervisory authority is the Ministry of Culture and Science of North Rhine-Westphalia, Völklinger Straße 49, 40221 Düsseldorf.
|
||||
</p>
|
||||
<p>
|
||||
<strong>VAT identification number:</strong><br />
|
||||
according to §27a Sales Tax Act<br />
|
||||
DE 811222416
|
||||
</p>
|
||||
<p><a href="https://www.hhu.de/impressum" target="_blank">Impressum HHU</a></p>
|
||||
</Trans>
|
||||
}
|
||||
|
||||
return <>
|
||||
{i18n.language != 'en' && <>
|
||||
<p><i>(English version below)</i></p>
|
||||
{content()}
|
||||
<hr />
|
||||
</>}
|
||||
{content('en')}
|
||||
</>
|
||||
}
|
||||
@ -1,56 +0,0 @@
|
||||
import * as React from 'react'
|
||||
import { Typography } from '@mui/material'
|
||||
import { Markdown } from '../utils'
|
||||
import { Trans, useTranslation } from 'react-i18next'
|
||||
import { useGetGameInfoQuery } from '../../state/api'
|
||||
import { GameIdContext } from '../../state/context'
|
||||
|
||||
/** Pop-up that is displaying the Game Info.
|
||||
*
|
||||
* `handleClose` is the function to close it again because it's open/closed state is
|
||||
* controlled by the containing element.
|
||||
*/
|
||||
export function InfoPopup () {
|
||||
let { t } = useTranslation()
|
||||
const {gameId} = React.useContext(GameIdContext)
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
|
||||
return <>
|
||||
<Typography variant="body1" component="div" className="welcome-text">
|
||||
<Markdown>{t(gameInfo.data?.info, {ns: gameId})}</Markdown>
|
||||
<hr />
|
||||
<Trans>
|
||||
<h2>Progress saving</h2>
|
||||
<p>
|
||||
The game stores your progress in your local browser storage. If you delete it, your progress will be lost!<br />
|
||||
Warning: In most browsers, deleting cookies will also clear the local storage (or "local site data").
|
||||
Make sure to download your game progress first!
|
||||
</p>
|
||||
<h2>Accessibility</h2>
|
||||
<p>
|
||||
If you experience any accessibilty barriers, please get in contact with us!
|
||||
We are dedicated to address such barriers to the best of our abilities.
|
||||
</p>
|
||||
<h2>Development</h2>
|
||||
<p>The game engine has been created by <strong>Alexander Bentkamp</strong>, <strong>Jon Eugster</strong>.
|
||||
On a prototype by <strong>Patrick Massot</strong>.
|
||||
</p>
|
||||
<p>
|
||||
The source code of this Lean game engine
|
||||
is <a href="https://github.com/leanprover-community/lean4game" target="_blank">available on Github</a>.
|
||||
If you experience any problems, please
|
||||
file an <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">Issue on Github</a> or
|
||||
get directly in contact.
|
||||
</p>
|
||||
<h2>Funding</h2>
|
||||
<p>
|
||||
The game engine has been developed as part of the
|
||||
project <a href="https://hhu-adam.github.io/" target="_blank">ADAM: Anticipating the Digital
|
||||
Age of Mathematics</a> at
|
||||
Heinrich-Heine-Universität Düsseldorf. It is funded by
|
||||
the <i>Stiftung Innovation in der Hochschullehre</i> as part of project <i>Freiraum 2022</i>.
|
||||
</p>
|
||||
</Trans>
|
||||
</Typography>
|
||||
</>
|
||||
}
|
||||
@ -1,58 +0,0 @@
|
||||
import * as React from 'react'
|
||||
import { useContext } from 'react'
|
||||
import { PrivacyPolicyPopup } from './privacy'
|
||||
import { ImpressumPopup } from './impressum'
|
||||
import { InfoPopup } from './info'
|
||||
import { ErasePopup } from './erase'
|
||||
import { PreferencesPopup } from './preferences'
|
||||
import { UploadPopup } from './upload'
|
||||
import { RulesPopup } from './rules'
|
||||
import '../../css/popup.css'
|
||||
import { NavButton } from '../navigation'
|
||||
import { faXmark } from '@fortawesome/free-solid-svg-icons'
|
||||
|
||||
/** The context which manages if a popup is shown.
|
||||
* If `popupContent` is `null`, the popup is closed.
|
||||
*/
|
||||
export const PopupContext = React.createContext<{
|
||||
popupContent: string,
|
||||
setPopupContent: React.Dispatch<React.SetStateAction<string>>
|
||||
}>({
|
||||
popupContent: null,
|
||||
setPopupContent: () => {}
|
||||
})
|
||||
|
||||
/** To create a new Popup, one needs to add its content as `React.JSX.Element` here
|
||||
* and then call `setPopupConent(key)` at the place where to popup should be opened.
|
||||
*
|
||||
* TODO: The drawback of this design is that there is no check for key missmatches.
|
||||
* How could that be achieved?
|
||||
*/
|
||||
export const Popups = {
|
||||
"erase": <ErasePopup />,
|
||||
"impressum": <ImpressumPopup />,
|
||||
"info": <InfoPopup />,
|
||||
"preferences": <PreferencesPopup />,
|
||||
"privacy": <PrivacyPolicyPopup />,
|
||||
"rules": <RulesPopup />,
|
||||
"upload": <UploadPopup />,
|
||||
}
|
||||
|
||||
/** The skeleton for the popups. */
|
||||
export function Popup () {
|
||||
const {popupContent, setPopupContent} = useContext(PopupContext)
|
||||
function closePopup() {
|
||||
setPopupContent(null)
|
||||
}
|
||||
|
||||
return <div className="modal-wrapper">
|
||||
<div className="modal-backdrop" onClick={closePopup} />
|
||||
<div className="modal">
|
||||
{/* <NavButton icon={faXmark}
|
||||
onClick={closePopup}
|
||||
inverted={true} /> */}
|
||||
<div className="codicon codicon-close modal-close" onClick={closePopup}></div>
|
||||
{Popups[popupContent]}
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
@ -1,48 +0,0 @@
|
||||
import * as React from 'react'
|
||||
import { Trans, useTranslation } from 'react-i18next';
|
||||
|
||||
/** Pop-up that is displayed when opening the privacy policy.
|
||||
*
|
||||
* Note: Do not translate the Impressum!
|
||||
*/
|
||||
export function PrivacyPolicyPopup () {
|
||||
let {t, i18n} = useTranslation()
|
||||
function content (lng = i18n.language) {
|
||||
const tt = i18n.getFixedT(lng);
|
||||
return <Trans t={tt} >
|
||||
<h2>Privacy Policy</h2>
|
||||
<p>
|
||||
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 your game progress is stored in the browser
|
||||
as site data. Your game progress is not saved on the server; if you delete
|
||||
your browser storage, it is completely gone.
|
||||
</p>
|
||||
<p>Our server is located in Germany.</p>
|
||||
<p>
|
||||
<strong>Contact:</strong><br />
|
||||
Marcus Zibrowius, Jon Eugster<br />
|
||||
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
|
||||
Universitätsstr. 1<br />
|
||||
40225 Düsseldorf<br />
|
||||
Germany<br />
|
||||
+49 211 81-14690<br />
|
||||
<a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team">Contact Details</a>
|
||||
</p>
|
||||
</Trans>
|
||||
}
|
||||
|
||||
return <>
|
||||
{i18n.language != 'en' && <>
|
||||
<p><i>(English version below)</i></p>
|
||||
{content()}
|
||||
<hr />
|
||||
</>}
|
||||
{content('en')}
|
||||
</>
|
||||
}
|
||||
@ -0,0 +1,61 @@
|
||||
/**
|
||||
* @fileOverview The impressum/privacy policy
|
||||
*/
|
||||
import { faShield } from '@fortawesome/free-solid-svg-icons';
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome';
|
||||
import * as React from 'react'
|
||||
|
||||
/** Pop-up that is displayed when opening the privacy policy.
|
||||
*
|
||||
* `handleClose` is the function to close it again because it's open/closed state is
|
||||
* controlled by the containing element.
|
||||
*
|
||||
* Note: Do not translate the Impressum!
|
||||
*/
|
||||
export function PrivacyPolicyPopup ({handleClose}: {handleClose: () => void}) {
|
||||
return <div className="privacy-policy modal-wrapper">
|
||||
<div className="modal-backdrop" onClick={handleClose} />
|
||||
<div className="modal">
|
||||
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
|
||||
<h2>Privacy Policy & Impressum</h2>
|
||||
<p>
|
||||
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 your game progress is stored in the browser
|
||||
as site data. Your game progress is not saved on the server; if you delete
|
||||
your browser storage, it is completely gone.
|
||||
</p>
|
||||
<p>Our server is located in Germany.</p>
|
||||
<p>
|
||||
<strong>Contact information:</strong><br />
|
||||
Alexander Bentkamp, Jon Eugster<br />
|
||||
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
|
||||
Universitätsstr. 1<br />
|
||||
40225 Düsseldorf<br />
|
||||
Germany<br />
|
||||
+49 211 81-12173<br />
|
||||
<a 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>
|
||||
<h2>Development & Funding</h2>
|
||||
<p>
|
||||
The source code of this Lean game engine
|
||||
is <a href="https://github.com/leanprover-community/lean4game" target="_blank">available on Github</a>.
|
||||
If you experience any problems, please
|
||||
file an <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">Issue on Github</a> or
|
||||
get directly in contact.
|
||||
</p>
|
||||
<p>
|
||||
The game engine has been developed as part of the
|
||||
project <a href="https://hhu-adam.github.io/" target="_blank">ADAM: Anticipating the Digital
|
||||
Age of Mathematics</a> at
|
||||
Heinrich-Heine-Universität Düsseldorf. It is funded by
|
||||
the <i>Stiftung Innovation in der Hochschullehre</i> as part of project <i>Freiraum 2022</i>.
|
||||
</p>
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
@ -1,88 +0,0 @@
|
||||
import { Box, Slider } from '@mui/material'
|
||||
import * as React from 'react'
|
||||
import { Trans, useTranslation } from 'react-i18next'
|
||||
import { changedDifficulty, selectDifficulty } from '../../state/progress'
|
||||
import { useSelector } from 'react-redux'
|
||||
import { useContext } from 'react'
|
||||
import { useAppDispatch } from '../../hooks'
|
||||
import { GameIdContext } from '../../state/context'
|
||||
|
||||
/** Pop-up that is displayed when opening the help explaining the game rules.
|
||||
*
|
||||
*/
|
||||
export function RulesPopup () {
|
||||
const { t } = useTranslation()
|
||||
const { gameId } = useContext(GameIdContext)
|
||||
const difficulty = useSelector(selectDifficulty(gameId))
|
||||
const dispatch = useAppDispatch()
|
||||
|
||||
function label(x : number) {
|
||||
return x == 0 ? t("none") : x == 1 ? t("relaxed") : t("regular")
|
||||
}
|
||||
|
||||
return <>
|
||||
<h2>{t("Game Rules")}</h2>
|
||||
|
||||
{/* <span className="difficulty-label">{t("Rules")}
|
||||
<FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
|
||||
</span> */}
|
||||
<Box className="slider-wrapper">
|
||||
<Slider
|
||||
orientation="horizontal"
|
||||
title={t("Game Rules")}
|
||||
min={0} max={2}
|
||||
aria-label={t("Game Rules")}
|
||||
value={difficulty}
|
||||
marks={[
|
||||
{value: 0, label: label(0)},
|
||||
{value: 1, label: label(1)},
|
||||
{value: 2, label: label(2)}
|
||||
]}
|
||||
valueLabelFormat={label}
|
||||
getAriaValueText={label}
|
||||
valueLabelDisplay="off"
|
||||
onChange={(ev, val: number) => {
|
||||
dispatch(changedDifficulty({game: gameId, difficulty: val}))
|
||||
}}
|
||||
/>
|
||||
</Box>
|
||||
<Trans>
|
||||
<p>
|
||||
Game rules determine if it is allowed to skip levels and if the games runs checks to only
|
||||
allow unlocked tactics and theorems in proofs.
|
||||
</p>
|
||||
<p>
|
||||
Note: "Unlocked" tactics (or theorems) are determined by two things: The set of minimal
|
||||
tactics needed to solve a level, plus any tactics you unlocked in another level. That means
|
||||
if you unlock <code>simp</code> in a level, you can use it henceforth in any level.
|
||||
</p>
|
||||
<p>The options are:</p>
|
||||
</Trans>
|
||||
<table>
|
||||
<thead>
|
||||
<tr>
|
||||
<th scope="col"></th>
|
||||
<th scope="col">{t("levels")}</th>
|
||||
<th scope="col">{t("tactics")}</th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody>
|
||||
<tr>
|
||||
<th scope="row">{t("regular")}</th>
|
||||
<td>🔐</td>
|
||||
<td>🔐</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<th scope="row">{t("relaxed")}</th>
|
||||
<td>🔓</td>
|
||||
<td>🔐</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<th scope="row">{t("none")}</th>
|
||||
<td>🔓</td>
|
||||
<td>🔓</td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
</>
|
||||
}
|
||||
@ -0,0 +1,60 @@
|
||||
/**
|
||||
* @fileOverview
|
||||
*/
|
||||
import * as React from 'react'
|
||||
import { Trans, useTranslation } from 'react-i18next'
|
||||
|
||||
/** Pop-up that is displayed when opening the help explaining the game rules.
|
||||
*
|
||||
* `handleClose` is the function to close it again because it's open/closed state is
|
||||
* controlled by the containing element.
|
||||
*/
|
||||
export function RulesHelpPopup ({handleClose}: {handleClose: () => void}) {
|
||||
const { t } = useTranslation()
|
||||
|
||||
return <div className="privacy-policy modal-wrapper">
|
||||
<div className="modal-backdrop" onClick={handleClose} />
|
||||
<div className="modal">
|
||||
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
|
||||
<h2>{t("Game Rules")}</h2>
|
||||
<Trans>
|
||||
<p>
|
||||
Game rules determine if it is allowed to skip levels and if the games runs checks to only
|
||||
allow unlocked tactics and theorems in proofs.
|
||||
</p>
|
||||
<p>
|
||||
Note: "Unlocked" tactics (or theorems) are determined by two things: The set of minimal
|
||||
tactics needed to solve a level, plus any tactics you unlocked in another level. That means
|
||||
if you unlock <code>simp</code> in a level, you can use it henceforth in any level.
|
||||
</p>
|
||||
<p>The options are:</p>
|
||||
</Trans>
|
||||
<table>
|
||||
<thead>
|
||||
<tr>
|
||||
<th scope="col"></th>
|
||||
<th scope="col">{t("levels")}</th>
|
||||
<th scope="col">{t("tactics")}</th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody>
|
||||
<tr>
|
||||
<th scope="row">{t("regular")}</th>
|
||||
<td>🔐</td>
|
||||
<td>🔐</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<th scope="row">{t("relaxed")}</th>
|
||||
<td>🔓</td>
|
||||
<td>🔐</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<th scope="row">{t("none")}</th>
|
||||
<td>🔓</td>
|
||||
<td>🔓</td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
@ -1,43 +0,0 @@
|
||||
import * as React from 'react'
|
||||
import { Link, LinkProps } from "react-router-dom"
|
||||
import { Box, CircularProgress } from "@mui/material"
|
||||
import ReactMarkdown from 'react-markdown'
|
||||
import remarkMath from 'remark-math'
|
||||
import rehypeKatex from 'rehype-katex'
|
||||
import rehypeRaw from 'rehype-raw'
|
||||
import 'katex/dist/katex.min.css' // `rehype-katex` does not import the CSS for you
|
||||
import gfm from "remark-gfm"
|
||||
|
||||
/** Simple loading icon */
|
||||
export function LoadingIcon () {
|
||||
return <Box display="flex" alignItems="center" justifyContent="center" sx={{ flex: 1, height: "calc(100vh - 64px)" }}>
|
||||
<CircularProgress />
|
||||
</Box>
|
||||
}
|
||||
|
||||
export interface ButtonProps extends LinkProps {
|
||||
disabled?: boolean
|
||||
inverted?: string // Apparently "inverted" in DOM cannot be `boolean` but must be `inverted`
|
||||
}
|
||||
|
||||
|
||||
/** Our own button class */
|
||||
export function Button(props: ButtonProps) {
|
||||
if (props.disabled) {
|
||||
return <span className={`btn btn-disabled ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</span>
|
||||
} else {
|
||||
return <Link className={`btn ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</Link>
|
||||
}
|
||||
}
|
||||
|
||||
/** Spiced-up markdown */
|
||||
export function Markdown(props) {
|
||||
const newProps = {
|
||||
...props,
|
||||
remarkPlugins: [...props.remarkPlugins ?? [], remarkMath, gfm],
|
||||
rehypePlugins: [...props.remarkPlugins ?? [], rehypeKatex, rehypeRaw],
|
||||
};
|
||||
return (
|
||||
<ReactMarkdown {...newProps} className="markdown" />
|
||||
);
|
||||
}
|
||||
@ -0,0 +1,151 @@
|
||||
import * as React from 'react'
|
||||
import { useEffect } from 'react'
|
||||
import Split from 'react-split'
|
||||
import { Box, CircularProgress } from '@mui/material'
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
|
||||
import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
|
||||
|
||||
import { GameIdContext } from '../app'
|
||||
import { useAppDispatch, useAppSelector } from '../hooks'
|
||||
import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
|
||||
import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
|
||||
import { Button } from './button'
|
||||
import { PreferencesContext } from './infoview/context'
|
||||
import { InventoryPanel } from './inventory'
|
||||
import { ErasePopup } from './popup/erase'
|
||||
import { InfoPopup } from './popup/game_info'
|
||||
import { PrivacyPolicyPopup } from './popup/privacy_policy'
|
||||
import { RulesHelpPopup } from './popup/rules_help'
|
||||
import { UploadPopup } from './popup/upload'
|
||||
import { PreferencesPopup} from "./popup/preferences"
|
||||
import { WorldTreePanel } from './world_tree'
|
||||
|
||||
import '../css/welcome.css'
|
||||
import { WelcomeAppBar } from './app_bar'
|
||||
import { Hint } from './hints'
|
||||
import i18next from 'i18next'
|
||||
import { useTranslation } from 'react-i18next'
|
||||
|
||||
|
||||
/** the panel showing the game's introduction text */
|
||||
function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) {
|
||||
const {mobile} = React.useContext(PreferencesContext)
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
|
||||
let { t } = useTranslation()
|
||||
|
||||
const dispatch = useAppDispatch()
|
||||
|
||||
// TODO: I left the setup for splitting up the introduction in place, but if it's not needed
|
||||
// then this can be simplified.
|
||||
|
||||
// let text: Array<string> = introduction.split(/\n(\s*\n)+/)
|
||||
let text: Array<string> = introduction ? [t(introduction, {ns : gameId})] : []
|
||||
|
||||
return <div className="column chat-panel">
|
||||
<div className="chat">
|
||||
{text?.map(((t, i) =>
|
||||
t.trim() ?
|
||||
<Hint key={`intro-p-${i}`}
|
||||
hint={{text: t, hidden: false, rawText: t, varNames: []}}
|
||||
step={0} selected={null} toggleSelection={undefined} />
|
||||
: <></>
|
||||
))}
|
||||
</div>
|
||||
{mobile &&
|
||||
<div className="button-row">
|
||||
<Button className="btn" to=""
|
||||
title="" onClick={() => {
|
||||
setPageNumber(1);
|
||||
dispatch(changedOpenedIntro({game: gameId, openedIntro: true}))
|
||||
}}>
|
||||
Start <FontAwesomeIcon icon={faArrowRight}/>
|
||||
</Button>
|
||||
</div>
|
||||
}
|
||||
</div>
|
||||
}
|
||||
|
||||
/** main page of the game showing among others the tree of worlds/levels */
|
||||
function Welcome() {
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
|
||||
// Load the namespace of the game
|
||||
i18next.loadNamespaces(gameId)
|
||||
|
||||
const {mobile} = React.useContext(PreferencesContext)
|
||||
const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
|
||||
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const inventory = useLoadInventoryOverviewQuery({game: gameId})
|
||||
|
||||
// For mobile only
|
||||
const openedIntro = useAppSelector(selectOpenedIntro(gameId))
|
||||
const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
|
||||
|
||||
// pop-ups
|
||||
const [eraseMenu, setEraseMenu] = React.useState(false)
|
||||
const [impressum, setImpressum] = React.useState(false)
|
||||
const [info, setInfo] = React.useState(false)
|
||||
const [rulesHelp, setRulesHelp] = React.useState(false)
|
||||
const [uploadMenu, setUploadMenu] = React.useState(false)
|
||||
const [preferencesPopup, setPreferencesPopup] = React.useState(false)
|
||||
|
||||
function closeEraseMenu() {setEraseMenu(false)}
|
||||
function closeImpressum() {setImpressum(false)}
|
||||
function closeInfo() {setInfo(false)}
|
||||
function closeRulesHelp() {setRulesHelp(false)}
|
||||
function closeUploadMenu() {setUploadMenu(false)}
|
||||
function closePreferencesPopup() {setPreferencesPopup(false)}
|
||||
function toggleEraseMenu() {setEraseMenu(!eraseMenu)}
|
||||
function toggleImpressum() {setImpressum(!impressum)}
|
||||
function toggleInfo() {setInfo(!info)}
|
||||
function toggleUploadMenu() {setUploadMenu(!uploadMenu)}
|
||||
function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
|
||||
|
||||
// set the window title
|
||||
useEffect(() => {
|
||||
if (gameInfo.data?.title) {
|
||||
window.document.title = gameInfo.data.title
|
||||
}
|
||||
}, [gameInfo.data?.title])
|
||||
|
||||
return gameInfo.isLoading ?
|
||||
<Box display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}>
|
||||
<CircularProgress />
|
||||
</Box>
|
||||
: <>
|
||||
<WelcomeAppBar pageNumber={pageNumber} setPageNumber={setPageNumber} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum}
|
||||
toggleEraseMenu={toggleEraseMenu} toggleUploadMenu={toggleUploadMenu}
|
||||
toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
|
||||
<div className="app-content">
|
||||
{ mobile ?
|
||||
<div className="welcome mobile">
|
||||
{(pageNumber == 0 ?
|
||||
<IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
|
||||
: pageNumber == 1 ?
|
||||
<WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
|
||||
rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
|
||||
:
|
||||
<InventoryPanel levelInfo={inventory?.data} />
|
||||
)}
|
||||
</div>
|
||||
:
|
||||
<Split className="welcome" minSize={0} snapOffset={200} sizes={[25, 50, 25]}>
|
||||
<IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
|
||||
<WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
|
||||
rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
|
||||
<InventoryPanel levelInfo={inventory?.data} />
|
||||
</Split>
|
||||
}
|
||||
</div>
|
||||
{impressum ? <PrivacyPolicyPopup handleClose={closeImpressum} /> : null}
|
||||
{rulesHelp ? <RulesHelpPopup handleClose={closeRulesHelp} /> : null}
|
||||
{eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
|
||||
{uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
|
||||
{info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
|
||||
{preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
|
||||
</>
|
||||
}
|
||||
|
||||
export default Welcome
|
||||
@ -1,99 +0,0 @@
|
||||
.chat {
|
||||
flex: 1;
|
||||
overflow-y: scroll;
|
||||
margin-left: .5em;
|
||||
margin-right: .5em;
|
||||
}
|
||||
|
||||
.chat-panel {
|
||||
padding-top: 0;
|
||||
padding-bottom: 0;
|
||||
overflow: hidden;
|
||||
display: flex;
|
||||
flex-direction: column;
|
||||
|
||||
}
|
||||
|
||||
.button-row {
|
||||
/* width:100%; */
|
||||
/* margin-left: .5em;
|
||||
margin-right: .5em; */
|
||||
min-height: 2.5em;
|
||||
border-top: 0.1em solid #aaa;
|
||||
display: flex;
|
||||
padding-top: .2rem;
|
||||
margin: .5rem;
|
||||
|
||||
}
|
||||
|
||||
.button-row > .btn:not(:last-child), .button-row > .btn-placeholder:not(:last-child) {
|
||||
/* display: block; */
|
||||
margin-right: .2rem;
|
||||
}
|
||||
|
||||
.button-row .btn-placeholder {
|
||||
display: inline-block;
|
||||
flex: 1;
|
||||
margin: 0;
|
||||
}
|
||||
|
||||
.button-row .btn {
|
||||
flex: 1;
|
||||
/* margin-top: 1rem;
|
||||
margin-bottom: 1rem;
|
||||
margin-left: .5rem;
|
||||
margin-right: .5rem; */
|
||||
text-align: center;
|
||||
margin: 0;
|
||||
padding: .5em;
|
||||
}
|
||||
|
||||
|
||||
.message {
|
||||
margin: 10px 0;
|
||||
padding: 5px 10px;
|
||||
border-radius: 3px 3px 3px 3px;
|
||||
}
|
||||
|
||||
.message.information, .message.info, .message.kind-5, .message.kind-3, .message.kind-4 {
|
||||
/* color: #059; */
|
||||
color: #000;
|
||||
background-color: #DDF6FF;
|
||||
}
|
||||
|
||||
.message.warning, .message.kind-2 {
|
||||
color: #9F6000;
|
||||
background-color: #FEEFB3;
|
||||
}
|
||||
|
||||
.message.error, .message.kind-1 {
|
||||
color: #D8000C;
|
||||
background-color: #FFBABA;
|
||||
}
|
||||
|
||||
.message.deleted-hint {
|
||||
background-color: #EEE;
|
||||
color: #777;
|
||||
box-shadow: .0em .0em .5em .2em #EEE;
|
||||
}
|
||||
|
||||
.message.success, , .message.kind-6 {
|
||||
color: #000;
|
||||
background-color: #E5FFDD;
|
||||
}
|
||||
|
||||
.chat .message {
|
||||
margin-left: .5em;
|
||||
margin-right: .5em;
|
||||
overflow-x: auto;
|
||||
}
|
||||
|
||||
.chat .recent {
|
||||
box-shadow: .0em .0em .4em .1em #8cbbe9;
|
||||
}
|
||||
|
||||
.chat .selected {
|
||||
/* border: 3px solid #5191d1; */
|
||||
|
||||
box-shadow: .0em .0em .4em .1em var(--clr-primary);
|
||||
}
|
||||
@ -1,27 +0,0 @@
|
||||
.editor-wrapper {
|
||||
flex: 1;
|
||||
position: relative;
|
||||
}
|
||||
|
||||
.editor-wrapper .editor-split {
|
||||
height: 100%;
|
||||
}
|
||||
|
||||
#editor {
|
||||
height: 400px;
|
||||
}
|
||||
|
||||
#infoview {
|
||||
height: 400px;
|
||||
}
|
||||
|
||||
#infoview iframe {
|
||||
width: 100%;
|
||||
height: 95%; /* TODO: setting this to 100% makes it a few pixels too high... */
|
||||
border: unset;
|
||||
}
|
||||
|
||||
/* .typewriter {
|
||||
background-color: lightpink;
|
||||
min-height: 400px;
|
||||
} */
|
||||
@ -1,60 +0,0 @@
|
||||
#error-page {
|
||||
height: 100vh;
|
||||
background-image: url("/RoboSurprised.png");
|
||||
background-repeat: no-repeat;
|
||||
background-size: contain;
|
||||
background-position: right bottom;
|
||||
}
|
||||
|
||||
/* these colours are matching the ones of `.messages.error` */
|
||||
.error-message{
|
||||
border: 2px solid #D8000C;
|
||||
background-color: #FFBABA;
|
||||
border-radius: 1rem;
|
||||
display: inline-block;
|
||||
margin: 3rem;
|
||||
padding-left: 1rem;
|
||||
padding-right: 1rem;
|
||||
/* color: #D8000C; */
|
||||
position: relative;
|
||||
}
|
||||
|
||||
|
||||
.thought-bubble {
|
||||
border: 2px solid #D8000C;
|
||||
background-color: #FFBABA;
|
||||
position: absolute;
|
||||
display: block;
|
||||
}
|
||||
|
||||
.thought-bubble:nth-of-type(1) {
|
||||
bottom: -3.5rem;
|
||||
left: 1rem;
|
||||
border-radius: 1.2rem;
|
||||
width: 2.4rem;
|
||||
height: 2.4rem;
|
||||
}
|
||||
|
||||
.thought-bubble:nth-of-type(2) {
|
||||
bottom: -6rem;
|
||||
left: 2.5rem;
|
||||
border-radius: 1rem;
|
||||
width: 2rem;
|
||||
height: 2rem;
|
||||
}
|
||||
|
||||
.thought-bubble:nth-of-type(3) {
|
||||
bottom: -7.5rem;
|
||||
left: 4.5rem;
|
||||
border-radius: 0.8rem;
|
||||
width: 1.6rem;
|
||||
height: 1.6rem;
|
||||
}
|
||||
|
||||
.thought-bubble:nth-of-type(4) {
|
||||
bottom: -8.2rem;
|
||||
left: 6.8rem;
|
||||
border-radius: 0.6rem;
|
||||
width: 1.4rem;
|
||||
height: 1.4rem;
|
||||
}
|
||||
@ -1,37 +0,0 @@
|
||||
.app-content {
|
||||
height: 100%;
|
||||
flex: 1;
|
||||
min-height: 0;
|
||||
display: flex;
|
||||
}
|
||||
|
||||
.gutter {
|
||||
background-color: #eee;
|
||||
|
||||
background-repeat: no-repeat;
|
||||
background-position: 50%;
|
||||
}
|
||||
|
||||
.gutter.gutter-vertical {
|
||||
background-image: url('data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAB4AAAAFAQMAAABo7865AAAABlBMVEVHcEzMzMzyAv2sAAAAAXRSTlMAQObYZgAAABBJREFUeF5jOAMEEAIEEFwAn3kMwcB6I2AAAAAASUVORK5CYII=');
|
||||
}
|
||||
|
||||
.gutter.gutter-horizontal {
|
||||
background-image: url('data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAUAAAAeCAYAAADkftS9AAAAIklEQVQoU2M4c+bMfxAGAgYYmwGrIIiDjrELjpo5aiZeMwF+yNnOs5KSvgAAAABJRU5ErkJggg==');
|
||||
}
|
||||
|
||||
|
||||
.column {
|
||||
width: 100%;
|
||||
height: 100%;
|
||||
overflow: auto;
|
||||
position: relative;
|
||||
scroll-behavior: smooth;
|
||||
}
|
||||
|
||||
.slider .column {
|
||||
height: 100%;
|
||||
overflow: auto;
|
||||
position: relative;
|
||||
scroll-behavior: smooth;
|
||||
}
|
||||
@ -1,97 +0,0 @@
|
||||
|
||||
nav {
|
||||
flex: 0;
|
||||
background: var(--clr-primary);
|
||||
display: flex;
|
||||
position: relative;
|
||||
flex-direction: row;
|
||||
justify-content: space-between;
|
||||
align-items: center;
|
||||
padding: 1.1em;
|
||||
filter: drop-shadow(0 0 5px rgba(0,0,0,0.5));
|
||||
z-index: 2;
|
||||
}
|
||||
|
||||
.nav-content {
|
||||
flex: 1;
|
||||
display: flex;
|
||||
}
|
||||
|
||||
.nav-content > div {
|
||||
/* border: 1px solid red; */
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
.nav-title-left, .nav-title-right {
|
||||
flex-grow: 0;
|
||||
flex-shrink: 0;
|
||||
display: flex;
|
||||
align-items: center;
|
||||
}
|
||||
|
||||
.nav-title-middle {
|
||||
flex-grow: 1;
|
||||
flex-shrink: 1;
|
||||
margin-left: .5rem;
|
||||
margin-right: .5rem;
|
||||
}
|
||||
|
||||
.nav-title {
|
||||
color: white;
|
||||
font-weight: 500;
|
||||
font-size: 1.3rem;
|
||||
display: inline-block;
|
||||
margin: 0;
|
||||
/* margin: 0 1em; */
|
||||
}
|
||||
|
||||
/* fix to make toggle buttons work */
|
||||
.svg-inline--fa {
|
||||
width: 1em;
|
||||
}
|
||||
|
||||
/* TODO */
|
||||
.nav-button:not(.btn-inverted) {
|
||||
font-size: 1.3rem;
|
||||
}
|
||||
|
||||
.dropdown {
|
||||
z-index: 10;
|
||||
}
|
||||
|
||||
.dropdown {
|
||||
position: absolute;
|
||||
display: flex;
|
||||
flex-direction: column;
|
||||
right: 0;
|
||||
top: 100%;
|
||||
background-color: #fff;
|
||||
z-index: 5;
|
||||
border-top: 1px solid rgba(0, 0, 0, 0.1);
|
||||
border-bottom: 1px solid rgba(0, 0, 0, 0.1);
|
||||
box-shadow: -.1rem .3rem .3rem 0 rgba(0, 0, 0, 0.1);
|
||||
}
|
||||
|
||||
.dropdown .svg-inline--fa {
|
||||
width: 1.8rem;
|
||||
}
|
||||
|
||||
.btn-right {
|
||||
float: right;
|
||||
margin: 0.2rem;
|
||||
}
|
||||
|
||||
.btn-input-mode {
|
||||
position: absolute;
|
||||
right: 0.4rem;
|
||||
z-index: 5;
|
||||
top: 0.4rem;
|
||||
margin: 0;
|
||||
border: 1px solid var(--clr-primary);
|
||||
background-color: #eee;
|
||||
font-size: .7rem;
|
||||
/* box-shadow: .0em .0em .4em .1em var(--clr-primary); */
|
||||
/* box-shadow: -.1rem .3rem .3rem 0 var(--clr-primary); */
|
||||
/* border-top-right-radius: 0;
|
||||
border-bottom-right-radius: 0; */
|
||||
}
|
||||
@ -1,30 +0,0 @@
|
||||
|
||||
/* For the "Rules" popup. */
|
||||
.slider-wrapper {
|
||||
padding-left: 2rem;
|
||||
padding-right: 2rem;
|
||||
padding-top: 1rem;
|
||||
}
|
||||
|
||||
.modal-close {
|
||||
float: right;
|
||||
scale: 2;
|
||||
color: var(--vscode-breadcrumb-foreground);
|
||||
cursor: pointer;
|
||||
}
|
||||
|
||||
.modal-close:hover {
|
||||
float: right;
|
||||
scale: 2;
|
||||
color: var(--vscode-breadcrumb-focusForeground);
|
||||
}
|
||||
|
||||
.modal .nav-button {
|
||||
float: right;
|
||||
font-size: 1.5rem;
|
||||
}
|
||||
|
||||
.settings-buttons .btn {
|
||||
margin-top: 0.2rem;
|
||||
margin-bottom: 0.2rem;
|
||||
}
|
||||
@ -1,9 +0,0 @@
|
||||
# Client
|
||||
|
||||
This document describes features of the frontent/client side.
|
||||
|
||||
|
||||
## URL
|
||||
|
||||
You can add `?lang=de` at the end of the URL to specify the language that should be set. This
|
||||
will change the user's preferred language to the one specified.
|
||||
@ -0,0 +1,78 @@
|
||||
There are multiple ways how to format the text content of your game. Notably Markdown with KaTeX.
|
||||
|
||||
# Escaping
|
||||
Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
|
||||
backslashes, but if you provide text inside a doc comment
|
||||
`/-- -/` (e.g. in the `Statement` description) you do not!
|
||||
|
||||
This means for example you'd write `/-- $\iff$ -/` but `"$\\iff$"`.
|
||||
|
||||
Furthermore, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`.
|
||||
|
||||
# KaTeX
|
||||
|
||||
LaTeX syntax is provided trough the [KaTeX library](https://katex.org). KateX supports most but not all of latex and its packages.
|
||||
See [supported](https://katex.org/docs/supported.html).
|
||||
|
||||
## Examples
|
||||
|
||||
### Commutative diagrams
|
||||
|
||||
Here is an example of how to write a commutative diagram in KaTeX:
|
||||
|
||||
$$
|
||||
\begin{CD}
|
||||
A @>{f}>> B @<{g}<< C \\
|
||||
@V{h}VV @V{i}VV @V{j}VV \\
|
||||
D @<{k}<< E @>{l}>> F \\
|
||||
@A{m}AA @A{n}AA @V{p}VV \\
|
||||
G @<{q}<< H @>{r}>> I
|
||||
\end{CD}
|
||||
$$
|
||||
|
||||
```
|
||||
$$
|
||||
\begin{CD}
|
||||
A @>{f}>> B @<{g}<< C \\
|
||||
@V{h}VV @V{i}VV @V{j}VV \\
|
||||
D @<{k}<< E @>{l}>> F \\
|
||||
@A{m}AA @A{n}AA @V{p}VV \\
|
||||
G @<{q}<< H @>{r}>> I
|
||||
\end{CD}
|
||||
$$
|
||||
```
|
||||
|
||||
Again, note that inside a string like `Hint`/`Introduction`/`Conclusion`/etc. you need to escape `\` and potentially `{`.
|
||||
|
||||
E.g. `\begin` as `\\begin`, `\\` as `\\\\` and inside a
|
||||
`Hint`, `@>{f}>>` as `@>\{f}>>`.
|
||||
|
||||
See https://www.jmilne.org/not/Mamscd.pdf
|
||||
|
||||
### Truth Tables
|
||||
|
||||
KaTeX does not support the tabular environment. You can use the array environment instead.
|
||||
|
||||
$$
|
||||
\begin{array}{|c|c|}
|
||||
\hline
|
||||
P & ¬P \\
|
||||
\hline
|
||||
T & F \\
|
||||
F & T \\
|
||||
\hline
|
||||
\end{array}
|
||||
$$
|
||||
|
||||
```
|
||||
$$
|
||||
\begin{array}{|c|c|}
|
||||
\hline
|
||||
P & ¬P \\
|
||||
\hline
|
||||
T & F \\
|
||||
F & T \\
|
||||
\hline
|
||||
\end{array}
|
||||
$$
|
||||
```
|
||||
@ -0,0 +1,14 @@
|
||||
services:
|
||||
lean4game:
|
||||
build: .
|
||||
privileged: true # needed to run bubblewrap inside docker
|
||||
environment:
|
||||
- LEAN4GAME_GITHUB_USER=${LEAN4GAME_GITHUB_USER}
|
||||
- LEAN4GAME_GITHUB_TOKEN=${LEAN4GAME_GITHUB_TOKEN}
|
||||
ports:
|
||||
- "8080:8080"
|
||||
volumes:
|
||||
- games_data:/app/games
|
||||
|
||||
volumes:
|
||||
games_data:
|
||||
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,43 @@
|
||||
import time
|
||||
|
||||
def measure_proc_stat() -> dict[str, int]:
|
||||
proc_stat_header = open("/proc/stat", "r").readline()
|
||||
proc_stat = proc_stat_header.split(' ')[2:]
|
||||
proc_stat[-1] = proc_stat[-1].removesuffix('\n')
|
||||
proc_stat = list(map(int, proc_stat))
|
||||
|
||||
proc_stat_dict= {'user': proc_stat[0],
|
||||
'nice': proc_stat[1],
|
||||
'system': proc_stat[2],
|
||||
'idle': proc_stat[3],
|
||||
'iowait': proc_stat[4],
|
||||
'irq': proc_stat[5],
|
||||
'softirq': proc_stat[6],
|
||||
'steal': proc_stat[7],
|
||||
'guest': proc_stat[8],
|
||||
'guest_nice': proc_stat[9]}
|
||||
|
||||
return proc_stat_dict
|
||||
|
||||
if __name__ == "__main__":
|
||||
"""
|
||||
Script emulates htop calculation of CPU at the
|
||||
moment of calling.
|
||||
"""
|
||||
prev = measure_proc_stat()
|
||||
prev_idle = prev.get('idle') + prev.get('iowait')
|
||||
prev_non_idle = prev.get('user') + prev.get('nice') + prev.get('system') + prev.get('irq') + prev.get('softirq') + prev.get('steal')
|
||||
prev_total = prev_idle + prev_non_idle
|
||||
|
||||
time.sleep(0.1)
|
||||
|
||||
curr = measure_proc_stat()
|
||||
curr_idle = curr.get('idle') + curr.get('iowait')
|
||||
curr_non_idle = curr.get('user') + curr.get('nice') + curr.get('system') + curr.get('irq') + curr.get('softirq') + curr.get('steal')
|
||||
curr_total = curr_idle + curr_non_idle
|
||||
|
||||
d_total = curr_total - prev_total
|
||||
d_idle = curr_idle - prev_idle
|
||||
|
||||
cpu_usage = ((d_total - d_idle)/d_total)
|
||||
print(cpu_usage)
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue