Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 88e6ad4

Browse files
committed
fix: handle archive and counterexamples correctly when adding port comments (#19237)
1 parent 016138c commit 88e6ad4

File tree

1 file changed

+7
-0
lines changed

1 file changed

+7
-0
lines changed

scripts/add_port_comments.py

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@
1212
status = PortStatus.deserialize_old()
1313

1414
src_path = Path(__file__).parent.parent / 'src'
15+
archive_path = Path(__file__).parent.parent / 'archive'
16+
counterexamples_path = Path(__file__).parent.parent / 'counterexamples'
1517

1618
def make_comment(fstatus):
1719
return textwrap.dedent(f"""\
@@ -87,6 +89,11 @@ def add_port_status(fcontent: str, fstatus: FileStatus) -> str:
8789
return fcontent
8890

8991
def fname_for(import_path: str) -> Path:
92+
for root in [src_path, archive_path, counterexamples_path]:
93+
p = root / Path(*import_path.split('.')).with_suffix('.lean')
94+
if p.exists():
95+
return p
96+
# used only for error messages, a best-guess
9097
return src_path / Path(*import_path.split('.')).with_suffix('.lean')
9198

9299

0 commit comments

Comments
 (0)