Merge pull request #283 from leanprover-community/server_capacity

Server capacity

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`)
+    const interval = setInterval(() => {
-    .then(response => {if (response.ok) {
+      fetch_stats();
-      return response.text() } else {throw ""}})
+    }, 2000)
-    .then(data => {
+    return () => clearInterval(interval)
-      // 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)
-    })
   }, [])
 
   return <div className="landing-page">
@@ -254,6 +239,31 @@ function LandingPage() {
     </footer>
   </div>
 
+
+  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