From 451dc262b201089dd7016094cf1911b30fea9525 Mon Sep 17 00:00:00 2001 From: matlorr Date: Fri, 10 Jan 2025 10:13:36 +0100 Subject: [PATCH 1/5] Fixed display error of server capacity by performing rounding as last step. --- .gitignore | 1 + client/src/components/landing_page.tsx | 4 ++-- relay/stats.sh | 4 ++-- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/.gitignore b/.gitignore index 72e3323..c0120b2 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,4 @@ server/.lake **/.DS_Store logs/ relay/prev_cpu_metric +test.ecosystem.config.cjs diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index b69f50c..6080eeb 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -193,8 +193,8 @@ function LandingPage() {

- { usageMem >= 0 && <> {t("RAM")}: {usageMem} %{t(" used")}.
} - { usageCPU >= 0 && <> {t("CPU")}: {usageCPU} %{t(" used")}. } + { usageMem >= 0 && <> {t("RAM")}: {usageMem.toFixed(2)} %{t(" used")}.
} + { usageCPU >= 0 && <> {t("CPU")}: {usageCPU.toFixed(2)} %{t(" used")}. }

diff --git a/relay/stats.sh b/relay/stats.sh index 8996046..07e6972 100755 --- a/relay/stats.sh +++ b/relay/stats.sh @@ -3,10 +3,10 @@ # Load python interpreter python=/usr/bin/python3 # Load python script -cpu_usage=$L4G_DIR/lean4game/relay/cpu_usage.py +cpu_usage=relay/cpu_usage.py # Execute python script cpu=$($python $cpu_usage) # Calculate memory usage by computing used_memory/total_memory mem=$(free | sed '2q;d' | awk '{print $3/$2}') -printf "CPU, MEM\n%.2f, %.2f\n" $cpu $mem +printf "CPU, MEM\n%f, %f\n" $cpu $mem From 5b0715629a8f4d610e59f4fd05b6c0331a36739c Mon Sep 17 00:00:00 2001 From: matlorr Date: Fri, 10 Jan 2025 12:11:06 +0100 Subject: [PATCH 2/5] Adjust memory to be approx. the same as by htop --- relay/stats.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/relay/stats.sh b/relay/stats.sh index 07e6972..f51d270 100755 --- a/relay/stats.sh +++ b/relay/stats.sh @@ -6,7 +6,7 @@ python=/usr/bin/python3 cpu_usage=relay/cpu_usage.py # Execute python script cpu=$($python $cpu_usage) -# Calculate memory usage by computing used_memory/total_memory -mem=$(free | sed '2q;d' | awk '{print $3/$2}') +# Calculate memory usage by computing 1 - %free_memory +mem=$(free | sed '2q;d' | awk '{print 1 - ($4/$2)}') printf "CPU, MEM\n%f, %f\n" $cpu $mem From 1845644e86d17c4f73139bef61f2d0d39b530870 Mon Sep 17 00:00:00 2001 From: matlorr Date: Fri, 24 Jan 2025 13:51:28 +0100 Subject: [PATCH 3/5] Extract fetching of stats and perform it every 2 seconds --- client/src/components/landing_page.tsx | 48 ++++++++++++++++---------- 1 file changed, 29 insertions(+), 19 deletions(-) diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index 6080eeb..3d4a0c9 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -122,25 +122,10 @@ function LandingPage() { /** 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 * parseFloat(values[0])); - setUsageMem(100 * parseFloat(values[1])); - } - }).catch(err => { - console.info('server stats unavailable') - console.debug(err) - }) + const interval = setInterval(() => { + fetch_stats(); + }, 2000) + return () => clearInterval(interval) }, []) return
@@ -254,6 +239,31 @@ function LandingPage() {
+ + function fetch_stats() { + 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 * parseFloat(values[0])); + setUsageMem(100 * parseFloat(values[1])); + } + }).catch(err => { + console.info('server stats unavailable'); + console.debug(err); + }); + } } export default LandingPage From 49062cc3d5c558b49ef1aae4d3132d011874b2bf Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 26 Jan 2025 14:29:54 +0100 Subject: [PATCH 4/5] add new game --- client/src/config.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/client/src/config.json b/client/src/config.json index cc4261d..8ae10b0 100644 --- a/client/src/config.json +++ b/client/src/config.json @@ -3,7 +3,8 @@ "leanprover-community/nng4", "hhu-adam/robo", "djvelleman/stg4", - "trequetrum/lean4game-logic" + "trequetrum/lean4game-logic", + "jadabouhawili/knightsandknaves-lean4game" ], "languages": [ From 50bf73a0c505a1d070b28a827beb212544afaae4 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 30 Jan 2025 11:02:20 +0100 Subject: [PATCH 5/5] Update publish_game.md --- doc/publish_game.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/doc/publish_game.md b/doc/publish_game.md index bd017fe..e720bf4 100644 --- a/doc/publish_game.md +++ b/doc/publish_game.md @@ -24,7 +24,11 @@ You should see a white screen which shows import updates and eventually reports Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITORY}`! -## 4. Main page +## 4. Update + +To upload a new version of the game you will have to repeat 1. and 2. whenever you want to publish the updated version. + +## 5. Main page Adding games to the main page happens manually by the server maintainers. Tell us if you want us to add a tile for your game!