update dataset with at leaset 10 min interval

app_leaderboard.py

@@ -3,12 +3,15 @@ import logging
 import datasets
 import gradio as gr
 import pandas as pd
+import datetime
 
 from fetch_utils import (check_dataset_and_get_config,
                          check_dataset_and_get_split)
 
 import leaderboard
 logger = logging.getLogger(__name__)
+global update_time 
+update_time = datetime.datetime.fromtimestamp(0)
 
 def get_records_from_dataset_repo(dataset_id):
     dataset_config = check_dataset_and_get_config(dataset_id)
@@ -75,6 +78,8 @@ def get_display_df(df):
     return display_df
 
 def get_demo(leaderboard_tab):
+    global update_time
+    update_time = datetime.datetime.now()
     logger.info("Loading leaderboard records")
     leaderboard.records = get_records_from_dataset_repo(leaderboard.LEADERBOARD)
     records = leaderboard.records
@@ -117,6 +122,10 @@ def get_demo(leaderboard_tab):
         leaderboard_df = gr.DataFrame(display_df, datatype=types, interactive=False)
 
     def update_leaderboard_records(model_id, dataset_id, columns, task):
+        global update_time
+        if datetime.datetime.now() - update_time < datetime.timedelta(minutes=10):
+            return gr.update()
+        update_time = datetime.datetime.now()
         logger.info("Updating leaderboard records")
         leaderboard.records = get_records_from_dataset_repo(leaderboard.LEADERBOARD)
         return filter_table(model_id, dataset_id, columns, task)