feat: add depends on rocq concept status

scripts/DumpPortingData.lean

@@ -46,6 +46,11 @@ meta def collectRocqAliases (env : Environment) : Array (Name × Name) :=
 private meta def nameToRocqStr (n : Name) : String :=
   n.toString (escape := false)
 
+meta def buildStatusJson : Status → Json 
+| .Ported => "ported"
+| .Missing => "missing"
+| .DependsOn ls => Json.mkObj [("depends_on", Json.arr <| ls.map (Json.str ·.toString))]
+
 /-- Build a JSON object from collected data. -/
 meta def buildJson (aliases : Array (Name × Name))
     (ignores : Array (Name × String))
@@ -60,7 +65,7 @@ meta def buildJson (aliases : Array (Name × Name))
   let conceptArr := concepts.map fun (folder, feature, sub, status, reason) =>
     Json.mkObj [("folder", folder), ("feature", feature),
       ("subfeature", match sub with | some s => Json.str s | none => Json.null),
-      ("status", status.toString), ("reason", reason)]
+      ("status", buildStatusJson status), ("reason", reason)]
   Json.mkObj [("aliases", Json.arr aliasArr), ("ignores", Json.arr ignoreArr),
     ("ignored_files", Json.arr ignoreFileArr), ("concepts", Json.arr conceptArr)]
 

scripts/check_porting.py

@@ -267,7 +267,7 @@ class ConceptEntry:
     dir: str       # e.g. "proofmode/"
     feature: str   # e.g. "IPM Tactics"
     subfeature: str  # e.g. "iIntros" or "" for top-level
-    status: str    # "ported" | "missing"
+    status: str    # "ported" | "missing" | "blocked" | "unreachable" (should not happen)
     reason: str
 
 
@@ -278,7 +278,16 @@ class LeanData:
     ignored_files: dict[str, str]
     concepts: list[ConceptEntry]
 
-
+def parse_status(status : str | dict[str, list[str]]) -> str:
+    if type(status) is str:
+        # ported | missing
+        return status
+    elif type(status) is dict and [*status.keys()][0] == "depends_on":
+        # blocked
+        return "blocked"
+    else: # Should be unreachable
+        return "unreachable"
+
 def load_lean_data(json_path: str) -> LeanData:
     """Load Lean alias/ignore/concept data from the JSON dump."""
     with open(json_path) as f:
@@ -293,7 +302,7 @@ def load_lean_data(json_path: str) -> LeanData:
         ConceptEntry(
             dir=c["folder"], feature=c["feature"],
             subfeature=c.get("subfeature") or "",
-            status=c["status"], reason=c["reason"],
+            status=parse_status(c["status"]), reason=c["reason"],
         )
         for c in data.get("concepts", [])
     ]

src/Iris/Std/RocqPorting.lean

@@ -153,8 +153,13 @@ elab "#rocq_ignore_file" folder:ident file:str reason:str : command => do
   checkRocqFolder folder
   modifyEnv (rocqIgnoreFileExt.addEntry · (folder.getId.toString, file.getString, reason.getString))
 
+public inductive Status where
+  | Ported
+  | Missing
+  | DependsOn (deps: Array Name)
+
 /-- A concept entry: `(dir, feature, subfeature?, status, reason)`. -/
-public abbrev ConceptEntry := String × String × Option String × Name × String
+public abbrev ConceptEntry := String × String × Option String × Status × String
 
 /-- Environment extension tracking all `#rocq_concept` entries. -/
 public meta initialize rocqConceptExt : SimplePersistentEnvExtension ConceptEntry (Array ConceptEntry) ←
@@ -163,6 +168,17 @@ public meta initialize rocqConceptExt : SimplePersistentEnvExtension ConceptEntr
     addImportedFn := fun es => es.foldl (fun acc a => a.foldl Array.push acc) #[]
   }
 
+public syntax status := "ported" <|> "missing" <|> ("depends_on" "[" ident,+ "]")
+
+syntax (name := rocq_concept) "#rocq_concept" ident str (str)? status str : command
+
+variable {m : Type → Type} [Monad m] [MonadError m] in
+meta def parseStatus : TSyntax `status → m Status 
+| `(status| ported) =>  return .Ported
+| `(status| missing) => return .Missing
+| `(status| depends_on [ $[$deps:ident],* ]) => return .DependsOn (deps.map (·.raw.getId))
+| stx => throwErrorAt stx s!"unsupported status: {stx.raw.getId}"
+
 /-- Track a Rocq concept (feature or sub-feature) that doesn't map to individual
 definitions. The folder is a top-level Rocq source directory keyword (`algebra`,
 `base_logic`, `bi`, `program_logic`, `proofmode`, `si_logic`). Status must be
@@ -175,10 +191,8 @@ under the feature in the HTML report.
 ```
 -/
 @[expose]
-elab "#rocq_concept" folder:ident feature:str sub:(str)? status:ident reason:str : command => do
+elab "#rocq_concept" folder:ident feature:str sub:(str)? status:status reason:str : command => do
   checkRocqFolder folder
-  let statusName := status.getId
-  unless statusName == `ported || statusName == `missing do
-    throwErrorAt status "status must be 'ported' or 'missing', got '{statusName}'"
+  let status ← parseStatus status
   let sub := sub.map (·.getString)
-  modifyEnv (rocqConceptExt.addEntry · (folder.getId.toString, feature.getString, sub, statusName, reason.getString))
+  modifyEnv (rocqConceptExt.addEntry · (folder.getId.toString, feature.getString, sub, status, reason.getString))