add outcomes png to dashboard (#327)

Adds the output of `outcomes_to_images.py` to the dashboard page.

Makes `generate_dashboard.py` responsible for launching subprocesses for
whatever intermediate artifacts it needs. This way, the dashboard
generating in `blueprint.yml` is reduced to a single line that calls
`generate_dashboard.py`.

![Screenshot from 2024-10-05
14-15-24](https://github.com/user-attachments/assets/95ef2da4-a60a-4944-a1ee-c58fc7a3c523)

.github/workflows/blueprint.yml

@@ -133,8 +133,8 @@ jobs:
 
       - name: Generate home_page/dashboard.md
         run: |
-          ~/.elan/bin/lake exe extract_implications outcomes equational_theories --hist > /tmp/hist.json
-          python scripts/generate_dashboard.py /tmp/hist.json
+          pip install pillow
+          python scripts/generate_dashboard.py
 
       - name: Generate home_page/implications/implications.js
         run: |

scripts/generate_dashboard.py

@@ -3,15 +3,14 @@
 import argparse
 import json
 import os
+import subprocess
 
 def make_progress_badge(ratio):
     percent = f"{ratio:.1%}"
     return f'<svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" width="100" height="20" role="img" aria-label="Progress: {percent}"><title>Progress: {percent}</title><linearGradient id="s" x2="0" y2="100%"><stop offset="0" stop-color="#bbb" stop-opacity=".1"/><stop offset="1" stop-opacity=".1"/></linearGradient><clipPath id="r"><rect width="100" height="20" rx="3" fill="#fff"/></clipPath><g clip-path="url(#r)"><rect width="59" height="20" fill="#555"/><rect x="59" width="41" height="20" fill="#007ec6"/><rect width="100" height="20" fill="url(#s)"/></g><g fill="#fff" text-anchor="middle" font-family="Verdana,Geneva,DejaVu Sans,sans-serif" text-rendering="geometricPrecision" font-size="110"><text aria-hidden="true" x="305" y="150" fill="#010101" fill-opacity=".3" transform="scale(.1)" textLength="490">Progress</text><text x="305" y="140" transform="scale(.1)" fill="#fff" textLength="490">Progress</text><text aria-hidden="true" x="790" y="150" fill="#010101" fill-opacity=".3" transform="scale(.1)" textLength="330">{percent}</text><text x="790" y="140" transform="scale(.1)" fill="#fff" textLength="330">{percent}</text></g></svg>'
 
 if __name__ == '__main__':
     parser = argparse.ArgumentParser(description="generate the dashboard markdown")
-    parser.add_argument("hist_file",
-                        help="json file containing output of `lake exe extract_implications outcomes --hist")
     parser.add_argument("--out_file",
                         default="home_page/dashboard/index.md",
                         help="markdown file to pass to jekyll")
@@ -20,8 +19,36 @@ def make_progress_badge(ratio):
                         help="path to create the progress badge for the Github repo")
 
     args = parser.parse_args()
-    with open(args.hist_file, 'r') as f:
-        data = json.load(f)
+
+    directory = os.path.dirname(args.out_file)
+    if not os.path.exists(directory):
+        os.makedirs(directory)
+    outcomes_image_path = os.path.join(directory, "outcomes.png")
+
+    print("extracting histogram...")
+    hist_command = [os.path.expanduser("~/.elan/bin/lake"),
+                    "exe", "extract_implications",
+                    "outcomes", "equational_theories", "--hist"]
+    hist_result = subprocess.run(hist_command, capture_output=True, text=True, check=True)
+
+    print("extracting outcomes json...")
+    outcomes_json_path = "/tmp/outcomes.json"
+    with open(outcomes_json_path, "w") as outcomes_file:
+        outcomes_command = [os.path.expanduser("~/.elan/bin/lake"),
+                            "exe", "extract_implications",
+                            "outcomes", "equational_theories"]
+        outcomes_result = subprocess.run(outcomes_command, text=True, check=True,
+                                         stdout = outcomes_file)
+
+    print("generating image...")
+    generate_image_command = ["./scripts/outcomes_to_image.py",
+                              outcomes_json_path,
+                              "--out",
+                              outcomes_image_path]
+    subprocess.run(generate_image_command, check=True)
+
+    print("generating markdown...")
+    data = json.loads(hist_result.stdout)
 
     explicit_proof_true = data.get('explicit_proof_true', 0)
     implicit_proof_true = data.get('implicit_proof_true', 0)
@@ -37,10 +64,6 @@ def make_progress_badge(ratio):
 
     total = proved_total + conjectured_total + unknown
 
-    directory = os.path.dirname(args.out_file)
-    if not os.path.exists(directory):
-        os.makedirs(directory)
-
     outfile = open(args.out_file, 'w')
 
     outfile.write("\n")
@@ -60,7 +83,6 @@ def make_progress_badge(ratio):
         implicit_proof_false, conjectured_total + unknown))
     outfile.write("\n")
 
-
     outfile.write("\nThe _no proof_ column above represents work that we still need to do.\n")
     outfile.write("Among the _no proof_ implications, we have the following conjecture counts:\n\n")
     outfile.write("| explicitly true | implicitly true | explicitly false | implicitly false | no conjecture |\n")
@@ -72,4 +94,7 @@ def make_progress_badge(ratio):
     ratio = (proved_total + conjectured_total) / total
     outfile.write(f"The implication graph is **{ratio:.3%}** complete if we include conjectures.\n\n")
 
+    outfile.write('## progress visualization\n\n')
+    outfile.write('<img src="{{site.url}}/dashboard/outcomes.png" width="700"/>')
+
     open(args.badge_file, 'w').write(make_progress_badge(ratio))