Log Query Cookbook

# View full contents
gzcat file.json.gz | jq .

# Pretty-print with less
gzcat file.json.gz | jq . | less

# Query specific fields
gzcat summary.json.gz | jq '.theorems[] | select(.wild_type.solved) | .name'

# Count nodes in proof term
gzcat wild_type_proof_term.json.gz | jq '.nodes | length'

# Search for text patterns in gzipped files
gzcat goal_cache.json.gz | rg "pattern"

# Extract just the keys
gzcat goal_cache.json.gz | jq 'keys'

uv run python -c "
from analysis.summary import CorpusRun
from pathlib import Path
run = CorpusRun.load(Path('logs/corpus-.../'))
print(f'Solved: {len([t for t in run.theorems if t.wild_type_solved])}/{len(run.theorems)}')
"

gzcat summary.json.gz | jq '{
  total: .aggregates.theorem_count,
  solve_rate: .aggregates.wild_type_solve_rate,
  interventions: .aggregates.intervention_count,
  int_rate: .aggregates.intervention_solve_rate
}'

cat theorem_name/wild_type_history.json | jq '.iterations[-5:] | map({iteration, attempts: [.attempts[]? | {tactic, outcome}]})'

cat theorem_name/wild_type_metrics.json | jq '{
  failure_ratio: .detour.failure_ratio,
  unique_tactics: .trajectory.tactic_diversity,
  max_depth: .trajectory.max_depth_reached
}'

cat theorem_name/block_simp_comparison.json | jq '{
  ged: .ged_search_graph.value,
  iter_delta: .trajectory_diff.iteration_diff,
  new_axioms: .axiom_delta
}'

# Compare proof lengths
echo "Wild:" && cat wild_type_graph.json | jq '.nodes | length'
echo "Intervention:" && cat block_simp_graph.json | jq '.nodes | length'

cat sheaf_analysis.json | jq '{
  consistency: .equiv_consistency,
  problematic_families: [.per_family_residual | to_entries[] | select(.value > 20)]
}'

cat sheaf_analysis.json | jq '.inconsistent_cases[:5]'

# List all unique signatures
gzcat goal_cache.json.gz | jq '.entries | keys | length'

# See which signatures have the most occurrences
gzcat goal_cache.json.gz | jq '.entries | to_entries | map({sig: .key[:30], occs: (.value.occurrences | length)}) | sort_by(-.occs) | .[:10]'

# Check outcomes for a specific signature (family 2 = intro)
gzcat goal_cache.json.gz | jq '.entries["<sig>"].occurrences | to_entries[0].value.outcomes'

# Which goal types saw the most tactic attempts
gzcat summary.json.gz | jq '.aggregates.goal_type_tactic_matrix | to_entries | map({goal: .key[:40], tactics: (.value | keys | length)}) | sort_by(-.tactics) | .[:10]'

# Success rate for "intro" on goals containing "→"
gzcat summary.json.gz | jq '.aggregates.goal_type_tactic_matrix | to_entries | map(select(.key | contains("→"))) | .[0].value | to_entries | map({tactic: .key, success: .value.success, fail: .value.failure})'

# See the theorem and step count
gzcat theorem_name/wild_type_assembly.json.gz | jq '{theorem: .theorem[:60], steps: (.steps | length)}'

# Trace each step with goals closed/opened
gzcat theorem_name/wild_type_assembly.json.gz | jq '.steps | to_entries | .[] | "\(.key + 1). \(.value.tactic)  closed=\(.value.goalsClosed | length) opened=\(.value.goalsOpened | length)"'

# See which tactics closed goals
gzcat theorem_name/wild_type_assembly.json.gz | jq '.steps | map(select(.goalsClosed | length > 0)) | .[] | {tactic, closed: (.goalsClosed | length)}'

# Count node types in final proof
gzcat theorem_name/wild_type_assembly.json.gz | jq '.finalTerm.nodes | group_by(.[1].kind) | map({kind: .[0][1].kind, count: length}) | sort_by(-.count)'

# Total nodes in proof term
gzcat theorem_name/wild_type_assembly.json.gz | jq '.finalTerm.nodes | length'

# Check for incomplete proofs (mvar nodes = holes)
gzcat theorem_name/wild_type_assembly.json.gz | jq '.finalTerm.nodes | map(select(.[1].kind == "mvar")) | length'

# Set up aliases for the two runs
RUN1="logs/corpus-2026-01-06-190731"  # ReProver
RUN2="logs/corpus-2026-01-07-120200"  # DeepSeek

# Compare overall solve rates
echo "Run 1:" && gzcat $RUN1/summary.json.gz | jq '.aggregates | {theorems: .theorem_count, rate: .wild_type_solve_rate}'
echo "Run 2:" && gzcat $RUN2/summary.json.gz | jq '.aggregates | {theorems: .theorem_count, rate: .wild_type_solve_rate}'

# Get theorem names that are solved in run1 but failed in run2
comm -23 \
  <(gzcat $RUN1/summary.json.gz | jq -r '.theorems[] | select(.wild_type.solved) | .name' | sort) \
  <(gzcat $RUN2/summary.json.gz | jq -r '.theorems[] | select(.wild_type.solved) | .name' | sort)

# Get theorem names that failed in run1 but solved in run2
comm -13 \
  <(gzcat $RUN1/summary.json.gz | jq -r '.theorems[] | select(.wild_type.solved) | .name' | sort) \
  <(gzcat $RUN2/summary.json.gz | jq -r '.theorems[] | select(.wild_type.solved) | .name' | sort)

# Compare intervention solve rates
gzcat $RUN1/summary.json.gz | jq '{run: "run1", interventions: .aggregates.intervention_count, rate: .aggregates.intervention_solve_rate}'
gzcat $RUN2/summary.json.gz | jq '{run: "run2", interventions: .aggregates.intervention_count, rate: .aggregates.intervention_solve_rate}'

cat analysis_report.json | jq '.by_theorem[] | .theorem as $t | .interventions[] | select(.classification == "TYPE_B_ANISOMORPHIC") | {
  theorem: $t,
  intervention: .name,
  ged: .search_dynamics.ged_search_graph,
  wild_dag: .complexity.wild.dag_size,
  int_dag: .complexity.intervention.dag_size
}'

cat analysis_report.json | jq '.by_theorem[] | .theorem as $t | .interventions[] | select(.complexity.intervention.dag_size < .complexity.wild.dag_size) | {
  theorem: $t,
  intervention: .name,
  reduction: (.complexity.wild.dag_size - .complexity.intervention.dag_size)
}' | head -20

# 1. See the theorem
cat theorem_name/wild_type_history.json | jq -r '.theorem'

# 2. Trace each step
cat theorem_name/wild_type_history.json | jq -r '.iterations[] | .iteration as $i | .attempts[]? | "\($i): \(.tactic) -> \(.outcome)"'

# 3. Check where it got stuck
cat theorem_name/wild_type_history.json | jq '.iterations | map(select([.attempts[].outcome] | index("success") | not)) | .[0]'

# 4. See the proof graph structure
cat theorem_name/wild_type_graph.json | jq '{
  nodes: (.nodes | length),
  edges: (.edges | length),
  root_type: .nodes[0].type
}'