Skip to content

Publish a downloadable build cache (Physlib + PhyslibAlpha) - #9

Closed
Alex-Zughaid wants to merge 20 commits into
masterfrom
feat/publish-build-cache-clean
Closed

Alex-Zughaid wants to merge 20 commits into
masterfrom
feat/publish-build-cache-clean

Conversation

@Alex-Zughaid

Copy link
Copy Markdown
Owner

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 get already solves for Mathlib, but nothing did for
Physlib's own code.

  • CI publishes build artifacts on every push to master, via Lake's own
    built-in content-addressed cache (lake cache), backed by a Cloudflare R2
    bucket (physlib-cache, lake-cache.toml).
  • scripts/get-cache.sh is a one-command wrapper: it fetches Mathlib's cache
    (via Mathlib's own tool) and Physlib's (via lake cache get against the R2
    bucket), so a contributor runs one command instead of two before their
    first lake build.
  • lakefile.toml gains enableArtifactCache / restoreAllArtifacts, which
    is 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 Cloudflare
account. 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

  • Local: full round-trip (build, restore, verify lake build is a
    no-op) proven via Lake's own cache mechanics
  • CI: stage -> put-staged against the live R2 bucket, verified publicly
    fetchable (correct LTAR content, HTTP 200) from outside CI
  • Fresh-clone timing: cold clone -> get-cache.sh -> lake build, 0 modules
    compiled, ~4-5 minutes total
  • Cross-platform: CI (Linux) -> local (macOS) cache consumption verified
  • Bucket ownership decision (see draft note above)
  • Maintainer review of the CI workflow changes

Generated with Claude Code

FergusMunro and others added 16 commits August 21, 2026 05:14
…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>
* 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
@github-actions

Copy link
Copy Markdown

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.

  1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

  2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

  3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

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.

@Alex-Zughaid
Alex-Zughaid force-pushed the feat/publish-build-cache-clean branch from 83e1700 to ced7af5 Compare August 27, 2026 11:42
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.
@Alex-Zughaid
Alex-Zughaid force-pushed the feat/publish-build-cache-clean branch from ced7af5 to 7f57624 Compare August 27, 2026 11:55
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.
@Alex-Zughaid
Alex-Zughaid force-pushed the feat/publish-build-cache-clean branch from 7f57624 to 9067d49 Compare August 27, 2026 13:18
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.

9 participants