Skip to content

Commit aa4a555

Browse files
authored
Merge pull request #13 from bentoner/lean-liquid-clean-up-change
Use same deletion logic for lean-liquid as for mathlib
2 parents eabf115 + 20151a1 commit aa4a555

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

cleanup.py

+4-4
Original file line numberDiff line numberDiff line change
@@ -21,17 +21,17 @@ def is_deletable_mathlib(sha, creation_time):
2121
and sha not in mathlib_master_commits \
2222
and current_time - creation_time > DURATION
2323

24-
# archives from e.g. lean-liquid are only saved if they come from recent master commits
24+
# archives from e.g. lean-liquid follow the same logic as mathlib
2525
def is_deletable_external(repo, sha, creation_time):
2626
if repo not in external_repo_info:
2727
new_cloned_repo = git.Repo.clone_from(f'https://{github_token}@github.com/leanprover-community/{repo}.git',repo)
2828
external_repo_info[repo] = {
2929
'branch_heads': set(r.commit.hexsha for r in new_cloned_repo.refs),
3030
'master_commits': set(c.hexsha for c in new_cloned_repo.iter_commits('master')),
31-
'master_head': new_cloned_repo.rev_parse('origin/master'),
3231
}
33-
return sha not in external_repo_info[repo]['master_commits'] or \
34-
(current_time - creation_time > DURATION and sha != external_repo_info[repo]['master_head'])
32+
return sha not in external_repo_info[repo]['branch_heads'] \
33+
and sha not in external_repo_info[repo]['master_commits'] \
34+
and current_time - creation_time > DURATION
3535

3636
def is_deletable(path, creation_time):
3737
if '/' not in path: # this archive came from mathlib

0 commit comments

Comments
 (0)