TEST: use cache in linter builds - #10
Closed
Alex-Zughaid wants to merge 21 commits into
Closed
Alex-Zughaid wants to merge 21 commits into
Alex-Zughaid wants to merge 21 commits into
Conversation
…unity#1552) * created alphaFileImports.lean * updated lakefile and agents.md to include alphaFileImports as build target * included alphaFileImports and noAlphaImports in lint_all.lean * changed alphaBuild workflow to use new lean script * modified lean checkers to allow for command line arguments * created Meta/test directory, populated with dummy project violating linter rules, and created testing lean script2 * added testImportScript to lakefile * added text for new checks in lint_all * temporarily removed Meta file * Removed newlines and accidental test case. * removed a few extra newlines --------- Co-authored-by: FergusMunro <fmunro07@gmail.com>
…eanprover-community#1560) * feat(Mathematics): gradient_add_const, gradient_const_mul, gradient_inner_self, gradient_coord Add `Physlib/Mathematics/Calculus/Gradient.lean` with the elementary gradient rules on a real Hilbert space: `gradient_add_const`, `gradient_const_mul`, `gradient_inner_self`, `gradient_const_mul_inner_self`, and `gradient_coord` for coordinate functionals on `EuclideanSpace ℝ ι`. These are the lemmas that the harmonic oscillator and damped harmonic oscillator currently prove privately and that the simple pendulum needs as well. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> * refactor(ClassicalMechanics): use shared gradient lemmas in HarmonicOscillator.Basic Replace the local `gradient_inner_self`, `gradient_const_mul_inner_self` and the private `gradient_add_const'` of the harmonic oscillator by the general lemmas of `Physlib.Mathematics.Calculus.Gradient`. No statement about the harmonic oscillator changes. Also remove `toDual_symm_innerSL`: it was a helper for the deleted gradient lemmas and has no remaining use anywhere in the repository. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> * refactor(ClassicalMechanics): use shared gradient_const_mul in DampedHarmonicOscillator.Basic Drop the private copy of `gradient_const_mul` in favour of the general lemma in `Physlib.Mathematics.Calculus.Gradient`. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> * docs(Mathematics): docstrings and scope notes for the shared gradient lemmas Add one-line docstrings to `gradient_add_const`, `gradient_const_mul`, `gradient_inner_self`, `gradient_const_mul_inner_self` and `gradient_coord`; explain in the module overview how this file relates to `Space.Derivatives.Grad` and why it is stated over `ℝ`; drop the redundant import of `Mathlib.Analysis.InnerProductSpace.PiL2`. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> * feat(Mathematics): gradient_comp_coord, the chain rule for a function of one coordinate Add `gradient_comp_coord : HasDerivAt f f' (x i) → gradient (fun y => f (y i)) x = f' • EuclideanSpace.single i 1`, the general form of the cosine-potential gradient that the simple pendulum needs. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
…unity#1567) Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…and equation of motion (leanprover-community#1564)
* feat(OperatorAlgebra): add Jordan structure on observables Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> * refactor(OperatorAlgebra): express Jordan product through realPart Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> * fix(Jordan): satisfy documentation and simp linters Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> * refactor(OperatorAlgebra): group Jordan observables Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> * refactor(Jordan): use OperatorAlgebra assumptions * fix(Jordan): address review comments - Drop @[simp] from coe_jordan so it doesn't force-unfold the Jordan product coercion everywhere; it's still available to invoke explicitly, which is all the existing proofs need. - Turn JordanObservable from an abbrev into a def so that the NonUnitalNonAssocCommRing instance built on it isn't picked up by typeclass search on Observable A itself (Observable has no canonical multiplication). Forward the AddCommGroup and Module ℝ instances explicitly since def blocks the automatic inheritance abbrev gave for free. --------- Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…ver-community#1556) * feat(OperatorAlgebra): characterize reversible Hilbert-space dynamics Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> * docs(OperatorAlgebra): note Hamiltonian quotient TODO Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> * revert(OperatorAlgebra): remove local Hamiltonian TODO Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> * feat(OperatorAlgebra): structure bounded operators Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com> * refactor(OperatorAlgebra): stack automorphism on Basic * refactor(OperatorAlgebra): separate Hilbert-space layer * refactor(OperatorAlgebra): bundle Hilbert-space assumptions * fix: sort Physlib imports * refactor(HilbertSpace): drop the bundling class per review Remove OperatorAlgebra.HilbertSpace and use the flat instance list [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] directly, per jstoobysmith's suggestion: bundling classes over already-existing instance conjunctions risks instance diamonds and hides Mathlib lemmas keyed on the flat instances, for no real benefit here. --------- Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
…ic integral of the first kind (leanprover-community#1573) * feat(Mathematics): Real.completeEllipticK, its integrability and positivity for m < 1 - Real.completeEllipticK m := ∫ φ in 0..π/2, (1 - m sin² φ)^(-1/2), the parameter convention (Abramowitz–Stegun 17.3.1), with an honest account of the junk values for m ≥ 1 - completeEllipticK_integrand_pos, continuous_completeEllipticK_integrand, completeEllipticK_intervalIntegrable (all under m < 1) - completeEllipticK_zero : K 0 = π/2 (simp); completeEllipticK_pos for m < 1 - registered in Physlib.lean Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com> * feat(Mathematics): completeEllipticK is monotone and continuous on (-∞, 1) - completeEllipticK_mono : m₁ ≤ m₂ < 1 → K m₁ ≤ K m₂, from the pointwise monotonicity of the integrand in the parameter (intervalIntegral.integral_mono_on, rpow_le_rpow_of_nonpos) - pi_div_two_le_completeEllipticK : 0 ≤ m < 1 → π/2 ≤ K m, from monotonicity and K 0 = π/2 - completeEllipticK_continuousOn : ContinuousOn completeEllipticK (Set.Iio 1), via intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' with the parameter restricted to the subtype Set.Iio 1 (continuousOn_iff_continuous_domRestrict) - completeEllipticK_continuousAt_zero : ContinuousAt completeEllipticK 0 - sections C–D, key results and table of contents updated; no new imports (DominatedConvergence is already public-imported through Integrals.Basic) Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com> * fix(Mathematics): review fixes for the complete elliptic integral module - correct the m ≥ 1 documentation: the Lean value for m > 1 is the finite positive integral over [0, arcsin (1/√m)], i.e. K(1/m)/√m (DLMF 19.7(ii)), not an unrelated number; K(1) = ∞ vs the totalized 0 - rename completeEllipticK_integrand_pos → completeEllipticK_radicand_pos (it bounds the radicand), and align the two integrand lemmas to the subject-first Mathlib scheme - drop the redundant Integrals.Basic import; import DominatedConvergence explicitly for the parametric-continuity lemma - document the rpow-vs-1/√ choice; golf the radicand positivity proof Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com> * fix(Mathematics): Mathlib-convention names and API additions for completeEllipticK - rename to head-symbol-first: continuous_completeEllipticK_integrand, intervalIntegrable_completeEllipticK_integrand, continuousOn_completeEllipticK, continuousAt_completeEllipticK_zero - drop the dead IntervalIntegral.Basic import (DominatedConvergence's closure has it) - @[pp_nodot] on the definition; @[gcongr] on completeEllipticK_mono - add completeEllipticK_eq, monotoneOn_completeEllipticK, completeEllipticK_strictMono, completeEllipticK_le (the upper bound (π/2)(1 - m)^(-1/2)), and the general continuousAt_completeEllipticK with the zero case derived from it - docs: DLMF §19.7(ii) and L&L §11 Problem 1 in the references; m = 1 sentence tightened Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com> * refactor(Mathematics): move the sine-square bounds to Trigonometry.SinSq and motivate completeEllipticK physically - Real.sin_sq_lt_one and Real.sin_half_sq_lt_one move from EllipticIntegral.lean to the new Physlib/Mathematics/Trigonometry/SinSq.lean, registered in Physlib.lean, per review: they are elementary facts about the sine unrelated to the elliptic integral, and nothing in EllipticIntegral.lean uses them, so the new file is not imported there - the §i Overview of EllipticIntegral.lean gains a paragraph on where K enters physics and why Physlib defines it, per review: the exact pendulum period 4 √(ℓ/g) K(sin² (θ₀/2)) (Landau & Lifshitz §11, Problem 1), its consumer SimplePendulum.PeriodFormula, and the loop field, ring potential and ellipse arc length where the complete integrals of the first and second kind appear more broadly Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
…d shift invariance (leanprover-community#1569) * feat(ClassicalMechanics): SimplePendulum variational equivalence and energy conservation - equationOfMotion_iff_gradLagrangian_zero: for smooth lifts the equation of motion holds iff the variational derivative of the action vanishes - isSolution_iff: solutions are exactly the smooth critical points of the action - energy_conservation_of_equationOfMotion: the time derivative of the energy vanishes along smooth lifts satisfying the equation of motion - energy_conservation_of_equationOfMotion': the energy at any time equals its initial value - IsSolution.energy_eq: energy conservation packaged for solutions Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com> * feat(ClassicalMechanics): SimplePendulum equilibria, separatrix energy and energy bounds - equationOfMotion_const_zero, isSolution_const_zero: the hanging equilibrium, the first explicit solution of the pendulum - equationOfMotion_const_pi, isSolution_const_pi: the inverted equilibrium - equationOfMotion_const_iff: a constant lift solves the equation of motion iff the sine of its angle vanishes — the constant solutions are the equilibria - separatrixEnergy, separatrixEnergy_pos: the energy 2 m g ℓ of the inverted equilibrium, the threshold between libration and rotation - energy_const_pi: the energy of the inverted equilibrium is the separatrix energy - kineticEnergy_nonneg, inertia_mul_inner_deriv_le, potentialEnergy_le_energy: the elementary energy bounds along every lift of the angle - neg_one_lt_cos_of_energy_lt: libration — below the separatrix energy the bob never reaches the top of the swing - deriv_ne_zero_of_energy_gt: rotation — above the separatrix energy the angular velocity never vanishes - potentialEnergy_eq_energy_of_deriv_eq_zero: turning points — where the velocity vanishes the potential energy equals the total energy Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com> * feat(ClassicalMechanics): SimplePendulum dynamics 2πn-shift invariance Section K (Independence of the lift): the lifted dynamics of the simple pendulum is invariant under shifting the lift by a whole number of turns, so it descends to the configuration space. New declarations: - SimplePendulum.potentialEnergy_add_two_pi - SimplePendulum.torque_add_two_pi - SimplePendulum.energy_add_const - SimplePendulum.equationOfMotion_add_two_pi - SimplePendulum.isSolution_add_two_pi - SimplePendulum.ofAngle_add_two_pi_coord Module doc: the Overview now points at section K for the 2πn statement, and the Key results name the equilibria as solutions (isSolution_const_zero, isSolution_const_pi) and list the section K results. Imports gain the geometric configuration space module for ConfigurationSpace.ofAngle. API map: two new rows (equilibria as solutions with the libration/rotation threshold; invariance of the lifted dynamics under whole-turn shifts) and the Overview extended to match. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com> * fix(ClassicalMechanics): review fixes for the simple pendulum conservation module Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com> * refactor(ClassicalMechanics): split the simple pendulum module into Basic, Equilibria and LiftInvariance - `SimplePendulum/Basic.lean` keeps the model and its dynamics (sections A–H): the input data, energies, Lagrangian, torque, equation of motion, variational principle and energy conservation. - New `SimplePendulum/Equilibria.lean` (old sections I–J): the hanging and inverted equilibria, the constant solutions as the equilibria, the separatrix energy, the energy bounds, libration/rotation and turning points. - New `SimplePendulum/LiftInvariance.lean` (old section K): invariance of the energies, the torque, the equation of motion and its solutions under `θ ↦ θ + 2πn`, and the shifted lift describing the same configuration. Takes over the `Geometric.Basic` import, which nothing in `Basic.lean` used. - Declarations and proofs are moved verbatim; only section labels, cross-references and the module docs change. `Physlib.lean` and the API map updated. Requested by review on leanprover-community#1569. Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com> --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Codex GPT-5.6 <noreply@openai.com>
… docstring (leanprover-community#1581) The module docstring described `ε4` as living in `d = 3`; the file's results (e.g. the full contraction equalling 24 = 4!) are in `d = 4`. Closes leanprover-community#1533
…ommunity#1579) * feat(Units): reducible rational arithmetic via Exponent * feat(Units): use Exponent for dimension coordinates * feat(Units): native exponent-tuple representation of dimensions via DimensionBasis * feat(Units): add Exponent coercion API and Exponent-valued dimension powers
…er-community#1565) * feat(tensors): prove the Levi-Civita contraction identities * refactor(tensors): relocate reindexing lemmas * refactor(tensors): organize Levi-Civita contraction APIs Move reusable contraction, metric, unit, Minkowski, and Kronecker component lemmas into their owning modules. Keep the finite-index proof scaffolding private and the headline identities in LeviCivita/Contractions. * refactor(tensors): streamline Levi-Civita contractions * refactor(tensors): simplify contraction component routing
…lum and the equivalence of formulations (leanprover-community#1570)
…community#1568) * feat(pauli): prove epsilon triple-product identities * refactor(pauli): express triple products via index dualization * refactor(pauli): address tensor API review * style(pauli): compact triple-product statements
* Enable Lake's built-in artifact cache enableArtifactCache makes a build populate Lake's own content-addressed cache; restoreAllArtifacts materialises cached artifacts back into .lake/build. Both are needed for the CI publish/consume flow in the next commit, and they help locally too: switching branches reuses cached work instead of recompiling. * CI: publish Physlib's build cache to R2 on every push to master New contributors currently compile all of Physlib, QuantumInfo, and PhyslibAlpha from source on first build. lake exe cache get already solves this for Mathlib; nothing did for Physlib's own code. A new, standalone workflow (publish-cache.yml), triggered only by push to master -- never by pull_request. build.yml and alphaBuild.yml are not touched at all: diffed against upstream/master, this branch makes zero changes to either file. That independence has a real cost: this workflow cannot reuse build.yml/alphaBuild.yml's build output (GitHub Actions jobs in different workflow runs do not share a filesystem), so its two jobs rebuild Physlib+QuantumInfo and PhyslibAlpha from scratch, on top of the builds those other workflows already do for linting. Each job is gated on LAKE_CACHE_KEY existing and skipped outright otherwise, so nothing is wasted rebuilding before the bucket exists. Each job builds with Lake's artifact cache enabled, emits input-to-output mappings, stages them, and uploads with `lake cache put-staged` to a Cloudflare R2 bucket (lake-cache.toml). R2 rather than S3 or Azure because the cost that scales here is egress -- every contributor download -- and R2 charges nothing for it at any volume. lake-cache.toml is committed rather than generated in the workflow, since its endpoints are public information and committing it means local contributors get the cache with no manual configuration. It declares separate read (physlib-r2) and write (physlib-r2-upload) services, so a contributor cannot write to the cache even by accident. Publishing never blocks a merge if it fails -- both jobs' cache steps are continue-on-error, with an explicit warning annotation on failure rather than a silent no-op. * Add scripts/get_cache.lean: fetch the build cache in one command Downloads Mathlib's prebuilt files (via Mathlib's own lake exe cache get) and Physlib's own (via lake cache get against the R2 bucket), so a contributor runs one command instead of two before their first lake build. A Lean lean_exe rather than a shell script, matching every other tool in scripts/ (check_file_imports, sorry_lint, style_lint, etc) -- bash was the odd one out. Only imports Lean core, not Mathlib, so building it does not need Mathlib already built. Safe to run at any time and safe to skip: any failure warns and exits 0, falling back to a normal build from source. Unrecognised flags are rejected up front rather than silently ignored, so a typo'd flag does not fall through into running the full fetch unexpectedly. * docs: cache setup guide and updated install instructions docs/cache-setup.md covers provisioning the R2 bucket end to end, for whoever administers it next. README's install steps now mention lake exe get_cache, with measured timings from a fresh clone: clone + fetch + build in ~4-5 minutes, compiling zero modules, versus 35+ minutes for a from-source CI build. * CI: restore each job's own R2 cache before building Without this, publish-cache.yml rebuilds Physlib and PhyslibAlpha from scratch on every merge, even though the previous merge's artifacts are already sitting in the bucket this job is about to publish to. Each job now runs `lake cache get --scope=physlib-master` against that same bucket before its build step -- the same mechanism scripts/get_cache.lean already uses for contributors, applied here to the job's own build. Whatever hasn't changed since the last successful publish gets restored instead of recompiled, so a typical incremental merge only compiles its actual diff rather than the whole library. No LAKE_CACHE_KEY needed for this step -- it only reads the bucket's public endpoint. A cold bucket (the very first run) falls through to a full build, same as before. * changed the readme and comments * make the secrets accesible for the workflow * Update cache-setup.md * Update lake-cache.toml * docs changes and also fix to look in /artifacts
Needs fetch-depth 0, lake looks back through commits to find one with a cache and a shallow clone only has one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Thank you for this pull-request (PR). If this is your first PR, welcome to the community! Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.
Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages. If you have any problems or questions, please reach out to the community on the Zulip. |
Owner
Author
|
Test complete - cache restore verified working. Closing. |
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
10 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.
Throwaway test PR on the fork to verify the cache restore works in the linter workflows. Not for merging.