feat: implement catalog and generator overhaul foundations

.github/workflows/ci.yml

@@ -113,6 +113,19 @@ jobs:
       - name: Validate manifest structure and module coverage
         run: lake exe lean-eval validate-manifest --structure-only
 
+      - name: Validate catalog lifecycle metadata and frozen sets
+        env:
+          BASE_SHA: ${{ github.event.pull_request.base.sha || github.event.before }}
+        run: |
+          set -euo pipefail
+          base_args=()
+          if [ -n "$BASE_SHA" ] &&
+              [ "$BASE_SHA" != "0000000000000000000000000000000000000000" ] &&
+              git cat-file -e "$BASE_SHA^{commit}"; then
+            base_args+=(--base-ref "$BASE_SHA")
+          fi
+          python scripts/validate_catalog.py "${base_args[@]}"
+
       # Source-only changes intentionally leave generated/index.json for the
       # trusted main regenerator. If a PR touches generated/ itself, however,
       # its committed global index must be current and it may not add an
@@ -152,7 +165,7 @@ jobs:
           lake exe test_check_comparator_installation
 
       - name: Run Python unit tests
-        run: python tests/python/test_select_ci_problems.py
+        run: python -m unittest discover -s tests/python -p 'test_*.py'
 
   security:
     name: Security and scoring smoke tests

.github/workflows/notify-leaderboard.yml

@@ -14,7 +14,7 @@ on:
       - 'LeanEval/**'
       - 'EvalTools/**'
       - 'templates/**'
-      - 'manifests/problems/**'
+      - 'manifests/**'
       - 'generated/**'
       - 'lakefile.toml'
       - 'lean-toolchain'

.github/workflows/regenerate-main.yml

@@ -9,7 +9,7 @@ on:
       - 'LeanEval/**'
       - 'EvalTools/**'
       - 'templates/**'
-      - 'manifests/problems/**'
+      - 'manifests/**'
       - '.github/workflows/regenerate-main.yml'
       - 'lakefile.toml'
       - 'lean-toolchain'

EvalTools/CheckEvalWorkflow.lean

@@ -69,7 +69,7 @@ private def assertCounts (summary : ScoreSummary) (attempted succeeded : Nat) (l
     throw <| IO.userError <|
       s!"{label} produced unexpected results.\n" ++
       s!"Expected attempted={attempted}, succeeded={succeeded}.\n" ++
-      s!"Actual summary: attempted={summary.attemptedProblems}, succeeded={summary.succeededProblems} (test attempted/succeeded={summary.attemptedTestProblems}/{summary.succeededTestProblems}, main attempted/succeeded={summary.attemptedMainProblems}/{summary.succeededMainProblems})"
+      s!"Actual summary: attempted={summary.attemptedProblems}, succeeded={summary.succeededProblems} (hidden attempted/succeeded={summary.attemptedHiddenProblems}/{summary.succeededHiddenProblems}, visible attempted/succeeded={summary.attemptedVisibleProblems}/{summary.succeededVisibleProblems})"
 
 private def summarizeAtRoot (root : System.FilePath) (problems : Array EvalProblemMetadata)
     (workspacesRoot : System.FilePath) : IO ScoreSummary := do

EvalTools/Generate.lean

@@ -2142,7 +2142,11 @@ private def renderReadmeLines (entry : EvalProblemMetadata)
     entry.title,
     "",
     s!"- Problem ID: `{entry.id}`",
-    s!"- Test Problem: {if entry.test then "yes" else "no"}",
+    s!"- Group: `{entry.group}`",
+    s!"- Status: `{entry.status}`",
+    s!"- Visible: {if entry.visible then "yes" else "no"}",
+    s!"- Statement Revision: {entry.statementRevision}",
+    s!"- Tags: {if entry.tags.isEmpty then "none" else ", ".intercalate entry.tags.toList}",
     s!"- Submitter: {entry.submitter}"
   ]
   if multiHole then
@@ -2767,7 +2771,11 @@ def generatedIndexEntry (entry : EvalProblemMetadata) : OJson :=
   ojObj #[
     ("id", ojStr entry.id),
     ("title", ojStr entry.title),
-    ("test", ojBool entry.test),
+    ("group", ojStr entry.group),
+    ("status", ojStr entry.status),
+    ("visible", ojBool entry.visible),
+    ("statement_revision", ojNat entry.statementRevision),
+    ("tags", ojStrArr entry.tags),
     ("submitter", ojStr entry.submitter),
     ("module", ojStr entry.moduleName),
     ("holes", ojStrArr entry.holes),

EvalTools/Markers.lean

@@ -15,7 +15,17 @@ namespace EvalTools
 structure EvalProblemMetadata where
   id : String
   title : String
-  test : Bool
+  /-- Policy group containing this problem. Valid values are checked by the
+  manifest decoder and the catalog validator. -/
+  group : String
+  /-- Current lifecycle status (`draft`, `active`, or `archived`). -/
+  status : String
+  /-- Whether the problem is shown in public catalog surfaces. -/
+  visible : Bool
+  /-- Monotonic revision of the trusted statement. -/
+  statementRevision : Nat
+  /-- Stable registry keys from `manifests/tags.toml`. -/
+  tags : Array String
   moduleName : String
   /-- The names of the `@[eval_problem]`-tagged declarations in `moduleName` that
   comprise this problem; comparator's `theorem_names` and `definition_names`
@@ -57,11 +67,34 @@ def requireNonempty (field value : String) : EDecodeM String := do
     throwDecodeErrorAt Syntax.missing s!"Manifest field `{field}` must be non-empty."
   pure value
 
+def allowedProblemGroups : Array String :=
+  #["formalization-evaluation", "software-verification", "open-conjectures"]
+
+def allowedProblemStatuses : Array String :=
+  #["draft", "active", "archived"]
+
+def requireOneOf (field value : String) (allowed : Array String) : EDecodeM String := do
+  unless allowed.contains value do
+    throwDecodeErrorAt Syntax.missing
+      s!"Manifest field `{field}` must be one of {", ".intercalate allowed.toList}; got `{value}`."
+  pure value
+
 instance : DecodeToml EvalProblemMetadata where
   decode v := do
     let t ← v.decodeTable
     let id ← requireNonempty "id" (← t.decode `id)
     let title ← requireNonempty "title" (← t.decode `title)
+    let group ← requireOneOf "group" (← t.decode `group) allowedProblemGroups
+    let status ← requireOneOf "status" (← t.decode `status) allowedProblemStatuses
+    let statementRevision : Nat ← t.decode `statement_revision
+    if statementRevision == 0 then
+      throwDecodeErrorAt Syntax.missing
+        s!"Manifest entry `{id}` has statement_revision = 0; revisions start at 1."
+    let tags : Array String ← t.decode `tags
+    for tag in tags do
+      if tag.isEmpty then
+        throwDecodeErrorAt Syntax.missing
+          s!"Manifest entry `{id}` has an empty string in `tags`."
     let moduleName ← requireNonempty "module" (← t.decode `module)
     let holes : Array String ← t.decode `holes
     if holes.isEmpty then
@@ -78,7 +111,11 @@ instance : DecodeToml EvalProblemMetadata where
     return {
       id := id
       title := title
-      test := ← t.decode `test
+      group := group
+      status := status
+      visible := ← t.decode `visible
+      statementRevision := statementRevision
+      tags := tags
       moduleName := moduleName
       holes := holes
       submitter := submitter
@@ -91,8 +128,9 @@ def decodeErrorsToString (errors : Array DecodeError) : String :=
   "\n".intercalate <| errors.toList.map fun err => err.msg
 
 /-- Parse a single per-problem TOML file (top-level keys: `id`, `title`,
-`test`, `module`, `holes`, `submitter`, optional `notes`, `source`,
-`informal_solution`). The caller is responsible for `id ↔ filename` and
+`group`, `status`, `visible`, `statement_revision`, `tags`, `module`, `holes`,
+`submitter`, optional `notes`, `source`, `informal_solution`, and lifecycle
+history arrays). The caller is responsible for `id ↔ filename` and
 cross-file uniqueness checks (see `EvalTools.loadManifest`). -/
 def parseManifestEntry (contents : String) (fileName : String) :
     IO (Except String EvalProblemMetadata) := do
@@ -143,7 +181,11 @@ def formatManifestHover (metadata : EvalProblemMetadata) : String :=
       "",
       s!"- id: `{metadata.id}`",
       s!"- title: {metadata.title}",
-      s!"- test: `{metadata.test}`",
+      s!"- group: `{metadata.group}`",
+      s!"- status: `{metadata.status}`",
+      s!"- visible: `{metadata.visible}`",
+      s!"- statement revision: `{metadata.statementRevision}`",
+      s!"- tags: {", ".intercalate (metadata.tags.toList.map (s!"`{·}`"))}",
       s!"- module: `{metadata.moduleName}`",
       s!"- holes: {", ".intercalate (metadata.holes.toList.map (s!"`{·}`"))}",
       s!"- submitter: {metadata.submitter}"

EvalTools/RunEval.lean

@@ -14,7 +14,7 @@ set_option autoImplicit false
 structure ProblemScore where
   id : String
   title : String
-  test : Bool
+  visible : Bool
   attempted : Bool
   succeeded : Bool
   exitCode : Option UInt32
@@ -25,7 +25,7 @@ def ProblemScore.toOJson (s : ProblemScore) : OJson :=
   ojObj #[
     ("id", ojStr s.id),
     ("title", ojStr s.title),
-    ("test", ojBool s.test),
+    ("visible", ojBool s.visible),
     ("attempted", ojBool s.attempted),
     ("succeeded", ojBool s.succeeded),
     ("exit_code", match s.exitCode with
@@ -104,7 +104,7 @@ def scoreProblems (root : System.FilePath) (problems : Array EvalProblemMetadata
     scores := scores.push {
       id := entry.id
       title := entry.title
-      test := entry.test
+      visible := entry.visible
       attempted := attempted
       succeeded := succeeded
       exitCode := exitCode?
@@ -118,54 +118,54 @@ structure ScoreSummary where
   totalProblems : Nat
   attemptedProblems : Nat
   succeededProblems : Nat
-  attemptedTestProblems : Nat
-  succeededTestProblems : Nat
-  attemptedMainProblems : Nat
-  succeededMainProblems : Nat
+  attemptedHiddenProblems : Nat
+  succeededHiddenProblems : Nat
+  attemptedVisibleProblems : Nat
+  succeededVisibleProblems : Nat
 
 def summarizeScores (scores : Array ProblemScore) : ScoreSummary := Id.run do
   let attempted := scores.filter (·.attempted)
   let succeeded := attempted.filter (·.succeeded)
-  let attemptedTest := scores.filter fun s => s.attempted && s.test
-  let succeededTest := scores.filter fun s => s.succeeded && s.test
-  let attemptedMain := scores.filter fun s => s.attempted && !s.test
-  let succeededMain := scores.filter fun s => s.succeeded && !s.test
+  let attemptedHidden := scores.filter fun s => s.attempted && !s.visible
+  let succeededHidden := scores.filter fun s => s.succeeded && !s.visible
+  let attemptedVisible := scores.filter fun s => s.attempted && s.visible
+  let succeededVisible := scores.filter fun s => s.succeeded && s.visible
   return {
     totalProblems := scores.size
     attemptedProblems := attempted.size
     succeededProblems := succeeded.size
-    attemptedTestProblems := attemptedTest.size
-    succeededTestProblems := succeededTest.size
-    attemptedMainProblems := attemptedMain.size
-    succeededMainProblems := succeededMain.size
+    attemptedHiddenProblems := attemptedHidden.size
+    succeededHiddenProblems := succeededHidden.size
+    attemptedVisibleProblems := attemptedVisible.size
+    succeededVisibleProblems := succeededVisible.size
   }
 
 def summaryToOJson (scores : Array ProblemScore) (s : ScoreSummary) : OJson :=
   ojObj #[
     ("total_problems", ojNat s.totalProblems),
     ("attempted_problems", ojNat s.attemptedProblems),
     ("succeeded_problems", ojNat s.succeededProblems),
-    ("attempted_test_problems", ojNat s.attemptedTestProblems),
-    ("succeeded_test_problems", ojNat s.succeededTestProblems),
-    ("attempted_main_problems", ojNat s.attemptedMainProblems),
-    ("succeeded_main_problems", ojNat s.succeededMainProblems),
+    ("attempted_hidden_problems", ojNat s.attemptedHiddenProblems),
+    ("succeeded_hidden_problems", ojNat s.succeededHiddenProblems),
+    ("attempted_visible_problems", ojNat s.attemptedVisibleProblems),
+    ("succeeded_visible_problems", ojNat s.succeededVisibleProblems),
     ("problems", ojArr (scores.map ProblemScore.toOJson))
   ]
 
 /-- Human-readable summary. Mirrors `render_human_summary`. -/
 def renderHumanSummary (scores : Array ProblemScore) (s : ScoreSummary) : String := Id.run do
   let mut lines : Array String := #[
     s!"Attempted {s.attemptedProblems} / {s.totalProblems} problems; succeeded on {s.succeededProblems}.",
-    s!"Test problems: attempted {s.attemptedTestProblems}; succeeded on {s.succeededTestProblems}.",
-    s!"Main benchmark problems: attempted {s.attemptedMainProblems}; succeeded on {s.succeededMainProblems}."
+    s!"Hidden problems: attempted {s.attemptedHiddenProblems}; succeeded on {s.succeededHiddenProblems}.",
+    s!"Visible problems: attempted {s.attemptedVisibleProblems}; succeeded on {s.succeededVisibleProblems}."
   ]
   for sc in scores do
     let status :=
       if !sc.attempted then "unattempted"
       else if sc.succeeded then "passed"
       else "failed"
-    let testMarker := if sc.test then "test" else "main"
-    lines := lines.push s!"- {sc.id} [{testMarker}]: {status}"
+    let visibility := if sc.visible then "visible" else "hidden"
+    lines := lines.push s!"- {sc.id} [{visibility}]: {status}"
   return "\n".intercalate lines.toList
 
 /-- Filter problems by id. Mirrors `selected_problems`. -/