# Pinned to the revision Mathlib v4.35.0 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 a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93
%global shortcommit %(c=%{commit}; echo ${c:0:7})
%global snapdate 20261012
%global lean_version 4.35.0
%global lakename importGraph

Name:           lean4-importgraph
Version:        0^20261012gita41f0e9
Release:        2%{?dist}
Summary:        Import graph tools for Lean 4 projects

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

BuildArch:      noarch
BuildRequires:  lean4 = %{lean_version}
BuildRequires:  lean4-rpm-macros
BuildRequires:  git-core
BuildRequires:  lean4-package(Cli) = c24fe6078c630e89b489bffe59b3e20ac30d12c8
Requires:       lean4 = %{lean_version}
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
ImportGraph computes and renders the import graph of a Lean 4 project
and finds unused transitive imports. Mathlib's `lake exe graph` and its
linters are built on it.

%prep
%autosetup -n import-graph-%{commit}
%lean4_git_init %{SOURCE1} %{url}
%lean4_dep Cli

%build
%lean4_build ImportGraph

%check
# the installed oleans load and elaborate against this toolchain
cat > %{_builddir}/check-%{lakename}.lean <<'EOF'
import ImportGraph
example : True := trivial
EOF
lake env lean %{_builddir}/check-%{lakename}.lean

%install
%lean4_install %{lakename}

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

%changelog
* Fri Nov 06 2026 Morgan Hough <morgan.hough@gmail.com> - 0^20261012gita41f0e9-2
- Rebuild in mhough/scientific: math and computational-physics packages move out
  of mhough/neurofedora

* Mon Nov 02 2026 Morgan Hough <morgan.hough@gmail.com> - 0^20261012gita41f0e9-1
- Initial package: the revision Mathlib v4.35.0 pins