Skip to content

NOTICE.extra.yml: attribution for the Erdős–Sós (#548) import - #453

Merged
Vilin97 merged 1 commit into
mainfrom
claude/erdos548-notice-attribution
Sep 18, 2026
Merged

Vilin97 merged 1 commit into
mainfrom
claude/erdos548-notice-attribution

Conversation

@Vilin97

@Vilin97 Vilin97 commented Sep 18, 2026

Copy link
Copy Markdown
Collaborator

Non-content follow-up to #452 (Erdős–Sós conjecture import).

The upstream repository tadamcz/erdos548 ships a NOTICE file, so Apache License 2.0 §4(d) asks that its attribution notice travel with the redistributed sources. This adds the notice verbatim under Erdos548: in NOTICE.extra.yml (same shape as the Köthe entry added in #409) and regenerates NOTICE with python -m lean_pool.notice --repo ... No Lean content is touched.

🤖 Generated with Claude Code

Reproduces the upstream NOTICE of tadamcz/erdos548 (Apache License,
Version 2.0, Section 4(d)) under LeanPool/Erdos548 and regenerates NOTICE,
following the Köthe precedent in #409.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
@greptile-apps

greptile-apps Bot commented Sep 18, 2026

Copy link
Copy Markdown

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

Retrigger

No changed-code defect was identified, although exact fidelity to the externally hosted upstream NOTICE could not be independently verified from repository-local evidence.

Summary

This PR adds the upstream Erdős–Sós attribution to the notice source and updates the generated aggregate notice.

  • Registers the attribution under the correct Erdos548 project key.
  • Preserves the attribution text consistently between NOTICE.extra.yml and NOTICE.
  • Makes no Lean source or executable-code changes.

Reviews (1) · Last reviewed commit: "NOTICE.extra.yml: attribution for the Er..."

@Vilin97
Vilin97 merged commit 2c247e5 into main Sep 18, 2026
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant