Spaces:
Running
Running
feat(resilience): add circuit-breaker + observability patches (Doctrine v12, ADDITIVE). resilience/szl_breaker.py: pybreaker+tenacity CLOSED/OPEN/HALF-OPEN wrapper. resilience/szl_exporter.py: Prometheus exporter scraping breaker/healthz state. resilience/status_feed.py: fail-closed internal->public status filter (KEY-name allowlist). HONEST: in-memory buses; Sigstore sig PLACEHOLDER; SLSA L1; no cross-Space tracing. Does NOT modify serve.py/Dockerfile. ZERO BANDAID. Yachay, under CTO authority.
Browse files- resilience/status_feed.py +88 -0
- resilience/szl_breaker.py +123 -0
- resilience/szl_exporter.py +90 -0
resilience/status_feed.py
ADDED
|
@@ -0,0 +1,88 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
# SPDX-License-Identifier: Apache-2.0 · Doctrine v12 (additive). Yachay.
|
| 2 |
+
"""
|
| 3 |
+
status_feed — internal health -> public status_feed.json (fail-closed allow-list).
|
| 4 |
+
Reads Prometheus + active Alertmanager alerts + degradation receipts; emits ONLY the
|
| 5 |
+
szl.status_feed/v1 schema. Anything not explicitly mapped is dropped (never leaked).
|
| 6 |
+
|
| 7 |
+
Honest anti-cover-up: driven by the SAME Prometheus signals as the internal dashboard,
|
| 8 |
+
so the public page can never claim green while internally red. v11 LOCKED untouched.
|
| 9 |
+
"""
|
| 10 |
+
from datetime import datetime, timezone
|
| 11 |
+
|
| 12 |
+
# allow-list: internal flagship -> public component
|
| 13 |
+
PUBLIC_COMPONENT = {
|
| 14 |
+
"a11oy": "Governance & Brand", "amaru": "Memory / Cortex",
|
| 15 |
+
"sentra": "Immune / Policy", "vessels": "Maritime & Receipts",
|
| 16 |
+
"rosie": "Companion", "killinchu": "Drone Ops",
|
| 17 |
+
"lean-kernel": "Proof Kernel",
|
| 18 |
+
}
|
| 19 |
+
# Keys that MUST NEVER appear in the public feed (defense in depth; allow-list already
|
| 20 |
+
# drops them). We match on KEY NAMES (not a substring of the whole blob) so legitimate
|
| 21 |
+
# component copy like "Receipts"/"Companion" is never falsely flagged.
|
| 22 |
+
_NEVER_PUBLISH_KEYS = frozenset({
|
| 23 |
+
"provider", "model", "tripwire", "khipu_node", "digest",
|
| 24 |
+
"hostname", "ip", "secret", "token", "breaker", "circuit",
|
| 25 |
+
})
|
| 26 |
+
|
| 27 |
+
|
| 28 |
+
def _coarse_status(up: bool, degraded: bool, partial: bool) -> str:
|
| 29 |
+
if not up: return "major_outage"
|
| 30 |
+
if partial: return "partial_outage"
|
| 31 |
+
if degraded: return "degraded"
|
| 32 |
+
return "operational"
|
| 33 |
+
|
| 34 |
+
|
| 35 |
+
def build_feed(metrics: dict, alerts: list[dict]) -> dict:
|
| 36 |
+
components = []
|
| 37 |
+
for fl, comp in PUBLIC_COMPONENT.items():
|
| 38 |
+
up = metrics.get(f"szl_up::{fl}", 0) == 1
|
| 39 |
+
degraded = any(a for a in alerts
|
| 40 |
+
if a.get("flagship") == fl and a.get("impact") == "degraded")
|
| 41 |
+
components.append({
|
| 42 |
+
"name": comp,
|
| 43 |
+
"status": _coarse_status(up, degraded, partial=False),
|
| 44 |
+
"uptime_30d": round(metrics.get(f"szl_uptime_30d::{fl}", 0.0), 2),
|
| 45 |
+
})
|
| 46 |
+
# AI Responses component derived from router tiers (impact only, no provider names)
|
| 47 |
+
router_degraded = (metrics.get("szl_router_tier::T0_cache", 0)
|
| 48 |
+
+ metrics.get("szl_router_tier::T1_small", 0)) > 0
|
| 49 |
+
components.append({"name": "AI Responses",
|
| 50 |
+
"status": "degraded" if router_degraded else "operational",
|
| 51 |
+
"note": "Responses may be slower than usual." if router_degraded else None})
|
| 52 |
+
|
| 53 |
+
overall = "operational"
|
| 54 |
+
if any(c["status"] == "major_outage" for c in components): overall = "major_outage"
|
| 55 |
+
elif any(c["status"] == "partial_outage" for c in components): overall = "partial_outage"
|
| 56 |
+
elif any(c["status"] == "degraded" for c in components): overall = "degraded"
|
| 57 |
+
|
| 58 |
+
feed = {"schema": "szl.status_feed/v1",
|
| 59 |
+
"generated_at": datetime.now(timezone.utc).isoformat(),
|
| 60 |
+
"overall": overall, "components": components,
|
| 61 |
+
"active_incidents": _public_incidents(alerts),
|
| 62 |
+
"scheduled_maintenance": []}
|
| 63 |
+
_assert_no_leak(feed) # fail-closed: refuse to emit if any banned key present
|
| 64 |
+
return feed
|
| 65 |
+
|
| 66 |
+
|
| 67 |
+
def _public_incidents(alerts):
|
| 68 |
+
out = []
|
| 69 |
+
for a in alerts:
|
| 70 |
+
if not a.get("customer_impacting"): # only customer-impacting alerts go public
|
| 71 |
+
continue
|
| 72 |
+
out.append({"id": a["incident_id"], "title": a["public_title"], # pre-sanitized
|
| 73 |
+
"impact": a["impact"], "started_at": a["started_at"],
|
| 74 |
+
"latest_update": a["public_update"]})
|
| 75 |
+
return out
|
| 76 |
+
|
| 77 |
+
|
| 78 |
+
def _assert_no_leak(node) -> None:
|
| 79 |
+
"""Recursively assert no banned KEY appears anywhere in the feed (fail-closed)."""
|
| 80 |
+
if isinstance(node, dict):
|
| 81 |
+
for k, v in node.items():
|
| 82 |
+
if str(k).lower() in _NEVER_PUBLISH_KEYS:
|
| 83 |
+
raise RuntimeError(
|
| 84 |
+
f"status_feed leak guard tripped on key '{k}' — refusing to publish")
|
| 85 |
+
_assert_no_leak(v)
|
| 86 |
+
elif isinstance(node, (list, tuple)):
|
| 87 |
+
for item in node:
|
| 88 |
+
_assert_no_leak(item)
|
resilience/szl_breaker.py
ADDED
|
@@ -0,0 +1,123 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
# SPDX-License-Identifier: Apache-2.0
|
| 2 |
+
# © 2026 SZL Holdings · Doctrine v12 (additive over v11 LOCKED). Yachay.
|
| 3 |
+
"""
|
| 4 |
+
szl_breaker — Hystrix-style circuit breakers for every external SZL call.
|
| 5 |
+
|
| 6 |
+
pybreaker = state machine (CLOSED/OPEN/HALF-OPEN).
|
| 7 |
+
tenacity = bounded retry w/ exponential backoff + full jitter.
|
| 8 |
+
We add: per-call timeout, named fallback, and a Khipu degradation receipt
|
| 9 |
+
on every OPEN transition and every fallback execution.
|
| 10 |
+
|
| 11 |
+
ADDITIVE only: this wraps calls; it never alters the 13-axis Yuyay gate, the
|
| 12 |
+
Lambda aggregator, or any LOCKED number (749/14/163, replay-hash bacf5443…631fc5).
|
| 13 |
+
|
| 14 |
+
HONEST: receipt signature is DSSE PLACEHOLDER (Sigstore CI not wired, v11 §9).
|
| 15 |
+
Khipu DAG ingest reuses szl_wire.ingest_receipt (in-memory ring + S3 mirror).
|
| 16 |
+
"""
|
| 17 |
+
from __future__ import annotations
|
| 18 |
+
import functools
|
| 19 |
+
from concurrent.futures import ThreadPoolExecutor, TimeoutError as FutureTimeout
|
| 20 |
+
from datetime import datetime, timezone
|
| 21 |
+
from typing import Any, Callable
|
| 22 |
+
|
| 23 |
+
import pybreaker
|
| 24 |
+
from tenacity import (retry, stop_after_attempt, wait_exponential_jitter,
|
| 25 |
+
retry_if_exception_type)
|
| 26 |
+
|
| 27 |
+
try:
|
| 28 |
+
from szl_wire import ingest_receipt, SIGNATURE_PLACEHOLDER # reuse the live DAG
|
| 29 |
+
except Exception: # edge / standalone import
|
| 30 |
+
SIGNATURE_PLACEHOLDER = "PLACEHOLDER — Sigstore CI not wired (Doctrine v12)"
|
| 31 |
+
def ingest_receipt(receipt: dict) -> dict: # local fallback writer
|
| 32 |
+
return {"receipt": receipt, "note": "local-only ingest (no szl_wire)"}
|
| 33 |
+
|
| 34 |
+
_POOL = ThreadPoolExecutor(max_workers=16)
|
| 35 |
+
|
| 36 |
+
|
| 37 |
+
def _emit_degradation(breaker_name: str, flagship: str, failure_mode: str,
|
| 38 |
+
fallback_tier: str, state: str, traceparent: str | None) -> None:
|
| 39 |
+
"""Append a szl.degradation.receipt/v1 to the canonical Khipu DAG (RUWAY-only path)."""
|
| 40 |
+
ingest_receipt({
|
| 41 |
+
"schema": "szl.degradation.receipt/v1",
|
| 42 |
+
"event_id": f"deg-{datetime.now(timezone.utc).isoformat()}-{flagship}-{breaker_name}",
|
| 43 |
+
"flagship": flagship,
|
| 44 |
+
"failure_mode": failure_mode,
|
| 45 |
+
"circuit": breaker_name,
|
| 46 |
+
"breaker_state": state,
|
| 47 |
+
"fallback_tier_served": fallback_tier,
|
| 48 |
+
"detected_at": datetime.now(timezone.utc).isoformat(),
|
| 49 |
+
"user_visible": True,
|
| 50 |
+
"traceparent": traceparent,
|
| 51 |
+
"doctrine": "v12",
|
| 52 |
+
"dsse": {"sig": SIGNATURE_PLACEHOLDER, "keyid": "PENDING"},
|
| 53 |
+
})
|
| 54 |
+
|
| 55 |
+
|
| 56 |
+
class KhipuListener(pybreaker.CircuitBreakerListener):
|
| 57 |
+
"""Emit a Khipu receipt on every breaker state transition (honest audit trail)."""
|
| 58 |
+
def __init__(self, name: str, flagship: str, failure_mode: str, fallback_tier: str):
|
| 59 |
+
self.name, self.flagship = name, flagship
|
| 60 |
+
self.failure_mode, self.fallback_tier = failure_mode, fallback_tier
|
| 61 |
+
def state_change(self, cb, old, new):
|
| 62 |
+
_emit_degradation(self.name, self.flagship, self.failure_mode,
|
| 63 |
+
self.fallback_tier, str(new.name).upper(), None)
|
| 64 |
+
|
| 65 |
+
|
| 66 |
+
def make_breaker(name: str, flagship: str, failure_mode: str, fallback_tier: str,
|
| 67 |
+
fail_max: int = 5, reset_timeout_s: int = 15) -> pybreaker.CircuitBreaker:
|
| 68 |
+
return pybreaker.CircuitBreaker(
|
| 69 |
+
fail_max=fail_max,
|
| 70 |
+
reset_timeout=reset_timeout_s,
|
| 71 |
+
listeners=[KhipuListener(name, flagship, failure_mode, fallback_tier)],
|
| 72 |
+
name=name,
|
| 73 |
+
)
|
| 74 |
+
|
| 75 |
+
|
| 76 |
+
def guarded_call(breaker: pybreaker.CircuitBreaker, *, flagship: str, failure_mode: str,
|
| 77 |
+
fallback_tier: str, timeout_s: float, retry_budget: int,
|
| 78 |
+
fallback: Callable[[], Any], traceparent: str | None = None):
|
| 79 |
+
"""
|
| 80 |
+
Decorator: wraps an external call with breaker + timeout + bounded retry + fallback.
|
| 81 |
+
On OPEN (short-circuit) or exhausted retries, runs `fallback` and emits a Khipu receipt.
|
| 82 |
+
"""
|
| 83 |
+
def deco(fn: Callable[..., Any]) -> Callable[..., Any]:
|
| 84 |
+
@retry(stop=stop_after_attempt(max(1, retry_budget + 1)),
|
| 85 |
+
wait=wait_exponential_jitter(initial=1, max=300),
|
| 86 |
+
retry=retry_if_exception_type(Exception), reraise=True)
|
| 87 |
+
def _attempt(*a, **k):
|
| 88 |
+
fut = _POOL.submit(fn, *a, **k)
|
| 89 |
+
try:
|
| 90 |
+
return fut.result(timeout=timeout_s) # per-call hard timeout
|
| 91 |
+
except FutureTimeout:
|
| 92 |
+
raise TimeoutError(f"{breaker.name} exceeded {timeout_s}s")
|
| 93 |
+
|
| 94 |
+
@functools.wraps(fn)
|
| 95 |
+
def wrapper(*a, **k):
|
| 96 |
+
try:
|
| 97 |
+
return breaker.call(_attempt, *a, **k) # breaker tracks success/fail
|
| 98 |
+
except pybreaker.CircuitBreakerError: # OPEN → short-circuit
|
| 99 |
+
_emit_degradation(breaker.name, flagship, failure_mode,
|
| 100 |
+
fallback_tier, "OPEN", traceparent)
|
| 101 |
+
return fallback()
|
| 102 |
+
except Exception: # retries exhausted
|
| 103 |
+
_emit_degradation(breaker.name, flagship, failure_mode,
|
| 104 |
+
fallback_tier, "FALLBACK", traceparent)
|
| 105 |
+
return fallback()
|
| 106 |
+
return wrapper
|
| 107 |
+
return deco
|
| 108 |
+
|
| 109 |
+
|
| 110 |
+
# Breaker registry helper (names match OBSERVABILITY_DASHBOARD §3 + CIRCUIT_BREAKER_LAYER §1)
|
| 111 |
+
REGISTRY = {}
|
| 112 |
+
|
| 113 |
+
def register(name: str, flagship: str, failure_mode: str, fallback_tier: str,
|
| 114 |
+
fail_max: int = 5, reset_timeout_s: int = 15) -> pybreaker.CircuitBreaker:
|
| 115 |
+
b = make_breaker(name, flagship, failure_mode, fallback_tier, fail_max, reset_timeout_s)
|
| 116 |
+
REGISTRY[name] = b
|
| 117 |
+
return b
|
| 118 |
+
|
| 119 |
+
|
| 120 |
+
def breaker_states() -> dict[str, int]:
|
| 121 |
+
"""For /healthz: 0=CLOSED, 1=HALF_OPEN, 2=OPEN per registered breaker."""
|
| 122 |
+
m = {"closed": 0, "half-open": 1, "open": 2}
|
| 123 |
+
return {n: m.get(str(b.current_state).lower(), -1) for n, b in REGISTRY.items()}
|
resilience/szl_exporter.py
ADDED
|
@@ -0,0 +1,90 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
# SPDX-License-Identifier: Apache-2.0
|
| 2 |
+
# © 2026 SZL Holdings · Doctrine v12 (additive). Yachay.
|
| 3 |
+
"""
|
| 4 |
+
szl_exporter — scrapes each Space's honest in-process state and re-exposes it as
|
| 5 |
+
Prometheus metrics for the single-pane Grafana dashboard (OBSERVABILITY_DASHBOARD.md).
|
| 6 |
+
|
| 7 |
+
Reads /api/<space>/healthz, /v1/mesh/state, /v1/brain/sockets, vessels ledger,
|
| 8 |
+
lean-kernel /api/lean/theorems.
|
| 9 |
+
|
| 10 |
+
HONEST: it reports what the Spaces actually expose. Where a Space has no metric yet
|
| 11 |
+
(e.g. a static Space has no latency histogram), the series is simply absent, not faked.
|
| 12 |
+
The in-process buses + Khipu DAG are in-memory ring buffers (per szl_wire.py); the
|
| 13 |
+
durable record is the S3 mirror (BACKUP_AND_RECOVERY.md). v11 LOCKED numbers untouched.
|
| 14 |
+
"""
|
| 15 |
+
from prometheus_client import Gauge, start_http_server
|
| 16 |
+
import httpx, time
|
| 17 |
+
|
| 18 |
+
SPACES = {
|
| 19 |
+
"a11oy": "https://szlholdings-a11oy.hf.space",
|
| 20 |
+
"amaru": "https://szlholdings-amaru.hf.space",
|
| 21 |
+
"sentra": "https://szlholdings-sentra.hf.space",
|
| 22 |
+
"vessels": "https://szlholdings-vessels.hf.space",
|
| 23 |
+
"rosie": "https://szlholdings-rosie.hf.space",
|
| 24 |
+
"killinchu": "https://szlholdings-killinchu.hf.space",
|
| 25 |
+
"lean-kernel": "https://szlholdings-lean-kernel.hf.space",
|
| 26 |
+
}
|
| 27 |
+
|
| 28 |
+
up = Gauge("szl_up", "flagship up (1) or down (0)", ["flagship"])
|
| 29 |
+
dag_depth = Gauge("szl_khipu_dag_depth", "Khipu DAG depth (ring buffer)", ["chain"])
|
| 30 |
+
integ = Gauge("szl_khipu_integrity_ok", "Khipu integrity (1 ok / 0 mismatch)", ["chain"])
|
| 31 |
+
lean_dec = Gauge("szl_lean_declarations", "lean-kernel total declarations (live build)")
|
| 32 |
+
lean_sry = Gauge("szl_lean_sorry", "lean-kernel sorry count (live build)")
|
| 33 |
+
lean_axi = Gauge("szl_lean_axiom", "lean-kernel axiom count (live build)")
|
| 34 |
+
|
| 35 |
+
# LOCKED reference (Doctrine v11/v12) — surfaced alongside the live build, never edited.
|
| 36 |
+
LOCKED = Gauge("szl_lean_locked_reference", "Doctrine LOCKED reference numbers", ["kind"])
|
| 37 |
+
|
| 38 |
+
|
| 39 |
+
def _recompute_integrity(nodes: list[dict]) -> int:
|
| 40 |
+
"""Honest hash-chain check: digest must equal sha256(receipt sorted-json || parents)."""
|
| 41 |
+
import hashlib, json
|
| 42 |
+
prev = None
|
| 43 |
+
for n in nodes:
|
| 44 |
+
h = hashlib.sha256()
|
| 45 |
+
h.update(json.dumps(n.get("receipt", {}), sort_keys=True).encode())
|
| 46 |
+
for p in n.get("parents", []):
|
| 47 |
+
h.update(p.encode())
|
| 48 |
+
if n.get("digest") and n["digest"] != h.hexdigest():
|
| 49 |
+
return 0
|
| 50 |
+
prev = n.get("digest")
|
| 51 |
+
return 1
|
| 52 |
+
|
| 53 |
+
|
| 54 |
+
def scrape_once():
|
| 55 |
+
for name, base in SPACES.items():
|
| 56 |
+
try:
|
| 57 |
+
h = httpx.get(f"{base}/api/{name}/healthz", timeout=10)
|
| 58 |
+
up.labels(name).set(1 if h.status_code == 200 else 0)
|
| 59 |
+
except Exception:
|
| 60 |
+
up.labels(name).set(0) # honest: probe failed -> down
|
| 61 |
+
|
| 62 |
+
# Khipu DAG depth + integrity from vessels ledger read-view
|
| 63 |
+
try:
|
| 64 |
+
led = httpx.get(f"{SPACES['vessels']}/api/vessels/v1/receipts/ledger", timeout=10).json()
|
| 65 |
+
nodes = led.get("nodes", [])
|
| 66 |
+
dag_depth.labels("canonical").set(len(nodes))
|
| 67 |
+
integ.labels("canonical").set(_recompute_integrity(nodes))
|
| 68 |
+
except Exception:
|
| 69 |
+
integ.labels("canonical").set(0)
|
| 70 |
+
|
| 71 |
+
# Lean-kernel live build numbers (surfaced next to LOCKED reference)
|
| 72 |
+
try:
|
| 73 |
+
th = httpx.get(f"{SPACES['lean-kernel']}/api/lean/theorems", timeout=15).json()["summary"]
|
| 74 |
+
lean_dec.set(th.get("total_declarations", 0))
|
| 75 |
+
lean_sry.set(th.get("sorry", 0))
|
| 76 |
+
lean_axi.set(th.get("axiom", 0))
|
| 77 |
+
except Exception:
|
| 78 |
+
pass
|
| 79 |
+
|
| 80 |
+
# LOCKED reference (never edited): 749 declarations / 14 unique axioms / 163 sorries
|
| 81 |
+
LOCKED.labels("declarations").set(749)
|
| 82 |
+
LOCKED.labels("unique_axioms").set(14)
|
| 83 |
+
LOCKED.labels("sorries").set(163)
|
| 84 |
+
|
| 85 |
+
|
| 86 |
+
if __name__ == "__main__":
|
| 87 |
+
start_http_server(9100) # Prometheus scrapes :9100/metrics
|
| 88 |
+
while True:
|
| 89 |
+
scrape_once()
|
| 90 |
+
time.sleep(15)
|