#!/usr/bin/env python3
"""Lean Build Server — listens on port 8765, runs `lake build <module>`.

Endpoints:
  GET /<module>   — build module, return JSON {passed, output}
  GET /health     — return {"status": "ok", "modules": [...]}
"""
import subprocess, json, sys, os
from http.server import HTTPServer, BaseHTTPRequestHandler

LAKE_WORKDIR = os.environ.get("LAKE_WORKDIR",
    "/home/allaun/Research Stack/0-Core-Formalism/lean/Semantics")

def list_modules():
    """Parse lakefile.toml for [[lean_lib]] names."""
    import re
    try:
        text = open(f"{LAKE_WORKDIR}/lakefile.toml").read()
        return re.findall(r'^name\s*=\s*"(\w+)"', text, re.MULTILINE)
    except: return []

class BuildHandler(BaseHTTPRequestHandler):
    def do_GET(self):
        path = self.path.lstrip("/") or "Semantics"
        if path == "health":
            resp = json.dumps({"status": "ok", "workdir": LAKE_WORKDIR,
                               "modules": list_modules()}).encode()
        else:
            try:
                result = subprocess.run(
                    ["lake", "build", path],
                    capture_output=True, text=True, timeout=600, cwd=LAKE_WORKDIR,
                )
                ok = result.returncode == 0
                output = result.stdout + result.stderr
            except subprocess.TimeoutExpired:
                ok = False; output = "TIMEOUT"
            resp = json.dumps({"passed": ok, "output": output[-2000:]}).encode()
        self.send_response(200)
        self.send_header("Content-Type", "application/json")
        self.send_header("Access-Control-Allow-Origin", "*")
        self.end_headers()
        self.wfile.write(resp)

    def log_message(self, format, *args):
        sys.stderr.write("[build-server] %s\n" % (format % args))

HTTPServer(("0.0.0.0", 8765), BuildHandler).serve_forever()