mathlib4 present files colored

`--mathlib4` flags turns this on

mathlibtools/leanproject.py

@@ -302,13 +302,16 @@ def global_upgrade() -> None:
               help='Color by mathlib4 porting status')
 @click.option('--port-status-url', default=None,
               help='URL of yaml with mathlib4 port status')
+@click.option('--mathlib4', default=None,
+              help='Local directory of mathlib4 repo')
 @click.argument('output', default='import_graph.dot')
 def import_graph(
     to: Optional[str],
     from_: Optional[str],
     exclude : bool,
     port_status: bool,
     port_status_url: Optional[str],
+    mathlib4: Optional[str],
     output: str
 ) -> None:
     """Write an import graph for this project.
@@ -326,7 +329,7 @@ def import_graph(
         graph = graph.exclude_tactics()
         project._import_graph = graph
     if port_status or port_status_url:
-        project.port_status(port_status_url)
+        project.port_status(port_status_url, mathlib4=None if mathlib4 is None else Path(mathlib4))
     if to and from_:
         G = graph.path(start=from_, end=to)
     elif to:

mathlibtools/lib.py

@@ -1012,14 +1012,23 @@ def pull(self, remote: str='origin') -> None:
                 self.run_echo(['leanpkg', 'configure'])
             self.get_mathlib_olean()
 
-    def port_status(self, url: Optional[str] = None) -> None:
+    def port_status(self, url: Optional[str] = None, mathlib4: Optional[Path] = None) -> None:
         """
         Color nodes on the graph based on port status. Done in place to the graph nodes.
 
         Args:
             url: md or yaml file with "file: label" content, by default, from the wiki
         """
 
+        def snake_to_camel(filename: str) -> str:
+            return re.sub('(?!^)([A-Z]+)', r'_\1', filename).lower()
+
+        existing_files = set()
+        if mathlib4:
+            mathlib4 = mathlib4 / "Mathlib"
+            existing_files = {str.join(".",
+                map(snake_to_camel, leanfile.relative_to(mathlib4).with_suffix("").parts)).lower()
+                for leanfile in mathlib4.rglob("*") if leanfile.suffix == ".lean"}
 
         port_status = PortStatus.deserialize_old(PortStatus.old_yaml())
 
@@ -1044,8 +1053,10 @@ def port_status(self, url: Optional[str] = None) -> None:
             if degree > 0 or target_node["status"].comments:
                 continue
             target_node["status"].comments = "ready"
-        for _, node in self.import_graph.nodes(data=True):
+        for node_name, node in self.import_graph.nodes(data=True):
             if not node.get("status"):
                 continue
             node["style"] = "filled"
             node["fillcolor"] = node["status"].color()
+            if node_name in existing_files:
+                node["color"] = "red"