# Pinned to the revision the v4.35.0 tag locks in its lake-manifest.json; a dependent's
# `lake build` accepts an installed package only at that exact commit, so this
# moves together with lean4-mathlib and lean4.
%global commit af04d60bcd7618af849ff511e0a19d77f709937e
%global shortcommit %(c=%{commit}; echo ${c:0:7})
%global snapdate 20261015
%global lean_version 4.35.0
%global lakename physlib

Name:           lean4-physlib
Version:        4.35.0
Release:        3%{?dist}
Summary:        Physlib: results from physics digitalised in Lean 4

License:        Apache-2.0
URL:            https://github.com/leanprover-community/physlib
Source0:        %{url}/archive/%{commit}/physlib-%{commit}.tar.gz
# `git cat-file commit %%{commit}`: %%lean4_git_init rebuilds the checkout
# Lake expects from the tarball (see macros.lean4).
Source1:        physlib-%{commit}.commit

BuildArch:      noarch
BuildRequires:  lean4 = %{lean_version}
BuildRequires:  lean4-rpm-macros
BuildRequires:  git-core
BuildRequires:  lean4-package(mathlib) = 56a005855ea17e0b0958f73ec801ae140b0a1679
BuildRequires:  lean4-package(batteries) = 66e469188fe07963e5cf666c7d4433f45b8131c5
BuildRequires:  lean4-package(Qq) = dce0ad79c486cb1fb504af04f953c3466b0c6db8
BuildRequires:  lean4-package(aesop) = 4a174c490d8707121c4a9290800489f105d85e07
BuildRequires:  lean4-package(proofwidgets) = df72b022e558978a1c50264cfc4d7fec86fa8e04
BuildRequires:  lean4-package(importGraph) = a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93
BuildRequires:  lean4-package(LeanSearchClient) = d6b4c7be5be75ec4917c873ac50c756dc1436372
BuildRequires:  lean4-package(plausible) = dfa4f38190d07c37e315953e08b90fe2d95b3c24
BuildRequires:  lean4-package(Cli) = c24fe6078c630e89b489bffe59b3e20ac30d12c8
Requires:       lean4 = %{lean_version}
Requires:       lean4-package(mathlib) = 56a005855ea17e0b0958f73ec801ae140b0a1679
Requires:       lean4-package(batteries) = 66e469188fe07963e5cf666c7d4433f45b8131c5
Requires:       lean4-package(Qq) = dce0ad79c486cb1fb504af04f953c3466b0c6db8
Requires:       lean4-package(aesop) = 4a174c490d8707121c4a9290800489f105d85e07
Requires:       lean4-package(proofwidgets) = df72b022e558978a1c50264cfc4d7fec86fa8e04
Requires:       lean4-package(importGraph) = a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93
Requires:       lean4-package(LeanSearchClient) = d6b4c7be5be75ec4917c873ac50c756dc1436372
Requires:       lean4-package(plausible) = dfa4f38190d07c37e315953e08b90fe2d95b3c24
Requires:       lean4-package(Cli) = c24fe6078c630e89b489bffe59b3e20ac30d12c8
# what a dependent's spec pins: the Lake package name at its exact revision
Provides:       lean4-package(%{lakename}) = %{commit}

%description
Physlib (formerly HepLean and PhysLean) digitalises results from physics
into Lean 4 on top of Mathlib: Physlib (reviewed and curated) and
QuantumInfo (quantum information theory), upstream's default build targets.
Every result is a formally verified definition or theorem; the library is
noncomputable throughout. PhyslibAlpha (rapid development with lighter
review) ships as source only: its cubic point-group module proves the
group order by kernel evaluation and does not finish on a Copr builder.

%prep
%autosetup -n physlib-%{commit}
%lean4_git_init %{SOURCE1} %{url}
# Lake honours a package's own enableArtifactCache over every environment and
# workspace setting. With it on, replaying an up-to-date module chmods the
# package's .olean and hard-links it into ~/.cache/lake, which only the owner
# of /usr/share/lean4/packages/physlib may do: a user's `lake build` against
# the installed package stopped with "failed to cache artifact: operation not
# permitted". Off, Lake only reads the installed build tree.
sed -i 's/^enableArtifactCache = true$/enableArtifactCache = false/' lakefile.toml
%lean4_dep mathlib
%lean4_dep batteries
%lean4_dep Qq
%lean4_dep aesop
%lean4_dep proofwidgets
%lean4_dep importGraph
%lean4_dep LeanSearchClient
%lean4_dep plausible
%lean4_dep Cli

%build
%lean4_build Physlib QuantumInfo

%check
# the installed oleans load and elaborate against this toolchain
cat > %{_builddir}/check-%{lakename}.lean <<'EOF'
import Physlib
import QuantumInfo
example (a b : ℝ) : a + b = b + a := by ring
EOF
lake env lean %{_builddir}/check-%{lakename}.lean

%install
%lean4_install %{lakename}

%files
%license LICENSE
%doc README.md
%{_lean4_pkgdir}/%{lakename}/

%changelog
* Wed Nov 04 2026 Morgan Hough <morgan.hough@gmail.com> - 4.35.0-3
- Turn enableArtifactCache off in the shipped lakefile: Lake chmods and
  hard-links the installed oleans on replay, which fails for every user but
  root (`lake build` against the package: "failed to cache artifact")

* Wed Nov 04 2026 Morgan Hough <morgan.hough@gmail.com> - 4.35.0-2
- Build upstream's default targets, Physlib and QuantumInfo; PhyslibAlpha's
  PointGroup.Cubic (decide +kernel) ran for hours on every Copr builder

* Mon Nov 02 2026 Morgan Hough <morgan.hough@gmail.com> - 4.35.0-1
- Initial package: the revision the v4.35.0 tag pins