TEST - DO NOT MERGE#3
Closed
Alex-Zughaid wants to merge 2 commits into
Closed
Conversation
* chore: Bump v4.32.0 Bump lean-toolchain, mathlib, and doc-gen4 to v4.32.0 (tracker leanprover-community#1437) and repair the source breakages from the Mathlib 4.31->4.32 API drift across Physlib, QuantumInfo, and PhyslibAlpha. Proofs, instances, and imports only; no lemma/definition statement or mathematical content was changed. Breakage classes fixed: - Hand-rolled AddMonoid/AddCommMonoid/AddCommGroup instances whose nsmul/zsmul field proofs relied on `ring` closing scalar-multiplication (smul) goals, which it no longer does in 4.32. - Structure refactors: MonoidAlgebra and MvPolynomial are now wrapper structs (no longer defeq to their coefficient Finsupp); ContRepresentation gained a toMonoidHom field; Mathlib.Meta.Positivity.Strictness gained an Option PartialOrder index (13 positivity extensions); LeftOrdContinuous gained an s.Nonempty hypothesis. - Tactic drift in fun_prop / measurability (metavariable goals), simp / simpa / convert normal forms. - Deprecation renames: PiTensorProduct import, IsOpen.locallyPathConnectedSpace, Finset.le_eq_subset, TwoSidedIdeal.mem_ofRingCon, and the removed simpVarHead linter; def -> lemma for the propositions flagged by the defProp linter. `lake build` (Physlib + QuantumInfo + PhyslibAlpha) is green; `lake exe lint_all` and the version-bump scripts (TODO_to_yml, stats, informal, make_tag) pass. Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> * chore: address review feedback on the v4.32.0 bump Apply @nateabr's review suggestions, which simplify the migration in three places and, for the spectral measure, identify a cleaner root-cause fix: - SpaceAndTime/Space/Module.lean: define `zsmul` via `•` (`z • p.val i`), so the default `zsmul_zero'`/`zsmul_succ'`/`zsmul_neg'` proofs discharge and those blocks are dropped. - StringTheory/FTheory/SU5/Fluxes/Basic.lean: define `nsmul` via `•` and close `nsmul_zero`/`nsmul_succ` with `zero_nsmul`/`succ_nsmul`. - QuantumMechanics/Operators/SpectralTheory/SpectralMeasure.lean: the 4.32 breakage was the `CoeFun` coercion, not the composition lemmas; use `⇑μS.toVectorMeasure` and revert `comp_of_disjoint`, `comp_eq_of_inter`, and `commute` to their original form. Thanks to @nateabr for the careful and constructive review. Co-authored-by: nateabr <135662056+nateabr@users.noreply.github.com> Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> * fix(QuantumMechanics): drop unused instance arguments in StinespringDilation The `unusedArguments` alpha-linter (`runPhyslibAlphaLinters`) fails under the v4.32.0 toolchain on `StinespringDilation`. The file is unchanged since the v4.31.0 bump and the same linter is green on master, so the reports are a consequence of the 4.31 -> 4.32 Mathlib bump: the matrix operations these lemmas call (`tr₂`, `stinespringOp`, `Matrix.one`) no longer thread the flagged instances through their elaborated proof terms, so the arguments are now genuinely dead. Verified against each definition's signature: - `tr₂_e₀Xe₀`: `[Zero w]` — `tr₂` needs only `[Fintype n]` on the traced index. - `tracefree_version`: `[Zero r]`, `[DecidableEq m]` — `(1 : Matrix r r R)` needs `[DecidableEq r]` (index) and `Zero/One R` (from `RCLike R`), not `Zero r`; `stinespringForm` needs `[Fintype r] [DecidableEq r] [Fintype m]`, not `[DecidableEq m]`. - `stinespringOp_apply`: `[Fintype m]`, `[DecidableEq m]` — `stinespringOp` needs only `[Fintype r] [DecidableEq r]`. - `heisenberg_schrõdinger`: `[Zero r]`, `[DecidableEq m]` — same two; these were live only because its proof (`rw [tracefree_version]`) threaded them into `tracefree_version`. CI reported only the first three; removing them from `tracefree_version` exposes this caller, which the local linter then flags. Removing instance-implicit arguments is safe for callers (they are inferred, never passed positionally). `runPhyslibAlphaLinters` is now clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * fix(lint): quiet 5 v4.32.0 #lint regressions on pre-existing declarations Toolchain collateral from the v4.32.0 bump — not a source change. ## Symptom The `runLinter on Physlib` CI step (`env LEAN_ABORT_ON_PANIC=1 lake exe runPhyslibLinters`, build.yml) fails on this PR with 5 errors, while the *identical* step is green on `master`. `master` still runs Lean/Mathlib v4.31.0; this PR is the v4.32.0 bump. The v4.32.0 `#lint` linters (`unusedArguments`, `checkType`) are stricter than v4.31.0's and now flag code that predates this PR. ## These are not our edits None of the 5 flagged declarations is changed by this bump: - Physlib/Relativity/Tensors/LeviCivita/Basic.lean (untouched file) - Physlib/Relativity/.../Vector/Causality/LightLike.lean (untouched file) - Physlib/SpaceAndTime/Space/Integrals/Basic.lean (untouched file) - Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean (untouched file) - Physlib/Particles/.../SU5/ChargeSpectrum/Basic.lean (this PR only edits `subset_trans` at L187; the flagged `min_exists_inductive` at L333 is unchanged) ## The 5 findings and the fix 1. checkType — `leviCivita_contract_self`: whnf on its tensor-notation statement now exceeds the linter's 200k-heartbeat budget (v4.31.0 stayed under it). Statement unchanged. → `@[nolint checkType]`. 2-5. unusedArguments — `min_exists_inductive` (`hn`), `lightlike_spatial_parallel_implies_proportional` (`hv`, `hw`), `integrable_spherical_of_integrable` (`NormedSpace ℝ F`), `probability_nonneg` (`IsFiniteMeasure`, `NeZero`): each argument is part of the intended interface / goal statement but unused by the proof term. → `@[nolint unusedArguments]` (matching 17 existing uses in the tree). Consistent with this PR's charter (a toolchain bump: no lemma/definition statement or signature is added, removed, or changed), these are *silenced*, not restructured. Dropping the now-"unused" binders would alter public signatures and risk downstream breakage; that is out of scope for a bump. ## Why local `lake exe lint_all` did not catch it `scripts/lint_all.lean`'s `main` ends in an unconditional `pure 0` — it prints linter output but never sets a non-zero exit code, so it cannot gate a PR. CI does not use it; it invokes `lake exe runPhyslibLinters` directly, which *does* exit 1 on findings. Reproduce the CI gate locally with: env LEAN_ABORT_ON_PANIC=1 lake exe runPhyslibLinters Physlib Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> Co-authored-by: nateabr <135662056+nateabr@users.noreply.github.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
made by claude - just to test the PR
|
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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
made by claude to test the PR tracking system