From b6b31a06ac894b46bae35b6db461bf066ded7b63 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 24 Jul 2024 11:06:16 +0200 Subject: [PATCH 1/6] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 8d7680f..d1b303c 100644 --- a/README.md +++ b/README.md @@ -54,7 +54,7 @@ Providing the use access to a Lean instance running on the server is a severe se ## Credits -The project has pimarily been developed by Alexander Bentkamp and Jon Eugster. +The project has primarily 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/) From 2c22c445b197cace93605398e7ad52fc0833b793 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 24 Jul 2024 11:06:19 +0200 Subject: [PATCH 2/6] Update AbstractCtx.lean --- server/GameServer/AbstractCtx.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/GameServer/AbstractCtx.lean b/server/GameServer/AbstractCtx.lean index ab20709..763fb9d 100644 --- a/server/GameServer/AbstractCtx.lean +++ b/server/GameServer/AbstractCtx.lean @@ -21,7 +21,7 @@ def abstractCtx (goal : MVarId) : MetaM AbstractCtxResult := do def openAbstractCtxResult (res : AbstractCtxResult) (k : Array Expr → Expr → MetaM α) : MetaM α := do let (_mvars, _binderInfo, expr) ← openAbstractMVarsResult res.abstractMVarsResult lambdaLetTelescope (← instantiateMVars expr) k - -- TODO: Unfornately, lambdaLetTelescope does not allow us to provide the number of arguments. + -- TODO: Unfortunately, lambdaLetTelescope does not allow us to provide the number of arguments. -- If the goal is a function, this will not work. end AbstractCtx From 2c1e69611bf19dc58aab67761ba5b755c8c93067 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 24 Jul 2024 11:06:21 +0200 Subject: [PATCH 3/6] Update Commands.lean --- server/GameServer/Commands.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 76544f9..e30c426 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -119,7 +119,7 @@ elab "Languages" t:str* : command => do modifyCurGame fun game => pure {game with tile := {game.tile with languages := t.map (·.getString) |>.toList}} -/-- The Image of the game (optional). TODO: Not impementeds -/ +/-- The Image of the game (optional). TODO: Not implemented -/ elab "CoverImage" t:str : command => do let file := t.getString if not <| ← System.FilePath.pathExists file then @@ -610,7 +610,7 @@ where filterArgs (args : List Syntax) : List Syntax := | Syntax.node _ `GameServer.Tactic.Hint _ :: _ :: r | Syntax.node _ `GameServer.Tactic.Branch _ :: _ :: r => filterArgs r - -- delete `Hint` and `Branch` occurence at the end of the tactic sequence. + -- delete `Hint` and `Branch` occurrence at the end of the tactic sequence. | Syntax.node _ `GameServer.Tactic.Hint _ :: [] | Syntax.node _ `GameServer.Tactic.Branch _ :: [] => [] From 54c1e0dcaff334a019196999eefcbf2d678618af Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 24 Jul 2024 11:06:22 +0200 Subject: [PATCH 4/6] Update FileWorker.lean --- server/GameServer/FileWorker.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index e05915b..dabb2a1 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -187,7 +187,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState : where addMessageByDifficulty (info : SourceInfo) (s : MessageData) := -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors - -- deppending on difficulty. + -- depending on difficulty. let difficulty := workerState.difficulty if difficulty > 0 then addMessage info inputCtx (if difficulty > 1 then .error else .warning) s @@ -383,7 +383,7 @@ def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.Ini -- -- Should we get the diags from there? -- let diag : Array Widget.InteractiveDiagnostic := snap.interactiveDiags.toArray - -- -- Level is completed if there are no errrors or warnings + -- -- Level is completed if there are no errors or warnings -- let completed : Bool := ¬ diag.any (fun d => -- d.severity? == some .error ∨ d.severity? == some .warning) From 9b93e3817dcfe7a7ab15c6fcf35b51287c5dd5a3 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 24 Jul 2024 11:06:24 +0200 Subject: [PATCH 5/6] Update RpcHandlers.lean --- server/GameServer/RpcHandlers.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index e81bce4..ce4e61c 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -231,7 +231,7 @@ def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Proo -- Answer: The last snap only copied the diags from the end of this snap let mut diag : Array InteractiveDiagnostic := snap.interactiveDiags.toArray - -- Level is completed if there are no errrors or warnings + -- Level is completed if there are no errors or warnings let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error) let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning) From f518efc81c7d6a1cd1f305e7bcbbaa6ce33153fc Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 24 Jul 2024 11:06:26 +0200 Subject: [PATCH 6/6] Update LetIntros.lean --- server/GameServer/Tactic/LetIntros.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/GameServer/Tactic/LetIntros.lean b/server/GameServer/Tactic/LetIntros.lean index 473e0b7..ed94df0 100644 --- a/server/GameServer/Tactic/LetIntros.lean +++ b/server/GameServer/Tactic/LetIntros.lean @@ -44,7 +44,7 @@ def _root_.Lean.MVarId.letIntros (mvarId : MVarId) : MetaM (Array FVarId × MVar mvarId.introNP n /-- -`let_intros` introduces all `let` statements that are preceeding the proof. Concretely +`let_intros` introduces all `let` statements that are preceding the proof. Concretely it does a subset of what `intros` does. If names are provided, it will introduce as many `let` statements as there are names.