Skip to content

auto-task(Capacity): clear QuantumInfo/Capacity/Capacity.lean from the linter exemption list#1370

Merged
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
doxtor6:auto-lintqi-20260705-181624
Jul 6, 2026
Merged

auto-task(Capacity): clear QuantumInfo/Capacity/Capacity.lean from the linter exemption list#1370
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
doxtor6:auto-lintqi-20260705-181624

Conversation

@doxtor6

@doxtor6 doxtor6 commented Jul 5, 2026

Copy link
Copy Markdown
Collaborator

Summary

Removes QuantumInfo/Capacity/Capacity.lean from scripts/LinterExemption.txt, so the CI
linters (lake exe runPhyslibLinters and ./scripts/lint-style.sh) now enforce their rules on
it, and fixes the file so it passes them.

No open PR was handling this file (in particular #1244, which clears 56 other QuantumInfo
files, does not touch it).

Changes to QuantumInfo/Capacity/Capacity.lean

All changes are style/documentation only — no statement or proof was changed in meaning:

  • Reflowed all lines to the 100-character limit (doc-strings, theorem signatures, and a few
    proof-internal line breaks), using the standard 4-space continuation indent for split
    signatures.
  • Restructured the module docstring into the standard Physlib layout
    (i. Overview / ii. Key results / iii. Table of contents / iv. References), keeping
    the original physics content: the emulation-based definition of quantum capacity, the basic
    facts proved here, and the LSD (Lloyd–Shor–Devetak) theorem statements.
  • Filled in the table of contents and added matching lettered section headings
    (A. Basic definitions through E. The quantum capacity) so the file also passes the
    optional lake exe module_doc_lint.
  • Added the missing doc-string on quantumCapacity (the supremum of achievable transmission
    rates), required by the docBlame check in runPhyslibLinters.
  • Split an overlong variable line.

Verification

  • lake build succeeds (9119 jobs).
  • lake exe runPhyslibLinters reports no issues for this file (remaining local failures are
    all in files still on the exemption list).
  • ./scripts/lint-style.py QuantumInfo/Capacity/Capacity.lean exits clean, and
    ./scripts/lint-style.sh reports no new issues.
  • Optional linters: module_doc_lint and spelling also pass for this file.

🤖 Generated with Claude Code

…e linter exemption list

Co-authored-by: Claude <noreply@anthropic.com>
@github-actions

github-actions Bot commented Jul 5, 2026

Copy link
Copy Markdown
Contributor

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

Removed the definition of 'HasTimeDimension' from the API.

@jstoobysmith jstoobysmith left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved - will merge once passes linters (removed an entry from the API-map).

@jstoobysmith jstoobysmith added the ready-to-merge This PR is approved and will be merged shortly label Jul 6, 2026
@jstoobysmith jstoobysmith merged commit 2096ebd into leanprover-community:master Jul 6, 2026
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR is approved and will be merged shortly

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants