feat: snakemakeify hacker's delight

.gitignore

@@ -38,5 +38,5 @@ test-semantics/*.llvm
 lakefile.olean
 .lake/
 SSA/Projects/InstCombine/tests/logs/generalizer
-
+.snakemake
 **/.ruff_cache

.python-version

@@ -0,0 +1 @@
+3.12

bv-evaluation/.gitignore

@@ -1,3 +1,5 @@
+logs/
+__pycache__
 *.xz
 *.jpeg
 *.pdf

bv-evaluation/Snakefile

@@ -0,0 +1,98 @@
+#!/usr/bin/env python3
+import argparse
+import os
+import random
+import subprocess
+import concurrent.futures
+import shutil
+import multiprocessing
+import psutil
+import time
+import threading
+import platform
+from functools import partial
+from pathlib import Path
+import sys
+from runwithlimits import *
+from snakelib import *
+
+configfile: "config.yaml"
+workdir: "../"
+
+gitroot=get_git_root()
+sed=get_sed()
+HACKERSDELIGHT_FILE_NAMES, = glob_wildcards(gitroot / "SSA/Projects/InstCombine/HackersDelight/{file}.lean")
+hdel_nreps = config["hdel_nreps"]
+
+onstart:
+    shell("elan --version")
+    shell("cd {gitroot} && lake exe cache get && lake build")
+    shell("uv --version")
+    shell("bitwuzla --version")
+
+rule hdel_compare_make_lean:
+  input:
+    gitroot / "SSA/Projects/InstCombine/HackersDelight/{file}.lean"
+  output:
+     gitroot / "bv-evaluation/results/HackersDelight/{file}_{width}_{hdel_nreps}.lean"
+  log:
+      "logs/compare_make_lean_{file}_{width}_{hdel_nreps}.log"
+  params:
+      sed=sed,
+  shell:
+    "cp {input} {output} && "
+    "{params.sed} -i  -e \"s/all_goals sorry/all_goals bv_compare'/g\" -e \"s/WIDTH/{wildcards.width}/g\" {output} "
+
+
+rule hdel_compare_make_output:
+  params:
+      gitroot=gitroot,
+      timeout=config["hdel_timeout_sec"],
+      memout=config["hdel_memout_mb"],
+  input:
+    lambda wc: gitroot / f"bv-evaluation/results/HackersDelight/{wc.file}_{wc.width}_{hdel_nreps}.lean",
+  output:
+    gitroot / "bv-evaluation/results/HackersDelight/{file}_{width}_r{r}.txt"
+  log:
+      "logs/hdel_compare_make_output_{file}_{width}_{r}.log"
+  resources:
+  # TODO: actually impose memory and time limit, using a python script.
+  shell:
+    "{params.gitroot}/bv-evaluation/runwithlimits.py "
+    " --timeout-sec={params.timeout} "
+    " --memout-mb={params.memout} "
+    " -- lake 2>&1 lean {input}  | tee {log} > {output}"
+
+
+# We can eventually split these, if we carefully understand the naming convention
+# of 'collect' for hacker's delight.
+# We currently make a monolithic job that runs both collect and plot,
+# Since the naming convention is a little opaque to @bollu.
+rule hdel_collect_and_plot:
+  input:
+    expand(gitroot / "bv-evaluation/results/HackersDelight/{file}_{width}_r{r}.txt",
+      file=HACKERSDELIGHT_FILE_NAMES,
+      width=config["hdel_bv_widths"],
+      r=range(hdel_nreps))
+  params:
+    gitroot=gitroot,
+    nreps = lambda wc: hdel_nreps,
+    nthreads = lambda wc: config["hdel_nthreads"]
+  output:
+    tex=gitroot / "bv-evaluation/performance-hackersdelight.tex",
+    pdf_stacked=gitroot / "bv-evaluation/plots/bv_decide_stacked_perc_HackersDelight_bvw64.pdf"
+    # TODO: track the exact files generated by 'collect.py'.
+    # We currently just bother asking for the two outputs we care for.
+  log:
+    log_collect="logs/collect.log",
+    log_plot="logs/plot.log"
+  threads: 1
+  shell:
+    "pushd {params.gitroot}/bv-evaluation && ./collect.py hackersdelight 2>&1 > {log.log_collect} && "
+    "./plot.py hackersdelight 2>&1 > {log.log_plot}"
+
+rule all:
+  input:
+    rules.hdel_collect_and_plot.output
+  default_target: True
+

bv-evaluation/collect.py

@@ -1,3 +1,4 @@
+#!/usr/bin/env -S uv run
 import argparse
 import os
 import csv

bv-evaluation/config.yaml

@@ -0,0 +1,8 @@
+hdel_bv_widths: [4, 8, 16, 32, 64] # number of hackers delight widths.
+hdel_nreps: 2 # number of repetitions to run hacker's delight tests.
+hdel_timeout_sec: 1800 # timeout for hacker's delight test cases.
+hdel_memout_mb: 8000 # memout for hacker's delight test cases.
+hdel_nthreads: 8 # number of threads to use for hacker's delight tests.
+seed: 42 # random number generator seed.
+
+

bv-evaluation/plot.py

@@ -1,5 +1,4 @@
-#!/usr/bin/env python3
-
+#!/usr/bin/env -S uv run
 import argparse
 import os
 import pandas as pd

bv-evaluation/runwithlimits.py

@@ -1,12 +1,12 @@
-#!/usr/bin/env python3
+#!/usr/bin/env -S uv run
 import os
 import subprocess
-import shutil
-import multiprocessing
 import psutil
 import time
 import threading
-from typing import List, Dict
+import argparse
+import sys
+from typing import List, Dict, Optional
 
 def kill_process_tree(pid: int):
     """
@@ -43,12 +43,12 @@ def monitor_memory(pid: int, memout_mb: int, flag: Dict[str, bool]):
                 flag["memout"] = True
                 kill_process_tree(pid)
                 return
-            time.sleep(5)
+            time.sleep(0.1)
     except psutil.NoSuchProcess:
         pass
 
 
-def run_with_limits(cmd: List[str], timeout: int, memout_mb: int) -> (str, str, str):
+def run_with_limits(cmd: List[str], timeout: int, memout_mb: int, cwd : Optional[str] = None) -> (str, str, str):
     """
     Run the process 'cmd' with timeout 'timeout' in seconds,
     and memout 'memout_mb' in megabyte.
@@ -69,6 +69,7 @@ def run_with_limits(cmd: List[str], timeout: int, memout_mb: int) -> (str, str,
             stderr=subprocess.PIPE,
             text=True,
             preexec_fn=os.setsid,
+            cwd=cwd
         )
         flag = {"done": False, "memout": False}
         monitor_thread = threading.Thread(
@@ -91,3 +92,48 @@ def run_with_limits(cmd: List[str], timeout: int, memout_mb: int) -> (str, str,
             return "TIMEOUT", stdout, stderr
     except Exception as e:
         return "ERROR", "", str(e)
+
+class Errcode:
+    TIMEOUT = 10
+    MEMOUT = 20
+    PYERROR = 30
+
+def parse_args():
+    parser = argparse.ArgumentParser(formatter_class=argparse.RawDescriptionHelpFormatter,
+        description=(
+        f"Run a command with timeout and memory limits.\n\n"
+        f"RETURN CODES:\n"
+        f"  success:      0\n"
+        f"  timeout:      {Errcode.TIMEOUT}\n"
+        f"  memout:       {Errcode.MEMOUT}\n"
+        f"  python error: {Errcode.PYERROR}\n"
+        ))
+    parser.add_argument("--timeout-sec", type=int, required=True, help="Timeout in seconds")
+    parser.add_argument("--memout-mb", type=int, required=True, help="Memory limit in MB")
+    parser.add_argument("cmd", nargs=argparse.REMAINDER, help="Command to run with arguments")
+    return parser.parse_args()
+
+def main():
+    args = parse_args()
+
+    if args.cmd and args.cmd[0] == "--":
+        cmd_args = args.cmd[1:]
+    else:
+        cmd_args = args.cmd
+
+    err, stdout, stderr = run_with_limits(cmd_args, args.timeout_sec, args.memout_mb)
+    print(stdout, file=sys.stdout, end="")
+    print(stderr, file=sys.stderr, end="")
+
+    if isinstance(err, int):
+        sys.exit(err)
+    elif err == "TIMEOUT":
+        sys.exit(Errcode.TIMEOUT)
+    elif err == "MEMOUT":
+        sys.exit(Errcode.MEMOUT)
+    else:
+        sys.exit(Errcode.PYERROR)
+
+if __name__ == "__main__":
+    main()
+

bv-evaluation/snakelib.py

@@ -0,0 +1,21 @@
+import argparse
+import os
+import random
+import subprocess
+import concurrent.futures
+import shutil
+import multiprocessing
+import psutil
+import time
+import threading
+import platform
+from functools import partial
+from pathlib import Path
+import sys
+
+def get_git_root() -> Path:
+  return Path(subprocess.check_output( ["git", "rev-parse", "--show-toplevel"]).decode().strip())
+
+
+def get_sed() -> str:
+  return "gsed" if platform.system() == "Darwin" else "sed"

bv-evaluation/toplevel-hackersdelight.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+uv run snakemake all --cores all --show-failed-logs
+

pyproject.toml

@@ -0,0 +1,73 @@
+[project]
+name = "lean-mlir"
+version = "0.1.0"
+description = "Add your description here"
+readme = "README.md"
+requires-python = ">=3.12"
+dependencies = [
+    "appdirs==1.4.4",
+    "argparse-dataclass==2.0.0",
+    "attrs==25.3.0",
+    "certifi==2025.8.3",
+    "charset-normalizer==3.4.3",
+    "conda-inject==1.3.2",
+    "configargparse==1.7.1",
+    "connection-pool==0.0.3",
+    "contourpy==1.3.1",
+    "cycler==0.12.1",
+    "docopt==0.6.2",
+    "docutils==0.22",
+    "dpath==2.2.0",
+    "fastjsonschema==2.21.2",
+    "fonttools==4.56.0",
+    "gitdb==4.0.12",
+    "gitpython==3.1.45",
+    "humanfriendly==10.0",
+    "idna==3.10",
+    "immutables==0.21",
+    "importlib-metadata==8.6.1",
+    "jinja2==3.1.6",
+    "jsonschema==4.25.1",
+    "jsonschema-specifications==2025.4.1",
+    "jupyter-core==5.8.1",
+    "kiwisolver==1.4.8",
+    "markupsafe==3.0.2",
+    "matplotlib==3.10.1",
+    "nbformat==5.10.4",
+    "num2words==0.5.14",
+    "numpy==2.2.2",
+    "packaging==24.2",
+    "pandas==2.2.3",
+    "pillow==11.1.0",
+    "platformdirs==4.3.8",
+    "polars==1.24.0",
+    "psutil==7.0.0",
+    "pulp==3.2.2",
+    "pyparsing==3.2.1",
+    "python-dateutil==2.9.0.post0",
+    "pytz==2025.1",
+    "pyyaml==6.0.2",
+    "referencing==0.36.2",
+    "requests==2.32.5",
+    "reretry==0.11.8",
+    "rpds-py==0.27.0",
+    "six==1.17.0",
+    "smart-open==7.3.0.post1",
+    "smmap==5.0.2",
+    "snakemake==9.9.0",
+    "snakemake-interface-common==1.21.0",
+    "snakemake-interface-executor-plugins==9.3.9",
+    "snakemake-interface-logger-plugins==1.2.4",
+    "snakemake-interface-report-plugins==1.2.0",
+    "snakemake-interface-storage-plugins==4.2.2",
+    "tabulate==0.9.0",
+    "throttler==1.2.2",
+    "traitlets==5.14.3",
+    "typing-extensions==4.15.0",
+    "tzdata==2025.1",
+    "urllib3==2.5.0",
+    "visidata==3.1.1",
+    "wrapt==1.17.3",
+    "yte==1.9.0",
+    "zipp==3.21.0",
+]

requirements.txt

@@ -1,21 +1,65 @@
+appdirs==1.4.4
+argparse-dataclass==2.0.0
+attrs==25.3.0
+certifi==2025.8.3
+charset-normalizer==3.4.3
+conda-inject==1.3.2
+ConfigArgParse==1.7.1
+connection_pool==0.0.3
 contourpy==1.3.1
 cycler==0.12.1
+docopt==0.6.2
+docutils==0.22
+dpath==2.2.0
+fastjsonschema==2.21.2
 fonttools==4.56.0
+gitdb==4.0.12
+GitPython==3.1.45
+humanfriendly==10.0
+idna==3.10
+immutables==0.21
 importlib_metadata==8.6.1
+Jinja2==3.1.6
+jsonschema==4.25.1
+jsonschema-specifications==2025.4.1
+jupyter_core==5.8.1
 kiwisolver==1.4.8
+MarkupSafe==3.0.2
 matplotlib==3.10.1
+nbformat==5.10.4
+num2words==0.5.14
 numpy==2.2.2
 packaging==24.2
 pandas==2.2.3
 pillow==11.1.0
+platformdirs==4.3.8
 polars==1.24.0
 psutil==7.0.0
+PuLP==3.2.2
 pyparsing==3.2.1
 python-dateutil==2.9.0.post0
 pytz==2025.1
+PyYAML==6.0.2
+referencing==0.36.2
+requests==2.32.5
+reretry==0.11.8
+rpds-py==0.27.0
 six==1.17.0
+smart_open==7.3.0.post1
+smmap==5.0.2
+snakemake==9.9.0
+snakemake-interface-common==1.21.0
+snakemake-interface-executor-plugins==9.3.9
+snakemake-interface-logger-plugins==1.2.4
+snakemake-interface-report-plugins==1.2.0
+snakemake-interface-storage-plugins==4.2.2
 tabulate==0.9.0
+throttler==1.2.2
+traitlets==5.14.3
+typing_extensions==4.15.0
 tzdata==2025.1
+urllib3==2.5.0
 visidata==3.1.1
+wrapt==1.17.3
+yte==1.9.0
 zipp==3.21.0
-num2words==0.5.14