Compare commits
12
Commits
| Author | SHA1 | Date | |
|---|---|---|---|
 Jon Eugster
|
c533a635c2 | ||
|
Jon Eugster
|
7114a8c4cb | ||
|
Jon Eugster
|
b7eb15184d | ||
 Luke Naylor
|
892c70165a | ||
|
Jon Eugster
|
e579071a3b | ||
|
Jon Eugster
|
8cdac88b5a | ||
|
Jon Eugster
|
7882958f54 | ||
|
Jon Eugster
|
c4f4dbdc6b | ||
|
Jon Eugster
|
5f52e23f29 | ||
|
Jon Eugster
|
b067dea6e7 | ||
|
Jon Eugster
|
4edf67f0d6 | ||
|
Jon Eugster
|
004f81835f |
@@ -1,6 +1,6 @@
|
||||
# Lean 4 Game
|
||||
|
||||
This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
|
||||
This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
|
||||
|
||||
## Creating a Game
|
||||
|
||||
@@ -28,7 +28,9 @@ should be up-to-date:
|
||||
|
||||
### Backend
|
||||
|
||||
not written yet
|
||||
not fully written yet.
|
||||
|
||||
* [Server](doc/DOCUMENTATION.md): describes the server part (i.e. the content of `server/` und `relay/`).
|
||||
|
||||
## Contributing
|
||||
|
||||
@@ -40,7 +42,8 @@ Providing the use access to a Lean instance running on the server is a severe se
|
||||
|
||||
## Credits
|
||||
|
||||
The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
|
||||
The project has pimarily been developed by Alexander Bentkamp and Jon Eugster.
|
||||
|
||||
It is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
|
||||
(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
|
||||
by Kevin Buzzard and Mohammad Pedramfar.
|
||||
The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
|
||||
by Kevin Buzzard and Mohammad Pedramfar, and on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
|
||||
|
||||
@@ -1,93 +0,0 @@
|
||||
var stderrBuffer = ""
|
||||
var messageBuffer = []
|
||||
var initialized = false;
|
||||
var flushing = false;
|
||||
|
||||
var headerMode = true;
|
||||
var header="";
|
||||
var re = /Content-Length: (\d+)\r\n/i;
|
||||
var contentLength = 0;
|
||||
var content = []
|
||||
var utf8decoder = new TextDecoder();
|
||||
|
||||
|
||||
function flushMessageBuffer(){
|
||||
if (initialized && !flushing) {
|
||||
while(messageBuffer.length > 0) {
|
||||
flushing = true;
|
||||
var msg = messageBuffer.shift();
|
||||
console.log(`Send message: ${msg}`);
|
||||
Module.ccall('send_message', 'void', ['string'], [msg]);
|
||||
console.log(`Message done: ${msg}`);
|
||||
}
|
||||
flushing = false;
|
||||
}
|
||||
}
|
||||
|
||||
var Module = {
|
||||
"arguments": ["--worker"],
|
||||
"preRun": [function() {
|
||||
function stdin() {
|
||||
return null;
|
||||
}
|
||||
|
||||
function stdout(asciiCode) {
|
||||
if (headerMode) {
|
||||
header += String.fromCharCode(asciiCode)
|
||||
if (header.endsWith('\r\n\r\n')) {
|
||||
const found = header.match(re)
|
||||
if (found == null) { console.error(`Invalid header: ${header}`) }
|
||||
contentLength = parseInt(found[1])
|
||||
content = []
|
||||
headerMode = false
|
||||
}
|
||||
} else {
|
||||
content.push(asciiCode)
|
||||
if (content.length == contentLength) {
|
||||
const message = utf8decoder.decode(new Uint8Array(content))
|
||||
console.log(`Server: ${message}`)
|
||||
postMessage(message);
|
||||
headerMode = true
|
||||
header = ''
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
function stderr(asciiCode) {
|
||||
stderrBuffer += String.fromCharCode(asciiCode)
|
||||
}
|
||||
|
||||
FS.init(stdin, stdout, stderr);
|
||||
}],
|
||||
"noInitialRun": true,
|
||||
"onRuntimeInitialized": () => {
|
||||
Module.ccall('main', 'void', [], []);
|
||||
initialized = true;
|
||||
if (stderrBuffer !== "") {
|
||||
console.log(stderrBuffer);
|
||||
stderrBuffer = ""
|
||||
}
|
||||
flushMessageBuffer();
|
||||
}
|
||||
};
|
||||
|
||||
importScripts("server.js")
|
||||
|
||||
|
||||
|
||||
onmessage = (ev) => {
|
||||
console.log(`Client: ${ev.data}`)
|
||||
messageBuffer.push(ev.data);
|
||||
flushMessageBuffer();
|
||||
}
|
||||
|
||||
setInterval(() => {
|
||||
if (stderrBuffer !== "") {
|
||||
console.log(stderrBuffer);
|
||||
stderrBuffer = ""
|
||||
}
|
||||
}, 1000)
|
||||
|
||||
setTimeout(() =>{
|
||||
|
||||
},2000)
|
||||
@@ -1,339 +0,0 @@
|
||||
import { DataCallback, AbstractMessageReader, MessageReader } from 'vscode-jsonrpc/lib/common/messageReader.js';
|
||||
|
||||
import { Message } from 'vscode-jsonrpc/lib/common/messages.js';
|
||||
import { AbstractMessageWriter, MessageWriter } from 'vscode-jsonrpc/lib/common/messageWriter.js';
|
||||
import { Emitter } from 'vscode-jsonrpc/lib/common/events.js';
|
||||
import { Disposable, IWebSocket } from 'vscode-ws-jsonrpc/.';
|
||||
|
||||
declare var IO: any;
|
||||
|
||||
export class WasmWriter implements MessageWriter {
|
||||
protected errorCount = 0;
|
||||
errorEmitter
|
||||
closeEmitter
|
||||
constructor(private worker: Worker) {
|
||||
this.errorEmitter = new Emitter()
|
||||
this.closeEmitter = new Emitter()
|
||||
}
|
||||
dispose() {
|
||||
this.errorEmitter.dispose();
|
||||
this.closeEmitter.dispose();
|
||||
}
|
||||
get onError() {
|
||||
return this.errorEmitter.event;
|
||||
}
|
||||
fireError(error, message, count) {
|
||||
this.errorEmitter.fire([this.asError(error), message, count]);
|
||||
}
|
||||
get onClose() {
|
||||
return this.closeEmitter.event;
|
||||
}
|
||||
fireClose() {
|
||||
this.closeEmitter.fire(undefined);
|
||||
}
|
||||
asError(error) {
|
||||
if (error instanceof Error) {
|
||||
return error;
|
||||
}
|
||||
else {
|
||||
return new Error(`Writer received error. Reason: ${error.message}`);
|
||||
}
|
||||
}
|
||||
|
||||
end(): void {
|
||||
}
|
||||
|
||||
async write(msg: Message): Promise<void> {
|
||||
try {
|
||||
const content = JSON.stringify(msg);
|
||||
this.worker.postMessage(content)
|
||||
} catch (e) {
|
||||
this.errorCount++;
|
||||
this.fireError(e, msg, this.errorCount);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
export class WasmReader implements MessageReader {
|
||||
protected state: 'initial' | 'listening' | 'closed' = 'initial';
|
||||
protected callback: DataCallback | undefined;
|
||||
protected readonly events: { message?: any, error?: any }[] = [];
|
||||
|
||||
constructor(private worker: Worker) {
|
||||
this.worker.onmessage = (ev) => {
|
||||
this.readMessage(ev.data)
|
||||
}
|
||||
// this.socket.onMessage(message =>
|
||||
// this.readMessage(message)
|
||||
// );
|
||||
// this.socket.onError(error =>
|
||||
// this.fireError(error)
|
||||
// );
|
||||
// this.socket.onClose((code, reason) => {
|
||||
// if (code !== 1000) {
|
||||
// const error: Error = {
|
||||
// name: '' + code,
|
||||
// message: `Error during socket reconnect: code = ${code}, reason = ${reason}`
|
||||
// };
|
||||
// this.fireError(error);
|
||||
// }
|
||||
// this.fireClose();
|
||||
// });
|
||||
this.errorEmitter = new Emitter()
|
||||
this.closeEmitter = new Emitter()
|
||||
this.partialMessageEmitter = new Emitter()
|
||||
}
|
||||
|
||||
protected errorCount = 0;
|
||||
errorEmitter
|
||||
closeEmitter
|
||||
partialMessageEmitter
|
||||
|
||||
dispose() {
|
||||
this.errorEmitter.dispose();
|
||||
this.closeEmitter.dispose();
|
||||
}
|
||||
get onError() {
|
||||
return this.errorEmitter.event;
|
||||
}
|
||||
get onClose() {
|
||||
return this.closeEmitter.event;
|
||||
}
|
||||
get onPartialMessage() {
|
||||
return this.partialMessageEmitter.event;
|
||||
}
|
||||
firePartialMessage(info) {
|
||||
this.partialMessageEmitter.fire(info);
|
||||
}
|
||||
asError(error) {
|
||||
if (error instanceof Error) {
|
||||
return error;
|
||||
}
|
||||
else {
|
||||
return new Error(`Reader received error. Reason: ${error.message ? error.message : 'unknown'}`);
|
||||
}
|
||||
}
|
||||
|
||||
listen(callback: DataCallback): Disposable {
|
||||
if (this.state === 'initial') {
|
||||
this.state = 'listening';
|
||||
this.callback = callback;
|
||||
while (this.events.length !== 0) {
|
||||
const event = this.events.pop()!;
|
||||
if (event.message) {
|
||||
this.readMessage(event.message);
|
||||
} else if (event.error) {
|
||||
this.fireError(event.error);
|
||||
} else {
|
||||
this.fireClose();
|
||||
}
|
||||
}
|
||||
}
|
||||
return {
|
||||
dispose: () => {
|
||||
if (this.callback === callback) {
|
||||
this.callback = undefined;
|
||||
}
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
protected readMessage(message: any): void {
|
||||
if (this.state === 'initial') {
|
||||
this.events.splice(0, 0, { message });
|
||||
} else if (this.state === 'listening') {
|
||||
try {
|
||||
const data = JSON.parse(message);
|
||||
this.callback!(data);
|
||||
} catch (err) {
|
||||
const error: Error = {
|
||||
name: '' + 400,
|
||||
message: `Error during message parsing, reason = ${typeof err === 'object' ? (err as any).message : 'unknown'}`
|
||||
};
|
||||
this.fireError(error);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
protected fireError(error: any): void {
|
||||
if (this.state === 'initial') {
|
||||
this.events.splice(0, 0, { error });
|
||||
} else if (this.state === 'listening') {
|
||||
|
||||
this.errorEmitter.fire(this.asError(error));
|
||||
}
|
||||
}
|
||||
|
||||
protected fireClose(): void {
|
||||
if (this.state === 'initial') {
|
||||
this.events.splice(0, 0, {});
|
||||
} else if (this.state === 'listening') {
|
||||
this.closeEmitter.fire(undefined);
|
||||
}
|
||||
this.state = 'closed';
|
||||
}
|
||||
}
|
||||
export class WebSocketMessageWriter implements MessageWriter {
|
||||
protected errorCount = 0;
|
||||
errorEmitter
|
||||
closeEmitter
|
||||
|
||||
constructor(protected readonly socket: IWebSocket) {
|
||||
this.errorEmitter = new Emitter();
|
||||
this.closeEmitter = new Emitter();
|
||||
}
|
||||
dispose() {
|
||||
this.errorEmitter.dispose();
|
||||
this.closeEmitter.dispose();
|
||||
}
|
||||
get onError() {
|
||||
return this.errorEmitter.event;
|
||||
}
|
||||
fireError(error, message, count) {
|
||||
this.errorEmitter.fire([this.asError(error), message, count]);
|
||||
}
|
||||
get onClose() {
|
||||
return this.closeEmitter.event;
|
||||
}
|
||||
fireClose() {
|
||||
this.closeEmitter.fire(undefined);
|
||||
}
|
||||
asError(error) {
|
||||
if (error instanceof Error) {
|
||||
return error;
|
||||
}
|
||||
else {
|
||||
return new Error(`Writer received error. Reason: ${(error.message) ? error.message : 'unknown'}`);
|
||||
}
|
||||
}
|
||||
end(): void {
|
||||
}
|
||||
|
||||
async write(msg: Message): Promise<void> {
|
||||
console.log("WRITE",msg)
|
||||
try {
|
||||
const content = JSON.stringify(msg);
|
||||
this.socket.send(content);
|
||||
} catch (e) {
|
||||
this.errorCount++;
|
||||
this.fireError(e, msg, this.errorCount);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
export class WebSocketMessageReader implements MessageReader {
|
||||
protected state: 'initial' | 'listening' | 'closed' = 'initial';
|
||||
protected callback: DataCallback | undefined;
|
||||
protected readonly events: { message?: any, error?: any }[] = [];
|
||||
errorEmitter
|
||||
closeEmitter
|
||||
partialMessageEmitter
|
||||
|
||||
constructor(protected readonly socket: IWebSocket) {
|
||||
this.errorEmitter = new Emitter();
|
||||
this.closeEmitter = new Emitter();
|
||||
this.partialMessageEmitter = new Emitter();
|
||||
this.socket.onMessage(message =>{
|
||||
console.log("READ", message)
|
||||
this.readMessage(message)
|
||||
});
|
||||
this.socket.onError(error =>
|
||||
this.fireError(error)
|
||||
);
|
||||
this.socket.onClose((code, reason) => {
|
||||
if (code !== 1000) {
|
||||
const error: Error = {
|
||||
name: '' + code,
|
||||
message: `Error during socket reconnect: code = ${code}, reason = ${reason}`
|
||||
};
|
||||
this.fireError(error);
|
||||
}
|
||||
this.fireClose();
|
||||
});
|
||||
}
|
||||
dispose() {
|
||||
this.errorEmitter.dispose();
|
||||
this.closeEmitter.dispose();
|
||||
}
|
||||
get onError() {
|
||||
return this.errorEmitter.event;
|
||||
}
|
||||
get onClose() {
|
||||
return this.closeEmitter.event;
|
||||
}
|
||||
get onPartialMessage() {
|
||||
return this.partialMessageEmitter.event;
|
||||
}
|
||||
firePartialMessage(info) {
|
||||
this.partialMessageEmitter.fire(info);
|
||||
}
|
||||
asError(error) {
|
||||
if (error instanceof Error) {
|
||||
return error;
|
||||
}
|
||||
else {
|
||||
return new Error(`Reader received error. Reason: ${(error.message) ? error.message : 'unknown'}`);
|
||||
}
|
||||
}
|
||||
|
||||
listen(callback: DataCallback): Disposable {
|
||||
if (this.state === 'initial') {
|
||||
this.state = 'listening';
|
||||
this.callback = callback;
|
||||
while (this.events.length !== 0) {
|
||||
const event = this.events.pop()!;
|
||||
if (event.message) {
|
||||
this.readMessage(event.message);
|
||||
} else if (event.error) {
|
||||
this.fireError(event.error);
|
||||
} else {
|
||||
this.fireClose();
|
||||
}
|
||||
}
|
||||
}
|
||||
return {
|
||||
dispose: () => {
|
||||
if (this.callback === callback) {
|
||||
this.callback = undefined;
|
||||
}
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
protected readMessage(message: any): void {
|
||||
if (this.state === 'initial') {
|
||||
this.events.splice(0, 0, { message });
|
||||
} else if (this.state === 'listening') {
|
||||
try {
|
||||
const data = JSON.parse(message);
|
||||
this.callback!(data);
|
||||
} catch (err) {
|
||||
const error: Error = {
|
||||
name: '' + 400,
|
||||
message: `Error during message parsing, reason = ${typeof err === 'object' ? (err as any).message : 'unknown'}`
|
||||
};
|
||||
this.fireError(error);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
protected fireError(error: any): void {
|
||||
if (this.state === 'initial') {
|
||||
this.events.splice(0, 0, { error });
|
||||
} else if (this.state === 'listening') {
|
||||
this.errorEmitter.fire(this.asError(error));
|
||||
}
|
||||
}
|
||||
|
||||
protected fireClose(): void {
|
||||
if (this.state === 'initial') {
|
||||
this.events.splice(0, 0, {});
|
||||
} else if (this.state === 'listening') {
|
||||
this.closeEmitter.fire(undefined);
|
||||
}
|
||||
this.state = 'closed';
|
||||
}
|
||||
}
|
||||
+53
-321
@@ -1,335 +1,67 @@
|
||||
**NOTE! This document is deprecated! The current documentation is [How To Create A Game](create_game.md)**
|
||||
# Server
|
||||
|
||||
# Creating a game.
|
||||
The server is made out of two parts, named "relay" and "server".
|
||||
|
||||
Ideally one takes the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new game.
|
||||
The former, "relay", is the server which
|
||||
sets up a socket connection to the client, starts the lean servers to work on files and
|
||||
relays messages between the lean server and the client. `index.mjs` is the file that needs to
|
||||
be run, which is done for example using `pm2` or by calling `npm run start_server` or
|
||||
`npm run production`, see more later.
|
||||
|
||||
## Game Structure
|
||||
The latter, "server", is the lean server which has two jobs. For one it produces the "gameserver"
|
||||
executable which is the lean server that handles the files the player plays on. The second job
|
||||
is to provide the lean commands which are used when creating a game. These are located in
|
||||
`Commands.lean`.
|
||||
|
||||
A game consist of worlds which have multiple levels each. In the following we describe how to create a level file and how to combine these into a game.
|
||||
|
||||
### Level
|
||||
## Integration into Games
|
||||
|
||||
A level file is a lean file that imports at least `import GameServer.Commands` and starts with the following Lean commands.
|
||||
Games need the "server" as a lake-dependency, which is done in the game's lakefile.
|
||||
|
||||
A game imports `GameServer.Commands` which provides to all the API required to
|
||||
create a game.
|
||||
|
||||
In particular the lean command `MakeGame` compiles the entire game. Static information is
|
||||
stored as JSON files in `.lake/gamedata` for faster loading, while other data is only
|
||||
saved to lean env-extensions which the lean server has access to after loading the lean file.
|
||||
|
||||
For games to be run successfully, it is important that the "gameserver" executable inside
|
||||
the game's `.lake` folder is actually built.
|
||||
Currently this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`.
|
||||
(both commands are to be executed in the game's directory!)
|
||||
|
||||
## Modifying the server
|
||||
|
||||
### Starting the server
|
||||
|
||||
When using the [manual installation](running_locally.md#manual-installation) you can run the server
|
||||
using
|
||||
|
||||
```lean
|
||||
Game "NNG"
|
||||
World "Addition"
|
||||
Level 1
|
||||
Title "The rfl tactic"
|
||||
```
|
||||
|
||||
Note that the levels inside a world must have consecutive numbering starting with `1`. The `Game`
|
||||
and `World` strings can be anything, see below.
|
||||
|
||||
#### Statement
|
||||
|
||||
The core of a level is the `Statement`, which is the exercise that should be proven.
|
||||
|
||||
```lean
|
||||
/-- For all natural numbers $n$, we have $0 + n = n$. -/
|
||||
@[simp]
|
||||
Statement MyNat.zero_add
|
||||
(n : ℕ) : 0 + n = n := by
|
||||
Hint "You can start a proof by `induction n`."
|
||||
induction n with n hn
|
||||
· Hint "This is the base case."
|
||||
rw [add_zero]
|
||||
rfl
|
||||
· Hint "This is the induction hypothesis"
|
||||
rw [add_succ]
|
||||
Branch
|
||||
simp
|
||||
Hint "A branch is an alternative tactic sequence. Does not need to finish the proof."
|
||||
rw [hn]
|
||||
rfl
|
||||
```
|
||||
|
||||
##### Proof
|
||||
|
||||
The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax.
|
||||
|
||||
There are a few extra tactics that help you structuring the proof:
|
||||
|
||||
- `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
|
||||
the one where `Hint` is placed. For more options about hints, see below.
|
||||
- `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which
|
||||
helps setting `Hints` in different places. The `Branch` does not affect the main
|
||||
proof and does not need to finish any goals.
|
||||
- `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template`
|
||||
will be copied into the editor with all `Hole`s replaced with `sorry`. Note that
|
||||
having a `Template` will force the user to use Editor-mode for this level.
|
||||
|
||||
##### Statement Name (optional)
|
||||
|
||||
If you specify a name (`MyNat.zero_add`), this lemma will be available in future levels.
|
||||
(Note that a future level must also import this level,
|
||||
so that Lean knows about the added statement).
|
||||
|
||||
The name must be *fully qualified*. (TODO: is that still true? Did we implement namespaces?)
|
||||
|
||||
##### Doc Comment (optional)
|
||||
|
||||
There are three places where the documentation comment appears:
|
||||
|
||||
1. as doc comment when hovering over the theorem
|
||||
2. as exercise description at the top of the level: ``Theorem `zero_add`: yada yada.``
|
||||
3. in the inventory. This can be overwritten by using
|
||||
`LemmaDoc MyNat.zero_add "different yada yada"` as one might want to add a more detailed
|
||||
description there including examples etc.
|
||||
|
||||
Both latter points support Markdown (including katex).
|
||||
|
||||
##### Attributes (optional)
|
||||
|
||||
the `@[ attributes ]` prefix should work just like you know it from the `theorem` keyword.
|
||||
|
||||
#### Introduction/Conclusion
|
||||
|
||||
Optionally, you can add an `Introduction "some text"` and `Conclusion "some text"` to your level.
|
||||
The introduction will be shown at the beginning, the conclusion is displayed once the level
|
||||
is solved.
|
||||
|
||||
#### Theorems/Tactics/Definitions
|
||||
|
||||
Only enabled theorems/tactics/definitions (called "items" here) are available in a level.
|
||||
|
||||
To add a new item in a level, you can add
|
||||
|
||||
```lean
|
||||
NewTactic rfl simp
|
||||
NewLemma MyNat.add_zero MyNat.add_succ
|
||||
NewDefinition Nat Pow Mul
|
||||
```
|
||||
|
||||
Once added, items will be available in all future levels/worlds,
|
||||
unless you disable them for a particular level with
|
||||
|
||||
```lean
|
||||
DisabledTactic tauto
|
||||
DisabledLemma MyNat.add_zero
|
||||
```
|
||||
|
||||
or specify explicitly which items should be available with
|
||||
|
||||
```lean
|
||||
OnlyTactic rw rfl apply
|
||||
OnlyLemma MyNat.add_zero
|
||||
```
|
||||
|
||||
Lastly, all items need documentation entries (which are imported in the level),
|
||||
see more about that below. There is also explains the `LemmaTab` keyword.
|
||||
|
||||
### World
|
||||
|
||||
Multiple levels are combined into a world and the worlds are then added to the game. It is recommended that all levels of a world are inside one folder (e.g. `NNG/Levels/Addition/`) and
|
||||
then there is one world file (`NNG/Levels/Addition.lean`) which contains the following
|
||||
|
||||
```lean
|
||||
import NNG.Levels.Addition.Level_1
|
||||
import NNG.Levels.Addition.Level_2
|
||||
|
||||
Game "NNG"
|
||||
World "Addition"
|
||||
Title "Addition World"
|
||||
|
||||
Introduction "some text"
|
||||
```
|
||||
|
||||
The `Title` is the world's display title. The `Introduction` is displayed before loading level 1.
|
||||
Note that all levels of a world should be imported by the world file.
|
||||
|
||||
BUG: A level **must not** be imported in a different world's level. Instead, you have to import an entire world there: `import NNG.Levels.Addition`
|
||||
|
||||
### Game
|
||||
|
||||
The Game itself (i.e. the main file of you lake project, `NNG.lean`) should import all worlds and have the following layout, concluding with `MakeGame`:
|
||||
|
||||
```lean
|
||||
import NNG.Levels.Addition
|
||||
import NNG.Levels.Multiplication
|
||||
import NNG.Levels.Power
|
||||
|
||||
Game "NNG"
|
||||
Title "Natural Number Game"
|
||||
Introduction "some text"
|
||||
|
||||
MakeGame
|
||||
```
|
||||
|
||||
The game will automatically compute the order of the worlds depending on the sample proofs of the Levels (ignoring anything inside a `Branch`). You can add additional dependencies manually by adding `Dependency PowerWorld → ImpossibleWorld` before `MakeGame`.
|
||||
The order of worlds influences which tactics and lemmas will be unlocked in a given level.
|
||||
|
||||
`MakeGame` will display warnings about things in the game that need to be fixed, like missing
|
||||
documentation or if a tactic is never introduced.
|
||||
|
||||
### Documentation
|
||||
|
||||
Each tactic, theorem, or definition (all called items here) that is introduced in the game
|
||||
needs a documentation entry. These are statements of the following form:
|
||||
|
||||
```lean
|
||||
LemmaDoc MyNat.add_squared as "add_squared" in "Pow"
|
||||
"(missing)"
|
||||
|
||||
TacticDoc constructor
|
||||
"(missing)"
|
||||
|
||||
DefinitionDoc One as "1"
|
||||
"(missing)"
|
||||
```
|
||||
|
||||
Notes:
|
||||
|
||||
* The lemma name must be **fully qualified**. The string display name can be arbitrary.
|
||||
* Tactics must have their proper name. use `TacticDoc «have» ""` if it does not work
|
||||
without french quotes.
|
||||
* Definition names can be arbitrary. E.g. I used `DefinitionDoc Symbol.Fun as "fun x ↦ x" "(missing)"` once.
|
||||
|
||||
Moreover, the lemmas are in sorted in tabs (the `in "Pow`) part. In each level file, you
|
||||
can define which tab is open when the level is loaded by adding `LemmaTab "Pow"`.
|
||||
|
||||
There will be features added to get automatic information from mathlib!
|
||||
|
||||
## Escaping
|
||||
(TODO: Move)
|
||||
|
||||
|
||||
Inside the doc comment you don't need to escape the backslashes:
|
||||
|
||||
```lean
|
||||
/-- $\operatorname{succ}(n)$. notation for naturals is `\N`. -/
|
||||
Statement ...
|
||||
```
|
||||
|
||||
However, inside interpolated strings (e.g. in `Hint`, `Introduction` and `Conclusion`)
|
||||
you do need to escape backslashes
|
||||
with `\\` and `{` with `\{`:
|
||||
|
||||
```lean
|
||||
Hint "This code has some $\\operatorname\{succ}(n)$ math. The value of `h` is {h}.
|
||||
Notation for naturals is `\\N`."
|
||||
```
|
||||
|
||||
## Game design
|
||||
Here are some things you should consider designing a new game:
|
||||
|
||||
* A world with more than 16 levels will be displayed with the levels spiraling outwards,
|
||||
it might be desirable to stay below that bound. Above 22 levels the spiral start getting out
|
||||
of control.
|
||||
|
||||
# Running Games Locally
|
||||
|
||||
The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
|
||||
|
||||
## VSCode Dev Containers
|
||||
|
||||
1. **Install Docker and Dev Containers** *(once)*:<br/>
|
||||
See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
|
||||
Explicitly this means:
|
||||
* Install docker engine if you have not yet: [Instructions](https://docs.docker.com/engine/install/).
|
||||
I followed the "Server" instructions for linux.
|
||||
* Note that on Linux you need to add your user to the `docker` group
|
||||
([see instructions](https://docs.docker.com/engine/install/linux-postinstall/)) and probably reboot.
|
||||
* Open the games folder in VSCode: `cd NNG4 && code .` or "Open Folder" within VSCode
|
||||
* a message appears prompting you to install the "Dev Containers" extension (by Microsoft).
|
||||
|
||||
2. **Open Project in Dev Container** *(everytime)*:<br/>
|
||||
Once you have the Dev Containers Extension installed, (re)open the project folder of your game in VSCode.
|
||||
A message appears asking you to "Reopen in Container".
|
||||
|
||||
* The first start will take a while, ca. 2-10 minutes. After the first
|
||||
start this should be very quickly.
|
||||
* Once built, it should open a tab "Simple Browser" inside VSCode displaying
|
||||
the game. (Alternatively, open http://localhost:3000 in your browser).
|
||||
|
||||
3. **Editing Files** *(everytime)*:<br/>
|
||||
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
|
||||
explicitly 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`:
|
||||
```bash
|
||||
curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
|
||||
```
|
||||
then reopen bash and test with `command -v nvm` if it is available (Should print "nvm").
|
||||
|
||||
Now install node:
|
||||
```bash
|
||||
nvm install node
|
||||
```
|
||||
|
||||
Clone the game (e.g. `NNG4` here):
|
||||
```bash
|
||||
git clone https://github.com/hhu-adam/NNG4.git
|
||||
# or: git clone git@github.com:hhu-adam/NNG4.git
|
||||
```
|
||||
|
||||
Download dependencies and build the game:
|
||||
```bash
|
||||
cd NNG4
|
||||
lake update
|
||||
lake exe cache get # if your game depends on mathlib
|
||||
lake build
|
||||
```
|
||||
|
||||
Clone the game repository into a directory next to the game:
|
||||
```bash
|
||||
cd ..
|
||||
git clone https://github.com/leanprover-community/lean4game.git
|
||||
# or: git clone git@github.com:leanprover-community/lean4game.git
|
||||
```
|
||||
The folders `NNG4` and `lean4game` must be in the same directory!
|
||||
|
||||
In `lean4game`, install dependencies:
|
||||
```bash
|
||||
cd lean4game
|
||||
npm install
|
||||
```
|
||||
|
||||
TODO: This is outdated!
|
||||
If you are developing a game other than `Robo` or `NNG4`, adapt the
|
||||
code at the beginning of `lean4game/relay/index.mjs`:
|
||||
```typescript
|
||||
const games = {
|
||||
"g/hhu-adam/robo": {
|
||||
dir: "../../../../Robo",
|
||||
queueLength: 5
|
||||
},
|
||||
"g/hhu-adam/nng4": {
|
||||
dir: "../../../../NNG4",
|
||||
queueLength: 5
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
Run the game:
|
||||
```bash
|
||||
npm start
|
||||
```
|
||||
|
||||
This takes a little time. Eventually, the server is available on http://localhost:3000/
|
||||
and the game is available on http://localhost:3000/#/g/hhu-adam/NNG4.
|
||||
This way any changes to files in `client/` or `relay/` will cause the server to restart automatically.
|
||||
|
||||
### Modifying the GameServer
|
||||
Alternative, you can run `npm run build` followed by the commands
|
||||
|
||||
When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with this
|
||||
setup by setting `export NODE_ENV=development` inside your local game before building it:
|
||||
|
||||
```bash
|
||||
cd NNG4
|
||||
export NODE_ENV=development
|
||||
lake update
|
||||
lake build
|
||||
```
|
||||
This causes lake to search locally for the `GameServer` lake package instead of using the version from github.
|
||||
npm run start_client
|
||||
npm run production
|
||||
```
|
||||
|
||||
(in two separate terminals) to test the production modus of the server. This way it will only
|
||||
change once you build and restart the server.
|
||||
|
||||
### Modifying the lean server
|
||||
|
||||
To test a modified lean server (i.e. content of `server/`), you can use the local dev setup and call
|
||||
`lake update -R -Klean4game.local` in your game followed by `lake build`.
|
||||
This will cause lake to look for the
|
||||
local lean server as a dependency instead of the version it downloaded from git.
|
||||
|
||||
You can play a local game at https://localhost:3000/#/g/local/{FolderName} where you replace `{FolderName}` with the game folder name.
|
||||
|
||||
After modifications in `server/`, you will need to call `lake build gameserver` (called in `server/` or in your game's folder) to rebuild
|
||||
the gameserver executable and
|
||||
`lake build` (called in the game's folder) to rebuild the game.
|
||||
|
||||
+6
-1
@@ -129,6 +129,9 @@ NewLemma Nat.zero_mul
|
||||
NewDefinition Pow
|
||||
```
|
||||
|
||||
**Important:** All commands in this section 6a) expect the `Name` they take as input
|
||||
to be **fully qualified**. For example `NewLemma Nat.zero_mul` and not `NewLemma zero_mul`.
|
||||
|
||||
#### Doc entries
|
||||
|
||||
You'll see a warning about a missing Lemma documentation. You can fix it by adding doc-entries like the following somewhere above it.
|
||||
@@ -182,6 +185,8 @@ The statement is the exercise of the level. the basics work the same as they wou
|
||||
|
||||
You can give your exercise a name: `Statement my_first_exercise (n : Nat) ...`. If you do so, it will be added to the inventory and be available in future levels.
|
||||
|
||||
You can but a `Statement` inside namespaces like you would with `theorem`.
|
||||
|
||||
#### Doc String / Exercise statement
|
||||
|
||||
Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports Latex.
|
||||
@@ -230,7 +235,7 @@ Read [More about Hints](doc/hints.md) for how they work and what the options are
|
||||
### 6. e) Extra: Images
|
||||
You can add images on any layer of the game (i.e. game/world/level). These will be displayed in your game.
|
||||
|
||||
The images need to be placed in `images/` and you need to add a command like `Image "images/path/to/myWorldImage.png"`
|
||||
The images need to be placed in `images/` and you need to add a command like `Image "images/path/to/myWorldImage.png"`
|
||||
in one of the files you created in 2), 3), or 4) (i.e. game/world/level).
|
||||
|
||||
NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world.
|
||||
|
||||
@@ -10,6 +10,8 @@ Statement .... := by
|
||||
...
|
||||
```
|
||||
|
||||
Note that hints are only **context-aware but not history-aware**. In particular they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps placing hints outside the sample solution's proof.
|
||||
|
||||
## 1. When do hints show?
|
||||
|
||||
A hint will be displayed if the player's goal matches the one where the hint was placed in the
|
||||
|
||||
+1
-1
@@ -1,6 +1,6 @@
|
||||
# Publishing games
|
||||
|
||||
You can publish your game on the official (Lean Game Server)[https://adam.math.hhu.de] in a few simple
|
||||
You can publish your game on the official [Lean Game Server](https://adam.math.hhu.de) in a few simple
|
||||
steps.
|
||||
|
||||
## 1. Upload Game to github
|
||||
|
||||
+2
-10
@@ -2,6 +2,8 @@
|
||||
|
||||
The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
|
||||
|
||||
Please also consult the [Troubleshooting Collection](doc/troubleshoot.md), where some known pitfalls are collected.
|
||||
|
||||
There are several options to play a game locally:
|
||||
|
||||
1. VSCode Dev Container: needs `docker` installed on your machine
|
||||
@@ -36,16 +38,6 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta
|
||||
3. **Editing Files** *(everytime)*:<br/>
|
||||
After editing some Lean 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)
|
||||
* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.
|
||||
|
||||
## Codespaces
|
||||
|
||||
You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
|
||||
|
||||
+3
-3
@@ -9,8 +9,8 @@ Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https:
|
||||
|
||||
Then, depending on the setup you use, do one of the following:
|
||||
|
||||
* Dev Container: Rebuild the VSCode Devcontainer.
|
||||
* Local Setup: in your game's folder run the following:
|
||||
* **Dev Container**: Rebuild the VSCode Devcontainer (without Cache!).
|
||||
* **Local Setup**: in your game's folder run the following:
|
||||
```
|
||||
lake update -R
|
||||
lake build
|
||||
@@ -24,7 +24,7 @@ Then, depending on the setup you use, do one of the following:
|
||||
npm install
|
||||
```
|
||||
where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
|
||||
* Gitpod/Codespaces: Create a fresh one
|
||||
* **Gitpod/Codespaces**: Create a fresh one
|
||||
|
||||
This will update your game (and the mathlib version you might be using) to the new lean version.
|
||||
|
||||
|
||||
@@ -33,7 +33,6 @@
|
||||
</p>
|
||||
</div>
|
||||
</noscript>
|
||||
<script src="coi-serviceworker.js"></script>
|
||||
<script type="module" src="/client/src/index.tsx"></script>
|
||||
</body>
|
||||
|
||||
|
||||
Generated
-6
@@ -24,7 +24,6 @@
|
||||
"@types/cytoscape": "^3.19.9",
|
||||
"@types/react-router-dom": "^5.3.3",
|
||||
"@vitejs/plugin-react-swc": "^3.4.0",
|
||||
"coi-serviceworker": "^0.1.7",
|
||||
"cross-env": "^7.0.3",
|
||||
"cytoscape": "^3.23.0",
|
||||
"cytoscape-elk": "^2.1.0",
|
||||
@@ -6534,11 +6533,6 @@
|
||||
"node": ">=6"
|
||||
}
|
||||
},
|
||||
"node_modules/coi-serviceworker": {
|
||||
"version": "0.1.7",
|
||||
"resolved": "https://registry.npmjs.org/coi-serviceworker/-/coi-serviceworker-0.1.7.tgz",
|
||||
"integrity": "sha512-bjSUqEngCPOkErY2vbyWsaIGCNRODYzlNycaREVw5s12/C8SM+RnRUUeX6pZbTtov6C52ZLY/+tvHK+BDxuUuA=="
|
||||
},
|
||||
"node_modules/color-convert": {
|
||||
"version": "1.9.3",
|
||||
"resolved": "https://registry.npmjs.org/color-convert/-/color-convert-1.9.3.tgz",
|
||||
|
||||
@@ -21,7 +21,6 @@
|
||||
"@types/cytoscape": "^3.19.9",
|
||||
"@types/react-router-dom": "^5.3.3",
|
||||
"@vitejs/plugin-react-swc": "^3.4.0",
|
||||
"coi-serviceworker": "^0.1.7",
|
||||
"cross-env": "^7.0.3",
|
||||
"cytoscape": "^3.23.0",
|
||||
"cytoscape-elk": "^2.1.0",
|
||||
|
||||
@@ -28,3 +28,7 @@ do
|
||||
#tar -xvzf $f -C games/${OWNER}/${REPO}
|
||||
unzip -q -o $f -d ${OWNER}/${REPO}
|
||||
done
|
||||
|
||||
# Delete temporary files
|
||||
rm -f tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip
|
||||
rm -fr tmp/${OWNER}_${REPO}_${ARTIFACT_ID}
|
||||
|
||||
@@ -489,6 +489,8 @@ section Initialization
|
||||
return (ctx,
|
||||
{ doc := doc
|
||||
initHeaderStx := headerStx
|
||||
currHeaderStx := headerStx
|
||||
importCachingTask? := none
|
||||
pendingRequests := RBMap.empty
|
||||
rpcSessions := RBMap.empty
|
||||
})
|
||||
|
||||
@@ -4,10 +4,10 @@
|
||||
[{"url": "https://github.com/leanprover/std4.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
|
||||
"rev": "af7f36db6e7e9e395710a70635f915e8e3a0e69b",
|
||||
"name": "std",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v4.3.0",
|
||||
"inputRev": "v4.4.0",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"}],
|
||||
"name": "GameServer",
|
||||
|
||||
@@ -1 +1 @@
|
||||
leanprover/lean4:v4.3.0
|
||||
leanprover/lean4:v4.4.0
|
||||
|
||||
@@ -1,37 +0,0 @@
|
||||
#!/bin/bash
|
||||
|
||||
cd server
|
||||
|
||||
mkdir -p .lake/toolchains
|
||||
if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst ]
|
||||
then
|
||||
wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_wasm32.tar.zst
|
||||
tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_wasm32.tar.zst -C .lake/toolchains
|
||||
fi
|
||||
if [ ! -f .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst ]
|
||||
then
|
||||
wget -P .lake/toolchains https://github.com/leanprover/lean4/releases/download/v4.3.0-rc2/lean-4.3.0-rc2-linux_x86.tar.zst
|
||||
tar --use-compress-program=unzstd -xvf .lake/toolchains/lean-4.3.0-rc2-linux_x86.tar.zst -C .lake/toolchains
|
||||
fi
|
||||
|
||||
# Linking will fail, but that's ok. We only need the c files.
|
||||
.lake/toolchains/lean-4.3.0-rc2-linux_x86/bin/lake build -f=lakefile32.lean
|
||||
|
||||
|
||||
lake build
|
||||
|
||||
|
||||
OUT_DIR=../client/public
|
||||
LEAN_SYSROOT=.lake/toolchains/lean-4.3.0-rc2-linux_wasm32
|
||||
LEAN_LIBDIR=$LEAN_SYSROOT/lib/lean
|
||||
|
||||
emcc -o $OUT_DIR/server.js main.c -I $LEAN_SYSROOT/include -L $LEAN_LIBDIR .lake/build/ir/GameServer/*.c -lInit -lLean -lleancpp -lleanrt \
|
||||
-sFORCE_FILESYSTEM -lnodefs.js -s EXIT_RUNTIME=0 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto \
|
||||
-sPTHREAD_POOL_SIZE_STRICT=2 \
|
||||
--preload-file "${LEAN_SYSROOT}/lib/lean/Init"@/lib/Init \
|
||||
--preload-file "${LEAN_SYSROOT}/lib/lean/Init.olean"@/lib/Init.olean \
|
||||
--preload-file "${LEAN_SYSROOT}/lib/lean/Init.ilean"@/lib/Init.ilean \
|
||||
--preload-file "${LEAN_SYSROOT}/lib/lean/Lean"@/lib/Lean \
|
||||
--preload-file "${LEAN_SYSROOT}/lib/lean/Lean.olean"@/lib/Lean.olean \
|
||||
--preload-file "${LEAN_SYSROOT}/lib/lean/Lean.ilean"@/lib/Lean.ilean \
|
||||
--preload-file "./.lake/build32/lib"@/gamelib
|
||||
Reference in New Issue
Block a user