[Chart] Generate chart on website

Author: bobot

Makefile

@@ -19,7 +19,7 @@ test: generation ## Test the code with pytest
 	@echo "🚀 Testing code: Running pytest"
 	@poetry run pytest
 
-generation: submission-generation participant-data track-data division-track-data results-generation ## Files generation for the website
+generation: submission-generation participant-data track-data division-track-data results-generation charts-generation ## Files generation for the website
 
 .PHONY: build
 build: clean-build ## Build wheel file using poetry
@@ -84,6 +84,21 @@ results-generation:
 	@echo "🚀 Generating results to web/content/results for Parallel"
 	@poetry run smtcomp export-results-pages data Parallel
 
+charts-generation:
+	@echo "🚀 Generating results to web/content/results for SingleQuery"
+	@poetry run smtcomp generate-website-graphics data SingleQuery
+	@echo "🚀 Generating results to web/content/results for ModelValidation"
+	@poetry run smtcomp generate-website-graphics data ModelValidation
+	@echo "🚀 Generating results to web/content/results for UnsatCore"
+	@poetry run smtcomp generate-website-graphics data UnsatCore
+	@echo "🚀 Generating results to web/content/results for Incremental"
+	@poetry run smtcomp generate-website-graphics data Incremental
+	# @echo "🚀 Generating results to web/content/results for Cloud"
+	# @poetry run smtcomp generate-website-graphics data Cloud
+	@echo "🚀 Generating results to web/content/results for Parallel"
+	@poetry run smtcomp generate-website-graphics data Parallel
+
+
 cache:
 	@echo "🚀 Generating cache"
 	@poetry run smtcomp create-cache data

poetry.lock

@@ -21,6 +21,7 @@ dependencies = [
 "polars",
 "PyGithub",
 "altair",
+"python-frontmatter",
 ]
 #pystemd is not set as dependency because it is not in the CI
 
@@ -70,11 +71,10 @@ module = [
     "benchexec","benchexec.util",
     "benchexec.result","benchexec.tools.template",
     "benchexec.runexecutor",
-    "bs4","wget"
+    "bs4","wget","frontmatter"
 ]
 ignore_missing_imports = true
 
-
 [tool.ruff]
 target-version = "py37"
 line-length = 120

pyproject.toml

@@ -4,12 +4,15 @@
 from typing import Set, Dict, Optional, cast, List, DefaultDict, Tuple
 from pathlib import Path, PurePath
 from smtcomp import defs
+from rich.progress import track as rich_track
 
 import polars as pl
 import altair as alt
-import smtcomp.scoring
+import altair.utils.html
+import altair.vegalite.display
 from smtcomp.utils import *
-import smtcomp.results
+import smtcomp.generate_website_page
+import frontmatter
 
 c_file = pl.col("file")
 c_logic = pl.col("logic")
@@ -28,10 +31,9 @@
 def create_output(
     config: defs.Config,
     results: pl.LazyFrame,
-    output: Path,
     logics: list[defs.Logic] = [],
     divisions: list[defs.Division] = [],
-) -> None:
+) -> alt.api.ChartType:
 
     # We are computing the buckets offline because we have too much data
     results = results.filter(
@@ -82,7 +84,7 @@ def create_output(
 
     bucket_domain: list[float] = list(df_buckets["bucket"])
 
-    row1 = df_corr.row(1, named=True)
+    row1 = df_corr.row(min(1, len(df_corr) - 1), named=True)
 
     # Create heatmap with selection
     select_x = alt.selection_point(fields=["solver"], name="solver1", value=row1["solver"], toggle=False)
@@ -170,10 +172,58 @@ def create_output(
         .add_params(division)
     )
 
-    graph = (g_select_provers | g_results_rect + g_results_text).resolve_scale(color="independent")
+    graph: alt.api.ChartType = (g_select_provers | g_results_rect + g_results_text).resolve_scale(color="independent")
 
     graph = alt.vconcat(graph, legend_answer_x | legend_answer_y | legend_logic | legend_division)
 
     graph = graph.resolve_scale(color="independent")
 
-    graph.save(output)
+    return graph
+
+
+def save_output(
+    config: defs.Config,
+    results: pl.LazyFrame,
+    output: Path,
+    logics: list[defs.Logic] = [],
+    divisions: list[defs.Division] = [],
+) -> None:
+
+    create_output(config, results, logics, divisions).save(output)
+
+
+def save_hugo_output(chart: alt.api.ChartType, output: Path, title: str) -> None:
+
+    with alt.data_transformers.disable_max_rows():
+        content = chart.to_html(
+            fullhtml=False,
+        )
+    post = frontmatter.Post(content=content, title=title, layout="chart")
+    output.write_text(frontmatter.dumps(post))
+
+
+def generate_pages(config: defs.Config, results: pl.LazyFrame, track: defs.Track) -> None:
+    page_suffix = smtcomp.generate_website_page.page_track_suffix(track)
+    dst = config.web_results
+    dst.mkdir(parents=True, exist_ok=True)
+
+    df_results = results.filter(c_run == True).collect()
+    results = df_results.lazy()
+
+    divisions = list(df_results["division"].unique())
+    for div in rich_track(list(map(defs.Division.of_int, divisions)), description="Generating chart for divisions"):
+        chart = create_output(config, results, divisions=[div])
+        save_hugo_output(
+            chart,
+            output=dst / f"{div.name.lower()}-{page_suffix}-chart.html",
+            title=f"Chart for division {div.name}",
+        )
+
+    logics = list(df_results["logic"].unique())
+    for logic in rich_track(list(map(defs.Logic.of_int, logics)), description="Generating chart for logics"):
+        chart = create_output(config, results, logics=[logic])
+        save_hugo_output(
+            chart,
+            output=dst / f"{logic.name.lower()}-{page_suffix}-chart.html",
+            title=f"Chart for logic {logic.name}",
+        )

smtcomp/generate_graphics.py

@@ -1149,4 +1149,25 @@ def generate_graphics(
 
     results = smtcomp.scoring.add_disagreements_info(results, track).filter(disagreements=False).drop("disagreements")
 
-    smtcomp_generate_graphics.create_output(config, results, output, logic, division)
+    smtcomp_generate_graphics.save_output(config, results, output, logic, division)
+
+
+@app.command()
+def generate_website_graphics(
+    data: Path,
+    track: defs.Track,
+    src: List[Path] = typer.Argument(None),
+) -> None:
+    """
+    Generate graphics for hugo website
+
+    If src is empty use results in data
+    """
+    config = defs.Config(data)
+    results = smtcomp.results.helper_get_results(config, src, track)
+
+    smtcomp.scoring.sanity_check(config, results)
+
+    results = smtcomp.scoring.add_disagreements_info(results, track).filter(disagreements=False).drop("disagreements")
+
+    smtcomp_generate_graphics.generate_pages(config, results, track)

smtcomp/main.py

@@ -525,4 +525,7 @@ def helper_get_results(config: defs.Config, results: List[Path], track: defs.Tra
         defaults=defaults,
     )
 
+    if track == defs.Track.Parallel:
+        selected = selected.with_columns(run=True)
+
     return selected

smtcomp/results.py

@@ -15,9 +15,8 @@ <h1>{{ .Params.division }} ({{ $prettyTrack }})</h1>
   <p>
     Competition results for the {{ .Params.division }}
     {{ if $trueDivision }} division {{ else }} logic {{ end }}
-    in the {{ $prettyTrack }}.
+    in the {{ $prettyTrack }}. <a href="{{math.Add (path.Dir .RelPermalink) "-chart"}}"><b>Chart</b></a> </p>
   <p>Results were generated on {{ .Params.resultdate }}</p>
-  </p>
   <p>
     <b>Benchmarks</b>: {{ .Params.n_benchmarks }}<br/>
     <b>Time Limit:</b> {{ .Params.time_limit }} seconds<br/>