diff --git a/NOTICE b/NOTICE index 1c21a64e70..462840e5bd 100644 --- a/NOTICE +++ b/NOTICE @@ -116,9 +116,6 @@ MIT permission notice that follows them. LeanPool/PolyaEnumerationTheorem https://github.com/Luka-O/polya-enumeration-theorem Copyright (c) 2024 Luka-O - LeanPool/PrimeCert https://github.com/b-mehta/PrimeCert - Copyright (c) 2026 Bhavik Mehta - LeanPool/QuasiBorelSpaces https://github.com/YellPika/quasi-borel-spaces Copyright (c) 2025 Anthony Vandikas, Kiarash Sotoudeh diff --git a/candidates/README.md b/candidates/README.md index b197194ec6..defac5c968 100644 --- a/candidates/README.md +++ b/candidates/README.md @@ -233,7 +233,6 @@ Do not edit the autogenerated section by hand. | 11 | [WuProver/MonomialOrderedPolynomial](https://github.com/WuProver/MonomialOrderedPolynomial) | Monomial ordered polynomial implementation in Lean4 | Apache-2.0 | v4.29.0-rc8 | 4,816 | 2026-04-10 | ✗ | | | 11 | [Zetetic-Dhruv/formal-learning-theory-kernel](https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel) | Lean4 kernel for synthetic formalization and discovery of statistical learning theory. First and complete formalization… | | v4.29.0-rc6 | 31,925 | 2026-04-29 | – | ✓ | | 11 | [znssong/SetTheory](https://github.com/znssong/SetTheory) | A formalization project of set theory and elementary embeddings in Lean 4. Includes a proof of Kunen's inconsistency th… | Apache-2.0 | v4.29.0-rc4 | 2,860 | 2026-05-10 | – | ✓ | -| 10 | [b-mehta/PrimeCert](https://github.com/b-mehta/PrimeCert) | Formal prime certificates in Lean 4 | MIT | v4.32.0-rc1 | 1,936 | 2026-06-17 | ✓ | ✓ | | 10 | [Brunn-Minkowski-in-Lean/BrunnMinkowski](https://github.com/Brunn-Minkowski-in-Lean/BrunnMinkowski) | | | v4.19.0-rc2 | 1,731 | 2026-05-10 | – | | | 10 | [calcu16/lean_complexity](https://github.com/calcu16/lean_complexity) | Complexity analysis in Lean | | v4.5.0-rc1 | 5,595 | 2025-02-04 | – | | | 10 | [DavePearce/LeanEVM](https://github.com/DavePearce/LeanEVM) | A toy implementation of the EVM in Lean4. | Apache-2.0 | v4.8.0-rc2 | 818 | 2024-05-29 | ✗ | | diff --git a/candidates/decisions.jsonl b/candidates/decisions.jsonl index 8370c49338..5574e7b70c 100644 --- a/candidates/decisions.jsonl +++ b/candidates/decisions.jsonl @@ -407,7 +407,7 @@ {"repo":"argumentcomputer/lurk","include":false,"category":"tool","confidence":"high","rationale":"Lean implementation of the Lurk language: parser, evaluator, CLI, scalar/Poseidon hashing — runtime/interpreter, no absorbable theorems."} {"repo":"argumentcomputer/yatimastdlib","include":false,"category":"tool","confidence":"medium","rationale":"Auxiliary stdlib for Yatima Inc tooling: hashmaps, byte arrays, FFI, string interner, polynomial benchmarks; utility infrastructure, not theorems."} {"repo":"axiommath/ramanujan-tau-misses-primes","include":true,"category":"mathlib","confidence":"high","rationale":"~5.8k LOC formalization accompanying paper on ABC implying Ramanujan tau misses primes; substantive number theory built on Mathlib."} -{"repo":"b-mehta/primecert","include":true,"category":"mathlib","confidence":"high","rationale":"~1.9k LOC of Pocklington/Wieferich primality certificates with formal proofs over Mathlib; reusable number-theoretic lemmas plus elaborator."} +{"repo":"b-mehta/primecert","include":false,"category":"mathlib","confidence":"high","rationale":"Substantive number-theory project, but upstream is actively maintained, so lean-pool should not vendor a duplicate copy."} {"repo":"beneficial-ai-foundation/floatspec","include":true,"category":"mathlib","confidence":"medium","rationale":"Lean 4 port of Coq Flocq: IEEE 754 floating-point spec with ~2200 defs/lemmas; 388 sorries but substantive completed proofs in Calc/Operations, Sqrt, Core."} {"repo":"cameronfreer/exchangeability","include":true,"category":"mathlib","confidence":"high","rationale":"de Finetti-Ryll-Nardzewski theorem formalization with 3 distinct proofs (martingale/L2/Koopman); 774 declarations, only 15 sorries; probability theory."} {"repo":"enricozb/logic","include":false,"category":"educational","confidence":"high","rationale":"Follow-along of textbook 'A Concise Introduction to Mathematical Logic'; status notes 'currently formalizing chapter 1 section 5'; learning project."} diff --git a/candidates/manual.txt b/candidates/manual.txt index ec1f6079fb..e8f0f2eace 100644 --- a/candidates/manual.txt +++ b/candidates/manual.txt @@ -117,7 +117,6 @@ https://github.com/AydenLamp/FinDFA https://github.com/ayhon/iris-loogle https://github.com/b-mehta/ExponentialRamsey https://github.com/b-mehta/HighlyAbundant -https://github.com/b-mehta/PrimeCert https://github.com/badly-drawn-wizards/impdf https://github.com/badly-drawn-wizards/noperthedron https://github.com/badly-drawn-wizards/sqlean @@ -454,7 +453,6 @@ https://github.com/katydid/symbolic-automatic-derivatives https://github.com/katzenpost/lean-ffi https://github.com/kbuzzard/IISc-experiments https://github.com/kbuzzard/MweSkeletons -https://github.com/kckennylau/PrimeCert https://github.com/kencyke/quantum-system https://github.com/kevinsullivan/cs2120f24 https://github.com/Kha/do-supplement diff --git a/python/lean_pool/pr_advisory.py b/python/lean_pool/pr_advisory.py index d0ba197c2b..ada47323c8 100644 --- a/python/lean_pool/pr_advisory.py +++ b/python/lean_pool/pr_advisory.py @@ -322,6 +322,13 @@ def update_pr_advisory( rows = advisory_rows_for_pr( repo_full_name, pr_number, metadata_cache=metadata_cache ) + if not rows: + if dry_run: + print( + "[dry-run] Would skip advisory comment on " + f"PR #{pr_number}: no project metadata changes" + ) + return "skipped" return post_sticky_comment( repo_full_name, pr_number, diff --git a/python/tests/test_pr_advisory.py b/python/tests/test_pr_advisory.py index fd460ad143..3014595a33 100644 --- a/python/tests/test_pr_advisory.py +++ b/python/tests/test_pr_advisory.py @@ -19,6 +19,7 @@ post_sticky_comment, project_changes, render_comment, + update_pr_advisory, ) @@ -193,3 +194,33 @@ def fake_run_gh(*args: str, stdin: str | None = None) -> str: assert action == "updated" assert calls[1][0][:3] == ("api", "-X", "PATCH") assert json.loads(calls[1][1] or "{}")["body"].endswith("new") + + +def test_update_pr_advisory_skips_pr_without_project_changes( + monkeypatch: pytest.MonkeyPatch, +) -> None: + """PRs without project metadata changes do not need a sticky comment.""" + posted = False + + def fake_rows( + repo_full_name: str, + pr_number: int, + *, + metadata_cache: dict[str, UpstreamMetadata] | None = None, + ) -> list[AdvisoryRow]: + assert repo_full_name == "acme/pool" + assert pr_number == 7 + return [] + + def fake_post(*args: object, **kwargs: object) -> str: + nonlocal posted + posted = True + return "created" + + monkeypatch.setattr(pr_advisory, "advisory_rows_for_pr", fake_rows) + monkeypatch.setattr(pr_advisory, "post_sticky_comment", fake_post) + + action = update_pr_advisory("acme/pool", 7) + + assert action == "skipped" + assert not posted