From 88e6ad41d9c5d6da7e2ac45cae6d07a7fc6bb429 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sun, 16 Jul 2023 09:47:04 +0000 Subject: [PATCH] fix: handle archive and counterexamples correctly when adding port comments (#19237) --- scripts/add_port_comments.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/scripts/add_port_comments.py b/scripts/add_port_comments.py index 5c0160b5f9b56..366942aa8640f 100644 --- a/scripts/add_port_comments.py +++ b/scripts/add_port_comments.py @@ -12,6 +12,8 @@ status = PortStatus.deserialize_old() src_path = Path(__file__).parent.parent / 'src' +archive_path = Path(__file__).parent.parent / 'archive' +counterexamples_path = Path(__file__).parent.parent / 'counterexamples' def make_comment(fstatus): return textwrap.dedent(f"""\ @@ -87,6 +89,11 @@ def add_port_status(fcontent: str, fstatus: FileStatus) -> str: return fcontent def fname_for(import_path: str) -> Path: + for root in [src_path, archive_path, counterexamples_path]: + p = root / Path(*import_path.split('.')).with_suffix('.lean') + if p.exists(): + return p + # used only for error messages, a best-guess return src_path / Path(*import_path.split('.')).with_suffix('.lean')