doc: dark theme plots and improved styling (#2387)

- Toggles graph to light/dark theme based on user browser preference
- Improved styling for graph incl: fix aspect ratio to 16:9; hover over
has vertical bar;

Author: smmercuri

.github/workflows/build-and-docs.yml

@@ -130,7 +130,7 @@ jobs:
         shell: bash
         run: |
           cd docbuild
-          lake exe overwrite_index ./out/index.html ./out/file_counts.html | tee -a "$GITHUB_STEP_SUMMARY"
+          lake exe overwrite_index ./out/index.html ./out/file_counts_dark.html ./out/file_counts_white.html | tee -a "$GITHUB_STEP_SUMMARY"
 
       - name: Upload docs
         id: deployment

docbuild/scripts/overwrite_index.lean

@@ -113,9 +113,22 @@ unsafe def main (args : List String) : IO Unit := do
     | IO.println "Usage: stats <file>
 overwrites the contents of the `main` tag of a html `file` with a welcome page including stats."
   let inputHtmlContent ← IO.FS.readFile file
-  let .some (graphFile : String) := args[1]?
+  let .some (graphFileDark : String) := args[1]?
     | IO.println "Repository growth graph not supplied, generating docs without graph."
-  let graphHtml ← IO.FS.readFile graphFile
+  let .some (graphFileLight : String) := args[2]?
+    | IO.println "Repository growth graph not supplied, generating docs without graph."
+  let graphHtmlDark ← IO.FS.readFile graphFileDark
+  let graphHtmlLight ← IO.FS.readFile graphFileLight
+  let graphHtml :=
+    s!"<style>
+        .theme-dark \{ display: none; }
+        @media (prefers-color-scheme: dark) \{
+          .theme-light \{ display: none; }
+          .theme-dark \{ display: block; }
+        }
+      </style>
+      <div class=\"theme-light\">{graphHtmlLight}</div>
+      <div class=\"theme-dark\">{graphHtmlDark}</div>"
 
   runWithImports do
     let categoryStats ← getCategoryStatsMarkdown

docbuild/scripts/plot_growth.py

@@ -4,23 +4,24 @@
 import plotly.express as px
 import re
 import subprocess
-from datetime import datetime, timedelta
+from datetime import datetime
 
 conf = {
-  'line_color': '#4285F4', # Color used in plotting
-  'line_width': 3, # Width of line used in the plot
-  'title': dict(
-    text='Number of Lean files in Formal Conjectures', # Title text
-    font=dict(size=15), # Title font
-    x=0.5, # Center title
-    xanchor='center' # Center title
-  ),
-  'max-width': '1000px', # Width of plot in px
-  'aspect-ratio': 2, # aspect ratio of plot
-  'start_date': '2025-05-28', # Announcement date is '2025-05-28'
-  'xlabel': 'Date', # x-axis label on plot
-  'ylabel': 'Number of Lean files', # y-axis label on plot
-  'out_path': 'docbuild/out/file_counts.html' # This is used as an arg to overwrite_index.lean in .github/workflows/build-and-docs.yml
+    'line_color': '#4285F4',
+    'line_width': 2,
+    'title': dict(
+        text='Number of Lean files in Formal Conjectures',
+        font=dict(size=18),
+        x=0.5,
+        xanchor='center'
+    ),
+    'width_pct': '90%',
+    'height_px': 675,
+    'max_width' : 1200, # 16:9 aspect ratio at max
+    'start_date': '2025-05-28',
+    'xlabel': 'Date',
+    'ylabel': 'File Count',
+    'out_path_prefix': 'docbuild/out/file_counts'
 }
 
 def get_file_counts_over_time(start_date, columns):
@@ -66,44 +67,92 @@ def get_file_counts_over_time(start_date, columns):
 
     return pd.DataFrame(data, columns=columns)
 
-def plot_file_counts(df, xlabel, ylabel, max_width, aspect_ratio, line_color, line_width, title, out_path):
+def plot_file_counts(
+      df,
+      xlabel,
+      ylabel,
+      max_width,
+      width_pct,
+      height,
+      line_color,
+      line_width,
+      title,
+      out_path,
+      theme):
     """
     Plots the number of files over time.
 
     Args:
         df (pd.DataFrame): A pandas DataFrame which should contain `xlabel` and `ylabel` as columns
         xlabel (str): The column from `df` to use as the `x`-axis
         ylabel (str): The column from `df` to use as the `y`-axis
+        max_width (int): Maximum width of plot in `px`
+        width_pct (str): % width of plot inside parent div
+        height (int): Height of plot in `px`
         line_color (str): Colour of plotted graph
+        line_width (float): Width of plotted line in `px`
         title (dict): Dictionary specifying graph title and style
         out_path (str): Save location of html
+        theme (str): plotly template suffix to use as plot theme. E.g., use "dark" for "plotly_dark"
     """
+    out_path = f"{out_path}_{theme}.html"
     fig = px.line(df, xlabel, ylabel)
-    fig.update_layout(title=title)
-    fig.update_yaxes(
-       scaleanchor="x",
-       scaleratio=0.5
+
+    fig.update_layout(
+        title=title,
+        template=f"plotly_{theme}",
+        hovermode='x unified',
+        margin=dict(l=40, r=40, t=60, b=40),
+        autosize=True
+    )
+
+    fig.update_traces(
+        line=dict(color=line_color, width=line_width, shape='hv'),
+        marker=dict(size=6)
+    )
+
+    fig_html = fig.to_html(
+        full_html=False,
+        include_plotlyjs='cdn',
+        config={'responsive': True}
     )
-    fig.update_traces(line_color=line_color, line_width=line_width)
-    fig_html = f"<div style='max-width: {max_width}; aspect-ratio: {aspect_ratio};'> {
-       fig.to_html(full_html=False, include_plotlyjs='cdn')} </div>"
+
+    styled_html = f"""
+        <style>
+            .plot-container {{
+                width: {width_pct};
+                max-width: {max_width}px;
+                height: {height}px;
+                margin: 0 auto;
+                padding: 10px;
+            }}
+        </style>
+
+        <div class="plot-container">
+            {fig_html}
+        </div>
+    """
+
     with open(out_path, "w") as f:
-       f.write(fig_html)
+       f.write(styled_html)
 
 if __name__ == "__main__":
     github_url = "https://github.com/google-deepmind/formal-conjectures"
     print(f"Generating growth plots for: {github_url}")
 
     columns = [conf['xlabel'], conf['ylabel']]
     df = get_file_counts_over_time(conf['start_date'], columns)
-    plot_file_counts(
-      df=df,
-      xlabel=conf['xlabel'],
-      ylabel=conf['ylabel'],
-      max_width=conf['max-width'],
-      aspect_ratio=conf['aspect-ratio'],
-      line_color=conf['line_color'],
-      line_width=conf['line_width'],
-      title=conf['title'],
-      out_path=conf['out_path']
-    )
+    for theme in ["white", "dark"]:
+        plot_file_counts(
+          df=df,
+          xlabel=conf['xlabel'],
+          ylabel=conf['ylabel'],
+          max_width=conf['max_width'],
+          width_pct=conf['width_pct'],
+          height=conf['height_px'],
+          line_color=conf['line_color'],
+          line_width=conf['line_width'],
+          title=conf['title'],
+          out_path=conf['out_path_prefix'],
+          theme=theme
+        )