From a7aa4a2e6c4ebadf4974167c7c578772b60431c4 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 20 Dec 2022 09:02:03 +0000
Subject: [PATCH] fix(scripts/port_comments): handle moved files (#17978)

---
 scripts/add_port_comments.py | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

diff --git a/scripts/add_port_comments.py b/scripts/add_port_comments.py
index 7bf81c9db5742..35ef63c89ccb7 100644
--- a/scripts/add_port_comments.py
+++ b/scripts/add_port_comments.py
@@ -92,15 +92,20 @@ def fname_for(import_path: str) -> Path:
 
 
 missing_docstrings = []
+missing_files = []
 for iname, f_status in status.file_statuses.items():
     if f_status.ported:
         fname = fname_for(iname)
-        with open(fname) as f:
-            fcontent = f.read()
+        try:
+            with open(fname) as f:
+                fcontent = f.read()
+        except FileNotFoundError:
+            missing_files.append((iname, fname))
+            continue
         try:
             new_fcontent = add_port_status(fcontent, f_status)
         except NoModuleDocstringError:
-            missing_docstrings.append(fname)
+            missing_docstrings.append((iname, fname))
             continue
         if new_fcontent == fcontent:
             continue
@@ -110,6 +115,13 @@ def fname_for(import_path: str) -> Path:
 if missing_docstrings:
     print('\n---')
     print('The following files have no module docstring, so I have not added a message in this PR')
-    for fname in missing_docstrings:
-        print(f'* [`{fname}`](https://github.com/leanprover-community/mathlib/blob/master/{fname})')
+    for iname, fname in missing_docstrings:
+        print(f'* [`{iname}`](https://github.com/leanprover-community/mathlib/blob/master/{fname})')
     print('\nPlease make a PR to add a module docstring (for Lean3 and Lean4!), then I will add the freeze comment next time.')
+if missing_files:
+    print('\n---')
+    print('The following files no longer exist in Lean 3\' mathlib, so I have not added a message in this PR')
+    for iname, fname in missing_files:
+        f_status = status.file_statuses[iname]
+        print(f'* [`{iname}`](https://github.com/leanprover-community/mathlib/blob/{f_status.mathlib3_hash}/{fname})')
+    print('\nIn future we should find where they moved to, and check that the files are still in sync.')