Compare commits
9
Commits
wasm2
..
v4.5.0-bump
| Author | SHA1 | Date | |
|---|---|---|---|
 Jon Eugster
|
406c2799b1 | ||
|
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
|
||||
|
||||
+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",
|
||||
|
||||
@@ -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": "ee49cf8fada1bf5a15592c399a925c401848227f",
|
||||
"name": "std",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v4.3.0",
|
||||
"inputRev": "v4.5.0-rc1",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"}],
|
||||
"name": "GameServer",
|
||||
|
||||
@@ -1 +1 @@
|
||||
leanprover/lean4:v4.3.0
|
||||
leanprover/lean4:v4.5.0-rc1
|
||||
|
||||
@@ -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