Compare commits
1
Commits
stats
..
bump_v4.8.0
| Author | SHA1 | Date | |
|---|---|---|---|
 Jon Eugster
|
446d0296f0 |
@@ -3,4 +3,3 @@ client/dist
|
||||
games/
|
||||
server/.lake
|
||||
**/.DS_Store
|
||||
logs/
|
||||
|
||||
@@ -54,7 +54,7 @@ Providing the use access to a Lean instance running on the server is a severe se
|
||||
|
||||
## Credits
|
||||
|
||||
The project has primarily been developed by Alexander Bentkamp and Jon Eugster.
|
||||
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/)
|
||||
|
||||
@@ -1,94 +0,0 @@
|
||||
{
|
||||
"Intro": "",
|
||||
"Game Introduction": "",
|
||||
"World selection": "",
|
||||
"Start": "",
|
||||
"Inventory": "",
|
||||
"next level": "",
|
||||
"Next": "",
|
||||
"back to world selection": "",
|
||||
"Leave World": "",
|
||||
"previous level": "",
|
||||
"Previous": "",
|
||||
"Editor mode is enforced!": "",
|
||||
"Editor mode": "",
|
||||
"Typewriter mode": "",
|
||||
"information, Impressum, privacy policy": "",
|
||||
"Preferences": "",
|
||||
"Game Info & Credits": "",
|
||||
"Game Info": "",
|
||||
"Clear Progress": "",
|
||||
"Erase": "",
|
||||
"Download Progress": "",
|
||||
"Download": "",
|
||||
"Load Progress from JSON": "",
|
||||
"Upload": "",
|
||||
"Home": "",
|
||||
"back to games selection": "",
|
||||
"close inventory": "",
|
||||
"show inventory": "",
|
||||
"World": "",
|
||||
"Show more help!": "",
|
||||
"Goal": "",
|
||||
"Objects": "",
|
||||
"Assumptions": "",
|
||||
"Current Goal": "",
|
||||
"Further Goals": "",
|
||||
"No Goals": "",
|
||||
"Loading goal…": "",
|
||||
"Click somewhere in the Lean file to enable the infoview.": "",
|
||||
"Waiting for Lean server to start…": "",
|
||||
"Level completed! 🎉": "",
|
||||
"Level completed with warnings 🎭": "",
|
||||
"Failed command": "",
|
||||
"Retry proof from here": "",
|
||||
"Retry": "",
|
||||
"Active Goal": "",
|
||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "",
|
||||
"Line": "",
|
||||
"Character": "",
|
||||
"Loading messages…": "",
|
||||
"Execute": "",
|
||||
"Tactics": "",
|
||||
"Definitions": "",
|
||||
"Theorems": "",
|
||||
"Not unlocked yet": "",
|
||||
"Not available in this level": "",
|
||||
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "",
|
||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "",
|
||||
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "",
|
||||
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "",
|
||||
"This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "",
|
||||
"Prerequisites": "",
|
||||
"Worlds": "",
|
||||
"Levels": "",
|
||||
"Language": "",
|
||||
"Lean Game Server": "",
|
||||
"Development notes": "",
|
||||
"Adding new games": "",
|
||||
"Funding": "",
|
||||
"Level": "",
|
||||
"Introduction": "",
|
||||
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "",
|
||||
"Delete Progress?": "",
|
||||
"Delete": "",
|
||||
"Download & Delete": "",
|
||||
"Cancel": "",
|
||||
"Mobile": "",
|
||||
"Auto": "",
|
||||
"Desktop": "",
|
||||
"Layout": "",
|
||||
"Always visible": "",
|
||||
"Save my settings (in the browser store)": "",
|
||||
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "",
|
||||
"Game Rules": "",
|
||||
"levels": "",
|
||||
"tactics": "",
|
||||
"regular": "",
|
||||
"relaxed": "",
|
||||
"none": "",
|
||||
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "",
|
||||
"Upload Saved Progress": "",
|
||||
"Load selected file": "",
|
||||
"Rules": ""
|
||||
}
|
||||
@@ -1,7 +1,7 @@
|
||||
{
|
||||
"Tactics": "策略",
|
||||
"Lean Game Server": "LEAN 游戏服务器",
|
||||
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>游戏规则决定是否允许跳过关卡，以及游戏是否只允许在证明中使用已解锁的策略和定理。</p><1>注意：“解锁”的策略（或定理）由两个因素决定：解决关卡所需的最小策略集合，加上你在其他关卡中解锁的任何策略。这意味着，如果你在某个关卡中解锁了<1>simp</1>，你可以在任何关卡中使用它。</1><p>选项有：</p>",
|
||||
"Lean Game Server": "",
|
||||
"<p>Game rules determine if it is allowed to skip levels and if the games runs checks to only allow unlocked tactics and theorems in proofs.</p><1>Note: \"Unlocked\" tactics (or theorems) are determined by two things: The set of minimal tactics needed to solve a level, plus any tactics you unlocked in another level. That means if you unlock <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "<p>游戏规则决定是否允许跳过关卡，以及游戏是否允许在证明中使用未解锁的策略和定理。<p><1>注意：“解锁”的策略（或定理）由两个因素决定：解决关卡所需的最小策略集合，加上你在另一个关卡中解锁的任何策略。这意味着，如果你在某个关卡中解锁了<1>simp</1>，那么你可以在任何关卡中使用它。</1><p>选项是：</p>",
|
||||
"Game Rules": "游戏规则",
|
||||
"levels": "关卡",
|
||||
"tactics": "策略",
|
||||
@@ -20,11 +20,11 @@
|
||||
"Leave World": "离开世界",
|
||||
"previous level": "上一关",
|
||||
"Previous": "上一关",
|
||||
"Editor mode is enforced!": "编辑器模式已启用！",
|
||||
"Editor mode is enforced!": "编辑器模式开启！",
|
||||
"Editor mode": "编辑器模式",
|
||||
"Typewriter mode": "打字机模式",
|
||||
"information, Impressum, privacy policy": "信息、版权说明、隐私政策",
|
||||
"Preferences": "偏好设置",
|
||||
"information, Impressum, privacy policy": "",
|
||||
"Preferences": "",
|
||||
"Game Info & Credits": "游戏信息和荣誉",
|
||||
"Game Info": "游戏信息",
|
||||
"Clear Progress": "清除进度",
|
||||
@@ -43,14 +43,14 @@
|
||||
"Current Goal": "当前目标",
|
||||
"Objects": "对象",
|
||||
"Assumptions": "假设",
|
||||
"Further Goals": "进一步目标",
|
||||
"Further Goals": "Further Goals",
|
||||
"No Goals": "无目标",
|
||||
"Loading goal…": "加载目标中。。。",
|
||||
"Click somewhere in the Lean file to enable the infoview.": "单击 Lean 文件中的某处以启用信息视图。",
|
||||
"Waiting for Lean server to start…": "等待 Lean 服务器启动中…",
|
||||
"Level completed! 🎉": "关卡完成！🎉",
|
||||
"Loading goal…": "加载目标。。。",
|
||||
"Click somewhere in the Lean file to enable the infoview.": "单击Lean文件中的某处以启用信息视图。",
|
||||
"Waiting for Lean server to start…": "等待 Lean 服务器启动。。。",
|
||||
"Level completed! 🎉": "完成关卡！🎉",
|
||||
"Level completed with warnings 🎭": "关卡完成（带有警告） 🎭",
|
||||
"Retry proof from here": "从这里重新尝试证明",
|
||||
"Retry proof from here": "从这里重新试着证明",
|
||||
"Active Goal": "当前目标",
|
||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "程序崩溃！请转到编辑器模式，修复您的证明！最后一次服务器响应：",
|
||||
"Line": "行",
|
||||
@@ -61,35 +61,34 @@
|
||||
"Theorems": "定理",
|
||||
"Not unlocked yet": "尚未解锁",
|
||||
"Not available in this level": "本关卡不提供",
|
||||
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "这是一个为证明助手 <1>Lean</1> <i>(Lean 4)</i> 及其数学库 <5>mathlib</5> 设计的学习游戏库",
|
||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "未加载游戏。访问 <1>http://localhost:3000/#/g/local/FOLDER</1> 从本地文件夹打开游戏。",
|
||||
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "<p>这个服务器部署在我们大学的机器上，运行能力有限，目前估计最多可同时支持约 70 个游戏。我们希望将来能更有效地解决并测试这些限制。</p><1>游戏和基础设施的许多方面仍在开发之中。如果您遇到任何问题，欢迎在 <1>GitHub</1> 上提交问题反馈。</1>",
|
||||
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "<0>如果你打算编写自己的游戏，可以使用 <1>GameSkeleton Github Repo</1> 作为模板，并参阅 <3>如何创建游戏</3>。</0><1>你可以直接将游戏上传至服务器，并通过正确的 URL 进行游戏。上面的 <1>说明</1> 已详细介绍了如何将游戏加载到服务器的步骤。如果你有任何疑问，请随时联系我们。</1><p>本页上的精选游戏都是手动添加的。如果你想添加你的游戏，请与我们联系，我们非常欢迎。</p>",
|
||||
|
||||
"This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "此服务器是 Heinrich-Heine-Universität Düsseldorf 项目 <1>ADAM：预见数学的数字时代</1> 的一部分。",
|
||||
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "",
|
||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "没有加载游戏。使用<1>http://localhost:3000/#/g/local/FOLDER</1>直接从本地文件夹打开游戏。",
|
||||
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "",
|
||||
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "",
|
||||
"This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "",
|
||||
"Prerequisites": "前置条件",
|
||||
"Worlds": "世界",
|
||||
"Worlds": "世界(Worlds)",
|
||||
"Levels": "关卡",
|
||||
"Language": "语言",
|
||||
"Development notes": "开发笔记",
|
||||
"Adding new games": "添加新游戏",
|
||||
"Funding": "资助",
|
||||
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>您确定要永久删除您的游戏进度吗？</p><p>（此操作将删除您的所有证明和收集的定理与策略，但不会影响其他游戏的保存数据。）</p>",
|
||||
"Development notes": "",
|
||||
"Adding new games": "",
|
||||
"Funding": "",
|
||||
"<p>Do you want to delete your saved progress irreversibly?</p><p>(This deletes your proofs and your collected inventory. Saves from other games are not deleted.)</p>": "<p>您是否想要不可逆转地删除您的游戏进度？</p><p>（这将删除您的证明和您收集的定理和策略。其他游戏的进度不会被删除。）</p>",
|
||||
"Delete Progress?": "删除进度？",
|
||||
"Delete": "删除",
|
||||
"Download & Delete": "下载和删除",
|
||||
"Cancel": "取消",
|
||||
"Layout": "布局",
|
||||
"Always visible": "始终可见",
|
||||
"Save my settings (in the browser store)": "保存我的设置（在浏览器中存储）",
|
||||
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>选择一个包含已保存游戏进度的 JSON 文件来加载您的进度。</p><1><0>警告：</0>这将删除您当前的游戏进度！请考虑先<2>下载您当前的进度</2>！</1>",
|
||||
"Save my settings (in the browser store)": "",
|
||||
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "<p>选择一个包含已保存游戏进度的JSON文件来加载您的进度。</p><1><0>警告：</0>这将删除您当前的游戏进度！首先考虑<2>下载您当前的进度</2>！</1>",
|
||||
"Upload Saved Progress": "上传保存的进度",
|
||||
"Load selected file": "加载所选文件",
|
||||
"Mobile": "移动端",
|
||||
"Auto": "自动",
|
||||
"Desktop": "桌面端",
|
||||
"Level": "关卡",
|
||||
"Introduction": "介绍",
|
||||
"Retry": "重试",
|
||||
"Failed command": "命令失败"
|
||||
"Level": "",
|
||||
"Introduction": "",
|
||||
"Retry": "",
|
||||
"Failed command": ""
|
||||
}
|
||||
|
||||
@@ -95,9 +95,6 @@ function LandingPage() {
|
||||
const closePreferencesPopup = () => setPreferencesPopup(false);
|
||||
const togglePreferencesPopup = () => setPreferencesPopup(!preferencesPopup);
|
||||
|
||||
const [usageCPU, setUsageCPU] = React.useState<number>()
|
||||
const [usageMem, setUsageMem] = React.useState<number>()
|
||||
|
||||
const { t, i18n } = useTranslation()
|
||||
|
||||
// Load the namespaces of all games
|
||||
@@ -120,29 +117,6 @@ function LandingPage() {
|
||||
return q.data?.tile
|
||||
})
|
||||
|
||||
/** Parse `games/stats.csv` if present and display server capacity. */
|
||||
React.useEffect(() => {
|
||||
fetch(`${window.location.origin}/data/stats`)
|
||||
.then(response => {if (response.ok) {
|
||||
return response.text() } else {throw ""}})
|
||||
.then(data => {
|
||||
// Parse the CSV content
|
||||
const lines = data.split('\n');
|
||||
const [header, line2] = lines;
|
||||
if (!(header.replace(' ', '').startsWith("CPU,MEM"))) {
|
||||
console.info("Not displaying server stats: received unexpected: ", header)
|
||||
}
|
||||
if (line2) {
|
||||
let values = line2.split(',')
|
||||
setUsageCPU(100 * Number(values[0]));
|
||||
setUsageMem(100 * Number(values[1]));
|
||||
}
|
||||
}).catch(err => {
|
||||
console.info('server stats unavailable')
|
||||
console.debug(err)
|
||||
})
|
||||
}, [])
|
||||
|
||||
return <div className="landing-page">
|
||||
<header style={{backgroundImage: `url(${bgImage})`}}>
|
||||
<nav className="landing-page-nav">
|
||||
@@ -181,18 +155,6 @@ function LandingPage() {
|
||||
))
|
||||
}
|
||||
</div>
|
||||
{ // show server capacity from `games/stats.csv` if present
|
||||
(usageMem >= 0 || usageCPU >= 0 ) &&
|
||||
<section>
|
||||
<div className="wrapper">
|
||||
<h2>{t("Server capacity")}</h2>
|
||||
<p>
|
||||
{ usageMem >= 0 && <> {t("RAM")}: <strong>{usageMem} % </strong> {t("used")}.<br/></> }
|
||||
{ usageCPU >= 0 && <> {t("CPU")}: <strong>{usageCPU} % </strong> {t("used")}. </> }
|
||||
</p>
|
||||
</div>
|
||||
</section>
|
||||
}
|
||||
<section>
|
||||
<div className="wrapper">
|
||||
<h2>{t("Development notes")}</h2>
|
||||
|
||||
@@ -26,11 +26,6 @@
|
||||
"iso": "es",
|
||||
"flag": "ES",
|
||||
"name": "Español"
|
||||
},
|
||||
{
|
||||
"iso": "kr",
|
||||
"flag": "KR",
|
||||
"name": "한국어"
|
||||
}
|
||||
]
|
||||
}
|
||||
|
||||
@@ -18,8 +18,8 @@ export const AUTO_SWITCH_THRESHOLD = 800
|
||||
const initialState: PreferencesState = loadPreferences() ??{
|
||||
layout: "auto",
|
||||
isSavePreferences: false,
|
||||
language: import.meta.env.VITE_CLIENT_DEFAULT_LANGUAGE || "en",
|
||||
};
|
||||
language: "en",
|
||||
}
|
||||
|
||||
export const preferencesSlice = createSlice({
|
||||
name: "preferences",
|
||||
|
||||
+10
-18
@@ -6,11 +6,11 @@ This tutorial walks you through creating a new game for lean4. It covers from wr
|
||||
|
||||
1. Use the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
|
||||
2. Clone the game repo.
|
||||
3. Call `lake update -R && lake build` to build the Lean project.
|
||||
3. Call `lake update && lake exe cache get && lake build` to build the Lean project.
|
||||
|
||||
### Running the game
|
||||
Note that you need to host your game's code on github to publish it online later on. If you only
|
||||
want to play it locally, you can simply clone the NNG repo and start modifying that one.
|
||||
|
||||
Now you can open the game in VSCode (`cd YourGame/` and `code .`), and start modifying it like a regular Lean project. To run the game consult the section "**5. Testing the Game Locally**" below.
|
||||
|
||||
## 2. Game.lean
|
||||
|
||||
@@ -194,7 +194,7 @@ 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. See [LaTeX in Games](latex.md) for more details on formatting.
|
||||
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.
|
||||
|
||||
```lean
|
||||
/-- The exercise statement in natural language using latex: $\iff$. -/
|
||||
@@ -265,21 +265,13 @@ CoverImage "images/cover.png"
|
||||
* `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text.
|
||||
* `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens.
|
||||
|
||||
## 10. Advanced Topics
|
||||
## Further Notes
|
||||
|
||||
### Escaping
|
||||
Here are some random further things you should consider designing a new game:
|
||||
|
||||
Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you
|
||||
* Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you
|
||||
would write `Introduction "some latex here: $\\iff$."` but
|
||||
`/-- some latex here: $\iff$. -/ Statement ...`
|
||||
|
||||
### LaTeX support
|
||||
|
||||
LaTeX is rendered using the [KaTeX library](https://katex.org/),
|
||||
see [Using LaTeX in the Game](latex.md) for details.
|
||||
|
||||
### Number Of Levels Limit
|
||||
|
||||
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 starts getting out
|
||||
of control.
|
||||
* 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 starts getting out
|
||||
of control.
|
||||
|
||||
+28
-12
@@ -49,9 +49,6 @@ Statement .... := by
|
||||
Put variables in the hint text inside brackets like this: `{h}`! This way the server can replace
|
||||
the variable's name with the one the user actually used.
|
||||
|
||||
*Note*: This means you need to escape any other uses of **opening** curly brackets (i.e. `\{`). See also [LaTeX in Games](latex.md) for
|
||||
examples of this.
|
||||
|
||||
For example, if the sample proof contains
|
||||
|
||||
```
|
||||
@@ -87,19 +84,38 @@ create new assumptions.
|
||||
|
||||
## 6. Formatting
|
||||
|
||||
You can use Markdown to format your hints and you can
|
||||
use LaTeX. See [LaTeX in Games](latex.md) for more details.
|
||||
You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$`
|
||||
|
||||
### Images
|
||||
**Escaping**: Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
|
||||
backslashes, but if you provide text inside a doc comment
|
||||
`/-- -/` (e.g. in the `Statement` description) you do not!
|
||||
|
||||
Hints and introductions/conclusions can also contain images.
|
||||
TODO: Write a doc about latex/markdown options available.
|
||||
|
||||
For remote images, simply add:
|
||||
### Commutative diagrams
|
||||
|
||||
Here is an example of how to write a commutative diagram in KaTeX:
|
||||
|
||||
$$
|
||||
\begin{CD}
|
||||
A @>{f}>> B @<{g}<< C \\
|
||||
@V{h}VV @V{i}VV @V{j}VV \\
|
||||
D @<{k}<< E @>{l}>> F \\
|
||||
@A{m}AA @A{n}AA @V{p}VV \\
|
||||
G @<{q}<< H @>{r}>> I
|
||||
\end{CD}
|
||||
$$
|
||||
|
||||
```
|
||||
<img src=\"https://url.com/to/image\"/>
|
||||
$$
|
||||
\\begin{CD}
|
||||
A @>{f}>> B @<{g}<< C \\\\
|
||||
@V{h}VV @V{i}VV @V{j}VV \\\\
|
||||
D @<{k}<< E @>{l}>> F \\\\
|
||||
@A{m}AA @A{n}AA @V{p}VV \\\\
|
||||
G @<{q}<< H @>{r}>> I
|
||||
\\end{CD}
|
||||
$$
|
||||
```
|
||||
|
||||
Local images can currently only be included with a hack:
|
||||
|
||||
Images in the game's `images/` folder will be accessible at `data/g/[user]/[repo]/[image].[png|jpg|…]` and thus can be included as if they were external images.
|
||||
See https://www.jmilne.org/not/Mamscd.pdf
|
||||
|
||||
@@ -1,78 +0,0 @@
|
||||
There are multiple ways how to format the text content of your game. Notably Markdown with KaTeX.
|
||||
|
||||
# Escaping
|
||||
Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
|
||||
backslashes, but if you provide text inside a doc comment
|
||||
`/-- -/` (e.g. in the `Statement` description) you do not!
|
||||
|
||||
This means for example you'd write `/-- $\iff$ -/` but `"$\\iff$"`.
|
||||
|
||||
Furthermore, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`.
|
||||
|
||||
# KaTeX
|
||||
|
||||
LaTeX syntax is provided trough the [KaTeX library](https://katex.org). KateX supports most but not all of latex and its packages.
|
||||
See [supported](https://katex.org/docs/supported.html).
|
||||
|
||||
## Examples
|
||||
|
||||
### Commutative diagrams
|
||||
|
||||
Here is an example of how to write a commutative diagram in KaTeX:
|
||||
|
||||
$$
|
||||
\begin{CD}
|
||||
A @>{f}>> B @<{g}<< C \\
|
||||
@V{h}VV @V{i}VV @V{j}VV \\
|
||||
D @<{k}<< E @>{l}>> F \\
|
||||
@A{m}AA @A{n}AA @V{p}VV \\
|
||||
G @<{q}<< H @>{r}>> I
|
||||
\end{CD}
|
||||
$$
|
||||
|
||||
```
|
||||
$$
|
||||
\begin{CD}
|
||||
A @>{f}>> B @<{g}<< C \\
|
||||
@V{h}VV @V{i}VV @V{j}VV \\
|
||||
D @<{k}<< E @>{l}>> F \\
|
||||
@A{m}AA @A{n}AA @V{p}VV \\
|
||||
G @<{q}<< H @>{r}>> I
|
||||
\end{CD}
|
||||
$$
|
||||
```
|
||||
|
||||
Again, note that inside a string like `Hint`/`Introduction`/`Conclusion`/etc. you need to escape `\` and potentially `{`.
|
||||
|
||||
E.g. `\begin` as `\\begin`, `\\` as `\\\\` and inside a
|
||||
`Hint`, `@>{f}>>` as `@>\{f}>>`.
|
||||
|
||||
See https://www.jmilne.org/not/Mamscd.pdf
|
||||
|
||||
### Truth Tables
|
||||
|
||||
KaTeX does not support the tabular environment. You can use the array environment instead.
|
||||
|
||||
$$
|
||||
\begin{array}{|c|c|}
|
||||
\hline
|
||||
P & ¬P \\
|
||||
\hline
|
||||
T & F \\
|
||||
F & T \\
|
||||
\hline
|
||||
\end{array}
|
||||
$$
|
||||
|
||||
```
|
||||
$$
|
||||
\begin{array}{|c|c|}
|
||||
\hline
|
||||
P & ¬P \\
|
||||
\hline
|
||||
T & F \\
|
||||
F & T \\
|
||||
\hline
|
||||
\end{array}
|
||||
$$
|
||||
```
|
||||
@@ -7,13 +7,3 @@ Internally, websocket requests to `ws://localhost:3000/websockets` will be forwa
|
||||
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 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.
|
||||
|
||||
### Environment Variables
|
||||
|
||||
The client and server ports, as well as the default language, can be configured using environment variables:
|
||||
|
||||
* `PORT`: Sets the port for the backend server (default: `8080`).
|
||||
* `CLIENT_PORT`: Sets the port for the client server (default: `3000`).
|
||||
* `VITE_CLIENT_DEFAULT_LANGUAGE`: Sets the default language for the application (default: `en`).
|
||||
|
||||
Ensure these environment variables are set appropriately in your environment to configure the project as needed.
|
||||
|
||||
@@ -26,22 +26,3 @@ where you replace:
|
||||
Everything downloaded remains in the folder `lean4game/games`.
|
||||
The subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
|
||||
The other folders should only contain the built lean-games, sorted by owner and repo.
|
||||
|
||||
## Server capacity
|
||||
|
||||
If you would like to display the server capacity on the landing page,
|
||||
you can create a file `lean4game/games/stats.csv` of the following form:
|
||||
|
||||
```
|
||||
CPU,MEM
|
||||
0.1,0.8
|
||||
```
|
||||
|
||||
These numbers will be displayed on the landing page ("CPU: 10 % used" and "RAM: 80 % used").
|
||||
|
||||
If you only want one of the numbers, replace the number you don't want with `nan` (or anything
|
||||
else which does not parse as number).
|
||||
|
||||
If you don't want to show either, simply do not create `stats.csv`
|
||||
|
||||
Use your own script or cronjob to update the CSV file as desired.
|
||||
|
||||
+1
-1
@@ -33,7 +33,7 @@
|
||||
</p>
|
||||
</div>
|
||||
</noscript>
|
||||
<script type="module" src="client/src/index.tsx"></script>
|
||||
<script type="module" src="/client/src/index.tsx"></script>
|
||||
</body>
|
||||
|
||||
</html>
|
||||
|
||||
+1
-48
@@ -9,8 +9,6 @@ import os from 'os';
|
||||
import fs from 'fs';
|
||||
import anonymize from 'ip-anonymize';
|
||||
import { importTrigger, importStatus } from './import.mjs'
|
||||
import process from 'process';
|
||||
import { spawn } from 'child_process'
|
||||
// import fs from 'fs'
|
||||
|
||||
/**
|
||||
@@ -43,22 +41,6 @@ const server = app
|
||||
const owner = req.params.owner;
|
||||
const repo = req.params.repo
|
||||
const lang = req.params.lang
|
||||
|
||||
const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
|
||||
const log = `${process.cwd()}/logs/game-access.log`
|
||||
const header = "date;anon-ip;game;lang\n"
|
||||
const data = `${new Date()};${ip};${owner}/${repo};${lang}\n`
|
||||
|
||||
fs.writeFile(log, header.concat(data), { flag: 'ax' }, (file_exists) => {
|
||||
if (file_exists) {
|
||||
fs.appendFile(log, data, (err) => {
|
||||
if (err) console.log("Failed to append to log!")
|
||||
});
|
||||
}
|
||||
});
|
||||
|
||||
console.log(`[${new Date()}] ${ip} requested translation for ${owner}/${repo} in ${lang}`)
|
||||
|
||||
const filename = req.params[0];
|
||||
req.url = filename;
|
||||
express.static(path.join(getGameDir(owner,repo),".i18n",lang))(req, res, next);
|
||||
@@ -70,33 +52,6 @@ const server = app
|
||||
req.url = filename;
|
||||
express.static(path.join(getGameDir(owner,repo),".lake","gamedata"))(req, res, next);
|
||||
})
|
||||
.use('/data/stats', (req, res, next) => {
|
||||
// Returns a CSV of the form
|
||||
//
|
||||
// CPU,Mem
|
||||
// 0.21,0.65
|
||||
//
|
||||
// which contains the current server usage.
|
||||
|
||||
const statsProcess = spawn('/bin/bash', [path.join(__dirname, "stats.sh"), process.pid])
|
||||
|
||||
let outputData = ''
|
||||
let errorData = ''
|
||||
statsProcess.stdout.on('data', (data) => {
|
||||
outputData += data.toString();
|
||||
})
|
||||
statsProcess.stderr.on('data', (data) => {
|
||||
errorData += data.toString();
|
||||
})
|
||||
statsProcess.on('close', (code) => {
|
||||
if (code === 0) {
|
||||
res.send(outputData);
|
||||
} else {
|
||||
res.status(500).send(`Error executing script: ${errorData}`)
|
||||
console.error(`stats.sh exited with code ${code}. Error: ${errorData}`)
|
||||
}
|
||||
})
|
||||
})
|
||||
.use('/', router)
|
||||
.listen(PORT, () => console.log(`Listening on ${PORT}`));
|
||||
|
||||
@@ -223,9 +178,7 @@ wss.addListener("connection", function(ws, req) {
|
||||
|
||||
socketCounter += 1;
|
||||
const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
|
||||
|
||||
// TODO (Matvey): extract further information from `req`, for example browser language.
|
||||
console.log(`[${new Date()}] Socket opened - ${ip} - ${owner}/${repo}`)
|
||||
console.log(`[${new Date()}] Socket opened - ${ip}`)
|
||||
|
||||
const socket = {
|
||||
onMessage: (cb) => { ws.on("message", cb) },
|
||||
|
||||
@@ -1,10 +0,0 @@
|
||||
#!/bin/bash
|
||||
|
||||
# first argument is the process ID
|
||||
pid="$1"
|
||||
|
||||
# number of CPUs available
|
||||
nproc=$(nproc --all)
|
||||
|
||||
# hacky way to print the content of a CSV file containing CPU/Mem usage of the process
|
||||
top -bn2 -p $pid | awk -v nproc=$nproc 'NR > 16 {$12=substr($0,72); printf "CPU, MEM\n%.2f, %.2f\n", $9/nproc, $10}'
|
||||
@@ -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: Unfortunately, lambdaLetTelescope does not allow us to provide the number of arguments.
|
||||
-- TODO: Unfornately, lambdaLetTelescope does not allow us to provide the number of arguments.
|
||||
-- If the goal is a function, this will not work.
|
||||
|
||||
end AbstractCtx
|
||||
|
||||
@@ -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 implemented -/
|
||||
/-- The Image of the game (optional). TODO: Not impementeds -/
|
||||
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` occurrence at the end of the tactic sequence.
|
||||
-- delete `Hint` and `Branch` occurence at the end of the tactic sequence.
|
||||
| Syntax.node _ `GameServer.Tactic.Hint _ :: []
|
||||
| Syntax.node _ `GameServer.Tactic.Branch _ :: [] =>
|
||||
[]
|
||||
|
||||
@@ -190,7 +190,7 @@ def getCurLayer [MonadError m] : m Layer := do
|
||||
def getCurGameId [Monad m] : m Name := do
|
||||
match curGameExt.getState (← getEnv) with
|
||||
| some game => return game
|
||||
| none => return defaultGameName
|
||||
| none => return (.mkSimple defaultGameName)
|
||||
|
||||
/-- Get the current world -/
|
||||
def getCurWorldId [MonadError m] : m Name := do
|
||||
@@ -468,8 +468,8 @@ def getLevel? (levelId : LevelId) : m (Option GameLevel) := do
|
||||
|
||||
def getCurGame [Monad m] : m Game := do
|
||||
let some game ← getGame? (← getCurGameId)
|
||||
| let game := {name := defaultGameName}
|
||||
insertGame defaultGameName game
|
||||
| let game := {name := (.mkSimple defaultGameName)}
|
||||
insertGame (.mkSimple defaultGameName) game
|
||||
return game
|
||||
return game
|
||||
|
||||
|
||||
@@ -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
|
||||
-- depending on difficulty.
|
||||
-- deppending 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 errors or warnings
|
||||
-- -- Level is completed if there are no errrors or warnings
|
||||
-- let completed : Bool := ¬ diag.any (fun d =>
|
||||
-- d.severity? == some .error ∨ d.severity? == some .warning)
|
||||
|
||||
|
||||
@@ -3,7 +3,7 @@ import Lean.PrettyPrinter.Delaborator.Builtins
|
||||
import Lean.PrettyPrinter
|
||||
import Lean
|
||||
|
||||
import Std.Tactic.OpenPrivate
|
||||
import Batteries.Tactic.OpenPrivate
|
||||
|
||||
namespace GameServer
|
||||
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
import Lean.Environment
|
||||
import Std.Tactic.OpenPrivate
|
||||
import Batteries.Tactic.OpenPrivate
|
||||
import Lean.Data.Lsp.Communication
|
||||
|
||||
open Lean
|
||||
|
||||
@@ -124,7 +124,7 @@ partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : Co
|
||||
let allowed := GameServer.ALLOWED_KEYWORDS
|
||||
if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
|
||||
let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
|
||||
return {acc with tactics := acc.tactics.insert val}
|
||||
return {acc with tactics := acc.tactics.insert (.mkSimple val)}
|
||||
else
|
||||
return acc
|
||||
| .ident _info _rawVal val _preresolved =>
|
||||
|
||||
@@ -17,7 +17,7 @@ def levelIdFromFileName? (initParams : Lsp.InitializeParams) (fileName : String)
|
||||
let fileParts := fileName.splitOn "/"
|
||||
if fileParts.length == 3 then
|
||||
if let (some level, some game) := (fileParts[2]!.toNat?, initParams.rootUri?) then
|
||||
return some {game, world := fileParts[1]!, level := level}
|
||||
return some {game := .mkSimple game, world := .mkSimple fileParts[1]!, level := level}
|
||||
return none
|
||||
|
||||
def getLevelByFileName? [Monad m] [MonadEnv m] (initParams : Lsp.InitializeParams) (fileName : String) : m (Option GameLevel) := do
|
||||
@@ -123,7 +123,7 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
|
||||
let mut hintFVarsNames : Array Expr := #[]
|
||||
for fvar in hintFVars do
|
||||
let name₁ ← fvar.fvarId!.getUserName
|
||||
hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨s!"«\{{name₁}}»"⟩
|
||||
hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨.mkSimple s!"«\{{name₁}}»"⟩
|
||||
|
||||
let lctx := (← goal.getDecl).lctx -- the player's local context
|
||||
if let some bij ← matchDecls hintFVars lctx.getFVars
|
||||
@@ -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 errors or warnings
|
||||
-- Level is completed if there are no errrors or warnings
|
||||
let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error)
|
||||
let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning)
|
||||
|
||||
|
||||
@@ -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 preceding the proof. Concretely
|
||||
`let_intros` introduces all `let` statements that are preceeding 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.
|
||||
|
||||
@@ -35,7 +35,7 @@ elab "#show_option" verbose:(ppSpace showOptArg)? id:(ppSpace Parser.rawIdent)?
|
||||
| .ofNat val => s!"Nat := {repr val}"
|
||||
| .ofInt val => s!"Int := {repr val}"
|
||||
| .ofSyntax val => s!"Syntax := {repr val}"
|
||||
if let some val := opts.find name then
|
||||
if let some val := opts.find (.mkSimple name) then
|
||||
msg1 := s!"{msg1} (currently: {val})"
|
||||
msg := match verbose with
|
||||
| some opt =>
|
||||
|
||||
@@ -1,13 +1,13 @@
|
||||
{"version": 7,
|
||||
"packagesDir": ".lake/packages",
|
||||
"packages":
|
||||
[{"url": "https://github.com/leanprover/std4.git",
|
||||
[{"url": "https://github.com/leanprover-community/batteries.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
|
||||
"name": "std",
|
||||
"rev": "51e6e0d24db9341fb031288c298b7e6b56102253",
|
||||
"name": "batteries",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v4.7.0",
|
||||
"inputRev": "v4.8.0",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/mhuisi/lean4-cli",
|
||||
@@ -22,20 +22,20 @@
|
||||
{"url": "https://github.com/hhu-adam/lean-i18n.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"rev": "7550f08140c59c9a604bbcc23ab7830c103a3e39",
|
||||
"rev": "5158ce6720d88fa1f53fdb86aea8d515af69571c",
|
||||
"name": "i18n",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v4.7.0",
|
||||
"inputRev": "v4.8.0",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover-community/import-graph",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"rev": "ac07367cbdd57440e6fe78e5be13b41f9cb0f896",
|
||||
"rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404",
|
||||
"name": "importGraph",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v4.7.0",
|
||||
"inputRev": "v4.8.0",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"}],
|
||||
"configFile": "lakefile.toml"}],
|
||||
"name": "GameServer",
|
||||
"lakeDir": ".lake"}
|
||||
|
||||
@@ -6,7 +6,7 @@ package GameServer
|
||||
-- Using this assumes that each dependency has a tag of the form `v4.X.0`.
|
||||
def leanVersion : String := s!"v{Lean.versionString}"
|
||||
|
||||
require std from git "https://github.com/leanprover/std4.git" @ leanVersion
|
||||
require batteries from git "https://github.com/leanprover-community/batteries.git" @ leanVersion
|
||||
require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ leanVersion
|
||||
|
||||
require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion
|
||||
@@ -28,4 +28,4 @@ post_update pkg do
|
||||
let rootPkg ← getRootPackage
|
||||
if rootPkg.name = pkg.name then
|
||||
return -- do not run in GameServer itself
|
||||
discard <| runBuild gameserver.build >>= (·.await)
|
||||
discard <| runBuild gameserver.fetch
|
||||
|
||||
@@ -1 +1 @@
|
||||
leanprover/lean4:v4.7.0
|
||||
leanprover/lean4:v4.8.0
|
||||
|
||||
@@ -31,7 +31,6 @@ export default defineConfig({
|
||||
})
|
||||
],
|
||||
publicDir: "client/public",
|
||||
base: "/", // setting this to `/leangame/` means the server is now accessible at `localhost:3000/leangame`
|
||||
optimizeDeps: {
|
||||
exclude: ['games']
|
||||
},
|
||||
|
||||
Reference in New Issue
Block a user