Skip to content

Add systematic result metadata summarization - #25

Merged
tadamcz merged 1 commit into
mainfrom
codex/systematic-metadata-summaries
Aug 23, 2026
Merged

Add systematic result metadata summarization#25
tadamcz merged 1 commit into
mainfrom
codex/systematic-metadata-summaries

Conversation

@tadamcz

@tadamcz tadamcz commented Aug 23, 2026

Copy link
Copy Markdown
Collaborator

Summary

  • add Inspect tasks for Lite sequence, conjecture, and accepted-proof summaries
  • preserve the interactive, network-isolated Lean sandbox for proof summarization
  • collect normalized root catalogs and per-sample metadata deterministically from eval logs
  • export the root metadata directory alongside selected plaintext runs
  • add fast regression coverage for current dataset loading and the pinned sandbox image

Validation

  • ruff check on all changed Python files
  • strict mypy on all changed Python files
  • 28 focused dataset, registry, pin, and summarization tests
  • constructed 99 sequence, 100 conjecture, and 44 Fable proof samples
  • regenerated Lite catalogs and 44 Fable metadata files in a temporary directory; outputs matched the existing generated files byte for byte
  • exporter dry-run against the results repository reported no changes

Scope

No generated metadata, logs, plaintext runs, or exported results are included in this PR.

Compatibility fixes found while rebasing onto main

The original results-branch implementation referenced the pre-reorganization OEIS metadata paths and older load_subset and image-tag APIs. This branch uses the canonical metadata/snapshots and metadata/derived paths, passes OEIS_DIR to load_subset, and pins the sandbox image build to the OEIS Formal Conjectures commit.

A model-backed Inspect eval and Docker rebuild were not rerun for this PR; task construction and compose generation were verified without starting Docker.

@tadamcz
tadamcz merged commit 1c0bc6e into main Aug 23, 2026
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant