#!/usr/bin/env bash # lib/metrics.sh — performance measurements for performance mode. # # Functions: # proof_metric_start # proof_metric_stop # writes elapsed_ms # proof_metric_value [unit] # proof_sample_rss # MB # proof_compute_percentile # 50, 95, 99 # # All metrics emit to: # $PROOF_REPORT_DIR/raw/metrics/.jsonl _proof_metric_emit() { local case_id="$1" name="$2" value="$3" unit="$4" detail="$5" local out="${PROOF_REPORT_DIR}/raw/metrics/${case_id}.jsonl" mkdir -p "$(dirname "$out")" local e_detail e_detail=$(printf '%s' "$detail" | jq -Rs .) cat >> "$out" < "$f" } proof_metric_stop() { local case_id="$1" name="$2" local f="${PROOF_REPORT_DIR}/raw/metrics/_timer_${case_id}_${name}" if [ ! -f "$f" ]; then echo "[metrics] timer ${name} for case ${case_id} not started" >&2 return 1 fi local start_ms end_ms elapsed_ms start_ms=$(cat "$f") end_ms=$(date +%s%3N) elapsed_ms=$((end_ms - start_ms)) rm -f "$f" _proof_metric_emit "$case_id" "${name}_ms" "$elapsed_ms" "ms" "" echo "$elapsed_ms" } proof_metric_value() { local case_id="$1" name="$2" value="$3" unit="${4:-}" _proof_metric_emit "$case_id" "$name" "$value" "$unit" "" } # Sample resident-set-size (MB) for the first matching process. proof_sample_rss() { local case_id="$1" pattern="$2" local pid rss_kb rss_mb pid=$(pgrep -f "$pattern" | head -1) if [ -z "$pid" ]; then _proof_metric_emit "$case_id" "rss_${pattern//\//_}_mb" 0 "MB" "process not found" return 1 fi rss_kb=$(awk '/^VmRSS:/ {print $2}' "/proc/$pid/status" 2>/dev/null || echo 0) rss_mb=$(awk -v k="$rss_kb" 'BEGIN{printf "%.1f", k/1024}') _proof_metric_emit "$case_id" "rss_${pattern//\//_}_mb" "$rss_mb" "MB" "pid=${pid}" echo "$rss_mb" } # proof_compute_percentile: streams values from a file (one number per # line), prints the requested percentile. proof_compute_percentile() { local file="$1" pct="$2" sort -n "$file" | awk -v pct="$pct" ' { v[NR] = $1 } END { n = NR if (n == 0) { print "0"; exit } idx = int((pct/100.0) * n) if (idx < 1) idx = 1 if (idx > n) idx = n print v[idx] } ' }