Publish a downloadable build cache (Physlib + PhyslibAlpha) - #9
Alex-Zughaid wants to merge 20 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
|
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. |
83e1700 to
ced7af5
Compare
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.
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. Both workflows now build with Lake's artifact cache enabled, emit input-to-output mappings, stage them, and upload 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 is gated on the LAKE_CACHE_KEY secret being present and never blocks the rest of the build if it fails -- a stale or unreachable cache is an inconvenience, not a correctness problem.
ced7af5 to
7f57624
Compare
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.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.
7f57624 to
9067d49
Compare
Summary
New contributors currently compile all of Physlib (554 files), QuantumInfo
(84), and PhyslibAlpha (47) from source on their first build - the same
problem
lake exe cache getalready solves for Mathlib, but nothing did forPhyslib's own code.
master, via Lake's ownbuilt-in content-addressed cache (
lake cache), backed by a Cloudflare R2bucket (
physlib-cache,lake-cache.toml).scripts/get-cache.shis a one-command wrapper: it fetches Mathlib's cache(via Mathlib's own tool) and Physlib's (via
lake cache getagainst the R2bucket), so a contributor runs one command instead of two before their
first
lake build.lakefile.tomlgainsenableArtifactCache/restoreAllArtifacts, whichis what makes both the CI publish and the local restore work, and also
means a contributor's own local build populates their own cache, so
switching branches locally reuses work instead of recompiling.
Measured end to end on a fresh clone: clone + fetch + build in ~4-5 minutes,
compiling zero modules, versus 35+ minutes for a from-source CI build (and
well over an hour locally). Details and the exact numbers are in
docs/cache-setup.md.Draft - one thing maintainers should weigh in on
The R2 bucket (
physlib-cache) is currently on my personal Cloudflareaccount. That's fine for developing and testing this, but if this gets
merged, the project would depend on infrastructure owned and billed to me
personally. Before this is mergeable I think that's worth a deliberate
decision - moving the bucket to a project-owned account, or another
arrangement - rather than something noticed after the fact. Flagging it here
rather than waiting for it to be spotted in review.
Everything else has been tested end-to-end against the live bucket,
including CI runs that published real artifacts and a fresh clone that
consumed them successfully on a different OS than CI builds on (Linux CI
artifacts, macOS consumer).
Why R2
For a build cache the cost that scales is egress (every contributor
download), not storage. R2 has zero egress fees at any volume; Mathlib's own
cache uses Azure, which does not. Current bucket usage is ~29MB (well under
the 10GB free tier) for the full Physlib + QuantumInfo + PhyslibAlpha
artifact set, deduplicated by content hash across every push so far.
Test plan
lake buildis ano-op) proven via Lake's own cache mechanics
fetchable (correct LTAR content, HTTP 200) from outside CI
compiled, ~4-5 minutes total
Generated with Claude Code