style changes

README.md

@@ -4,7 +4,7 @@ emoji: 🏆
 colorFrom: blue
 colorTo: purple
 sdk: gradio
-sdk_version: 4.44.1
+sdk_version: 4.15.0
 app_file: app.py
 pinned: false
 license: apache-2.0

app.py

@@ -27,6 +27,7 @@ with gr.Blocks(title=f'{benchname} Leaderboard', head=head_style) as demo:
             table, type_map = build_df()
             headers = [coln for coln in table.columns if not coln.startswith('_')]
             datatypes = [type_map[x] for x in headers]
+            colwidths = [50, 400, 120, 130] + [150 for _ in headers[4:]]
 
             with gr.Row():
                 model_name = gr.Textbox(
@@ -54,7 +55,7 @@ with gr.Blocks(title=f'{benchname} Leaderboard', head=head_style) as demo:
                 interactive=False,
                 wrap=True,
                 visible=True,
-                column_widths=[130 for _ in headers],
+                column_widths=colwidths,
             )
 
             def filter_df(model_name, model_size, model_type):
@@ -75,7 +76,7 @@ with gr.Blocks(title=f'{benchname} Leaderboard', head=head_style) as demo:
                     interactive=False,
                     wrap=True,
                     visible=True,
-                    column_widths=[130 for _ in headers],
+                    column_widths=colwidths,
                 )
                 return ret
 

utils.py

@@ -16,7 +16,7 @@ def build_df():
         name = row['name']
         if row['clickable']:
             hfp = row['hf_path']
-            names_html.append(f'<a href="https://huggingface.co/{hfp}">{name}</a>')
+            names_html.append(f'<a href="https://huggingface.co/{hfp}" target="_blank">{name}</a>')
         else:
             names_html.append(name)
     df['Name'] = names_html
@@ -34,10 +34,13 @@ def build_df():
 
     for coln in raw_df.columns:
         if coln.startswith('SCORE '):
-            df[coln[6:]] = raw_df[coln].round(2)
-            type_map[coln[6:]] = 'number'
+            newc = coln[6:]
+            if newc == 'overall':
+                newc = '⭐ Overall'
+            df[newc] = raw_df[coln].round(2)
+            type_map[newc] = 'number'
 
-    df.sort_values('overall', ascending=False, inplace=True)
+    df.sort_values('⭐ Overall', ascending=False, inplace=True)
     df.reset_index(drop=True, inplace=True)
     df.insert(0, 'Rank', list(range(1, len(df)+1)))