phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge pull request #132 from pitmonticone/main

Browse Source 
Fix typos
This commit is contained in:
TentativeConvert
2023-10-27 09:54:24 +02:00
committed by GitHub
parent 8e4c993bd7 9b8e84cc9c
commit efdc9ee536
8 changed files with 19 additions and 19 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/landing_page.tsx
+1 -1
View File
@@ -164,7 +164,7 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet
a template.
</p>
<p>
There is an option to load and run your own games direclty on the server,
There is an option to load and run your own games directly 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.
doc/DOCUMENTATION.md
+5 -5
View File
@@ -17,7 +17,7 @@ Level 1
Title "The rfl tactic"
```
Note that the levels inside a world must have consequtive numbering starting with `1`. The `Game`
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
@@ -51,7 +51,7 @@ 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 alternativ tactic sequence, which
- `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`
@@ -108,7 +108,7 @@ DisabledTactic tauto
DisabledLemma MyNat.add_zero
```
or specify explicitely which items should be available with
or specify explicitly which items should be available with
```lean
OnlyTactic rw rfl apply
@@ -224,7 +224,7 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
1. **Install Docker and Dev Containers** *(once)*:<br/>
See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
Explicitely this means:
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
@@ -251,7 +251,7 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w
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
explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
container. (this will again take some time)
doc/create_game.md
+3 -3
View File
@@ -18,7 +18,7 @@ The file `Game.lean` is the backbone of the game putting everything together.
1. `MakeGame`: This command is where the game gets built. If there are things to fix, they will be shown here as warnings or errors (orange/red squigglies in VSCode). Note that you might have to call "Lean: Restart File" (Ctrl+Shift+X) to reload the file and see changes made in other files.
1. `Title`: Set the display title of your game.
1. `Ìntroduction`: This is the text displayed at the beggining next to the world selection tree.
1. `Introduction`: This is the text displayed at the beginning next to the world selection tree.
1. `Info`: This will be displayed in the game's menu as "Game Info". Use it for credits, funding and other meta information about the game.
1. Imports: The file needs to import all world files, which we look at in a second. If you add a new world, remember to import it here!
1. `Dependency`: (optional) This command adds another edge in the world tree. The game computes them automatically based on used tactics/theorems. However, sometimes you need a dependency the game can't compute, for example you explained `≠` in one world and in another world, the user is expected to know it already. The syntax is `Dependency World₁ → World₂ → World₃`.
@@ -209,7 +209,7 @@ 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 alternativ tactic sequence, which
- `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`
@@ -236,7 +236,7 @@ Further, you can choose to hide hints and only have them displayed when the play
Hint (hidden := true) "some hidden hint"
```
Lastly, you should put variable names in hints insid brackets:
Lastly, you should put variable names in hints inside brackets:
```
Hint "now use `rw [{h}]` to use your assumption {h}."
doc/npm_scripts.md
+1 -1
View File
@@ -6,4 +6,4 @@ Internally, websocket requests to `ws://localhost:3000/websockets` will be forwa
* `npm run build`: Build the project in production mode. All assets of the client will be compiled into `client/dist`.
On the server side, the command will set up a docker image containing the Lean server. The two parts can be built separately using `npm run build_client` and `npm run build_server`.
* `npm run production`: Start the project in production mode. This requires that the build script has been run. It will start a server on the port specified in the `PORT` environment variable or by default on `8080`. You can run on a specifiv port by running `PORT=80 npm run production`. The server will serve the files in `client/dist` via http and give access to the bubblewrapped Lean server via the web socket protocol.
* `npm run production`: Start the project in production mode. This requires that the build script has been run. It will start a server on the port specified in the `PORT` environment variable or by default on `8080`. You can run on a specific port by running `PORT=80 npm run production`. The server will serve the files in `client/dist` via http and give access to the bubblewrapped Lean server via the web socket protocol.
doc/running_locally.md
+1 -1
View File
@@ -15,7 +15,7 @@ The recommended option is "VSCode Dev containers" but you may choose any option
1. **Install Docker and Dev Containers** *(once)*:<br/>
See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
Explicitely this means:
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
server/GameServer/Commands.lean
+5 -5
View File
@@ -215,7 +215,7 @@ LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
* The identifier after `in` is the category to group lemmas by (in the Inventory).
* The description is a string supporting Markdown.
Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requries
Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
The lemma/definition to have the same fully qualified name as in mathlib.
-/
elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
@@ -243,7 +243,7 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur
* The string following `as` is the displayed name (in the Inventory).
* The description is a string supporting Markdown.
Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requries
Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
The lemma/definition to have the same fully qualified name as in mathlib.
-/
elab "DefinitionDoc" name:ident "as" displayName:str template:str : command =>
@@ -521,7 +521,7 @@ elab (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(t
let mut strict := false
let mut hidden := false
-- remove spaces at the beginngng of new lines
-- remove spaces at the beginning of new lines
let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do
match m with
| Syntax.node info k args =>
@@ -589,7 +589,7 @@ elab (name := GameServer.Tactic.Hole) "Hole" t:tacticSeq : tactic => do
/--
Iterate recursively through the Syntax, replace `Hole` with `sorry` and remove all
`Hint`/`Branch` occurences.
`Hint`/`Branch` occurrences.
-/
def replaceHoles (tacs : Syntax) : Syntax :=
match tacs with
@@ -603,7 +603,7 @@ where filterArgs (args : List Syntax) : List Syntax :=
-- replace `Hole` with `sorry`.
| Syntax.node info `GameServer.Tactic.Hole _ :: r =>
Syntax.node info `Lean.Parser.Tactic.tacticSorry #[Syntax.atom info "sorry"] :: filterArgs r
-- delete all `Hint` and `Branch` occurences in the middle.
-- delete all `Hint` and `Branch` occurrences in the middle.
| Syntax.node _ `GameServer.Tactic.Hint _ :: _ :: r
| Syntax.node _ `GameServer.Tactic.Branch _ :: _ :: r =>
filterArgs r
server/GameServer/EnvExtensions.lean
+1 -1
View File
@@ -67,7 +67,7 @@ structure InventoryTemplate where
/-- Depends on the type:
* Tactic: the tactic's name
* Lemma: fully qualified lemma name
* Definition: no restrictions (preferrably the definions fully qualified name)
* Definition: no restrictions (preferably the definitions fully qualified name)
-/
name: Name
/-- Only for Lemmas. To sort them into tabs -/
server/GameServer/FileWorker.lean
+2 -2
View File
@@ -292,7 +292,7 @@ where
-- TODO(MH): check for interrupt with increased precision
cancelTk.check
/- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
while prefering newer versions over old ones. The former is necessary because we do
while preferring newer versions over old ones. The former is necessary because we do
not explicitly clear older diagnostics, while the latter is necessary because we do
not guarantee that diagnostics are emitted in order. Specifically, it may happen that
we interrupted this elaboration task right at this point and a newer elaboration task
@@ -300,7 +300,7 @@ where
the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
because we cannot guarantee that no further diagnostics are emitted after clearing
them. -/
-- NOTE(WN): this is *not* redundent even if there are no new diagnostics in this snapshot
-- NOTE(WN): this is *not* redundant even if there are no new diagnostics in this snapshot
-- because empty diagnostics clear existing error/information squiggles. Therefore we always
-- want to publish in case there was previously a message at this position.
publishDiagnostics m snap.diagnostics.toArray ctx.hOut