Skip to content

Commit

Permalink
chore: remove some dead code in the port status script (#2254)
Browse files Browse the repository at this point in the history
Untested
  • Loading branch information
eric-wieser committed Feb 13, 2023
1 parent 0efa848 commit 10bfe18
Showing 1 changed file with 1 addition and 19 deletions.
20 changes: 1 addition & 19 deletions scripts/make_port_status.py
Original file line number Diff line number Diff line change
Expand Up @@ -27,16 +27,6 @@
source_module_re = re.compile(r"^! .*source module (.*)$")
commit_re = re.compile(r"^! (leanprover-community/[a-z]*) commit ([0-9a-f]*)")
import_re = re.compile(r"^import ([^ ]*)")
synchronized_re = re.compile(r".*SYNCHRONIZED WITH MATHLIB4.*")

# Not using re.compile as this is passed to git which uses a different regex dialect:
# https://www.sjoerdlangkemper.nl/2021/08/13/how-does-git-diff-ignore-matching-lines-work/
comment_git_re = r'\`(' + r'|'.join([
re.escape("> THIS FILE IS SYNCHRONIZED WITH MATHLIB4."),
re.escape("> https://github.com/leanprover-community/mathlib4/pull/") + r"[0-9]*",
re.escape("> Any changes to this file require a corresponding PR to mathlib4."),
r"",
]) + r")" + "\n"

def mk_label(path: Path) -> str:
rel = path.relative_to(Path(mathlib3_root))
Expand All @@ -59,8 +49,6 @@ def condense(s):
continue
graph.add_node(mk_label(path))

synchronized = dict()

for path in Path(mathlib3_root).glob('**/*.lean'):
if path.relative_to(mathlib3_root).parts[0] in ['tactic', 'meta']:
continue
Expand All @@ -77,8 +65,6 @@ def condense(s):
else:
imported = 'lean_core.' + imported
graph.add_edge(imported, label)
if synchronized_re.match(line):
synchronized[label] = True

def get_mathlib4_module_commit_info(contents):
module = repo = commit = None
Expand Down Expand Up @@ -154,10 +140,6 @@ def get_mathlib4_module_commit_info(contents):
_, repo, commit = get_mathlib4_module_commit_info(f.stdout.decode())
prs_of_condensed.setdefault(condense(l), []).append({'pr': num, 'repo': repo, 'commit': commit, 'fname': l})

def pr_to_str(pr):
labels = ' '.join(f'[{l.name}]' for l in pr.labels)
return f'[#{pr.number}]({pr.html_url}) (by {pr.user.login}, {labels}, last activity {pr.updated_at})'

COMMENTS_URL = "https://raw.githubusercontent.com/wiki/leanprover-community/mathlib4/port-comments.md"
comments_dict = yaml.safe_load(requests.get(COMMENTS_URL).content.replace(b"```", b""))

Expand All @@ -173,7 +155,7 @@ def pr_to_str(pr):
)
pr_status = f"mathlib4#{data[node]['mathlib4_pr']}" if data[node]['mathlib4_pr'] is not None else "_"
sha = data[node]['source']['commit'] if data[node]['source']['repo'] == 'leanprover-community/mathlib' else "_"

status = f"Yes {pr_status} {sha}"
else:
new_status = dict(ported=False)
Expand Down

0 comments on commit 10bfe18

Please sign in to comment.