diff --git a/DOCUMENTATION.md b/DOCUMENTATION.md index 50da568..b1eb73c 100644 --- a/DOCUMENTATION.md +++ b/DOCUMENTATION.md @@ -183,6 +183,16 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w After editing some files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes. +### Errors + +* If you don't get the pop-up, you might have disabled them and you can reenable it by + running the `remote-containers.showReopenInContainerNotificationReset` command in vscode. +* If the starting the container fails, in particular with a message `Error: network xyz not found`, + you might have deleted stuff from docker via your shell. Try deleting the container and image + explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the + container. (this will again take some time) + + ## Without Dev Containers Install `nvm`: ``` diff --git a/client/public/index.html b/client/public/index.html index eac10aa..070b31b 100644 --- a/client/public/index.html +++ b/client/public/index.html @@ -21,6 +21,16 @@ You need to enable JavaScript to use the Lean Game Server, as it is built using React.
+
+ Impressum:
+ Jon Eugster
+ Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf
+ Universitätsstr. 1
+ 40225 Düsseldorf
+ Germany
+ +49 211 81-12173
+ Contact Details
+
{doc.data?.statement}
docstring: {doc.data?.docstring} */}
- {level?.data?.descrFormat}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.
- -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. -
- -Our server is located in Germany.
- -Contact information:
- Jon Eugster
- Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf
- Universitätsstr. 1
- 40225 Düsseldorf
- Germany
- Contact Details
-
-
legal
-notes
-- {nodes[id].data.title ? nodes[id].data.title : id} -
-Editor is starting up...
+Waiting for Lean server to start...
- } else if (serverStoppedResult){ - ret ={serverStoppedResult.message}
{serverStoppedResult.reason}
Waiting for Lean server to start...
+ } else if (serverStoppedResult) { + ret ={serverStoppedResult.message}
{serverStoppedResult.reason}
{title}
} +//+//+//+//
Waiting for Lean server to start...
} + if (serverStoppedResult) { + return{serverStoppedResult.message}
+{serverStoppedResult.reason}
+Level completed! 🎉
: +
+ no goals left
+ This probably means you solved the level with warnings or Lean encountered a parsing error.
+
{title}
} ++++
{doc.data?.statement}
docstring: {doc.data?.docstring} */}
+ - There will be an option to load and run games through the server - directly by specifying a URL, but this is still in development. + There is an option to load and run your own games direclty on the server, + instructions are in the NNG repo. Since this is still in development we'd like to + encourage you to contact us for support creating your own game. The documentation is + not polished yet.
- To add games to this page, you should get in contact as + To add games to this main page, you should get in contact as games will need to be added manually.
+ 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. +
++ 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. +
+Our server is located in Germany.
+
+ Contact information:
+ Jon Eugster
+ Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf
+ Universitätsstr. 1
+ 40225 Düsseldorf
+ Germany
+ +49 211 81-12173
+ Contact Details
+
legal
+notes
++ This Lean game engine has been developed as part of the + project ADAM: Anticipating the Digital + Age of Mathematics at + Heinrich-Heine-Universität Düsseldorf. It is funded by + the Stiftung Innovation in der Hochschullehre as part of project Freiraum 2022. +
+ ++ The source code is available on Github. + If you experience any problems, please + file an Issue on Github or + get directly in contact. +
++ 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 anonymised. +
++ We do not use cookies, but your game progress is stored in the browser storage + as site data. Your game progress is not saved on the server; if you delete + your browser storage, it is completely gone. +
+Our server is located in Germany.
+
+ Contact information:
+ Jon Eugster
+ Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf
+ Universitätsstr. 1
+ 40225 Düsseldorf
+ Germany
+ +49 211 81-12173
+ Contact Details
+
+ {level} +
++ {title ? title : world} +
+