Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
An Import Graph for Mathlib
An Import Graph for Mathlib
Lean modules declare their dependencies with lines at the top of each file. Scanning those across a whole project yields a dependency graph. This tutorial builds the import graph of , aggregated by top-level namespace, straight from the source tree - no build required, since it only reads headers. It complements LeanLink's declaration-level .
import
.lean
Prerequisites
Prerequisites
You need a Mathlib source checkout (the files; the project need not be compiled for import scanning):
.lean
In[1]:=
mathlibDir=FileNameJoin[{$HomeDirectory,"src","mathlib4"}];mathlibSrc=FileNameJoin[{mathlibDir,"Mathlib"}];mathlibReady=DirectoryQ[mathlibSrc]
Out[1]=
True
Scanning the Source Tree
Scanning the Source Tree
Every file under :
.lean
Mathlib/
In[2]:=
leanFiles=If[mathlibReady,FileNames["*.lean",mathlibSrc,Infinity],{}];Length[leanFiles]
Out[2]=
8624
A module's top-level namespace is the component just after (so is in ). These helpers map a module name, and a file path, to that namespace:
Mathlib
Mathlib.Algebra.Group.Basic
Algebra
In[3]:=
namespaceOf[mod_String]:=With[{p=StringSplit[mod,"."]},If[Length[p]≥2&&p〚1〛"Mathlib",p〚2〛,Missing[]]];fileNamespace[file_String]:=namespaceOf@StringRiffle[FileNameSplit[StringReplace[FileNameDrop[file,FileNameDepth[mathlibDir]],".lean"""]],"."];
Imports live at the top of a file, so reading only the first 60 lines keeps the scan fast (a couple of seconds for all of Mathlib's eight thousand files). We keep just the imports and map each to its namespace:
Mathlib.*
In[4]:=
readImportNamespaces[file_String]:=Module[{stream=OpenRead[file],lines},lines=ReadList[stream,"String",60];Close[stream];DeleteMissing[namespaceOf/@(StringTrim[StringReplace[#,"import """]]&/@Select[lines,StringStartsQ[#,"import "]&])]];
Building the Namespace Graph
Building the Namespace Graph
Each file contributes edges from its own namespace to the namespaces it imports; we drop self-loops and duplicates:
In[5]:=
nsEdges=If[mathlibReady,DeleteDuplicates@DeleteCases[Flatten@Map[file(DirectedEdge[fileNamespace[file],#]&/@readImportNamespaces[file]),leanFiles],DirectedEdge[x_,x_]],{}];Length[nsEdges]
Out[5]=
233
Count the files in each namespace - this both sizes the nodes and orders the legend:
In[6]:=
nsCounts=If[mathlibReady,Reverse@Sort@Counts[fileNamespace/@leanFiles],];Take[Normal[nsCounts],UpTo[5]]
Out[6]=
{Algebra1380,CategoryTheory1131,Analysis812,RingTheory729,Topology703}
Color each namespace from the standard scheme, size each node by its file count, and lay the graph out. No background is pinned, so it reads on both light and dark themes:
In[7]:=
importGraph=If[mathlibReady,Module[{namespaces=Keys[nsCounts],maxCount=Max[nsCounts],colorOf},colorOf=AssociationThread[namespaces(ColorData[97]/@Range[Length[namespaces]])];Graph[namespaces,nsEdges,VertexStyleNormal[colorOf],VertexSizeAssociationMap[0.3+0.7Sqrt[nsCounts[#]/maxCount]&,namespaces],VertexLabelsPlaced["Name",Tooltip],EdgeStyleDirective[Opacity[0.2],GrayLevel[0.5],Arrowheads[0.012]],GraphLayout"SpringElectricalEmbedding",ImageSize540]],"Mathlib source not found"]
Out[7]=
Statistics
Statistics
The full ranking of namespaces by file count:
In[8]:=
If[mathlibReady,Dataset@KeyValueMap["Namespace"#1,"Files"#2&,nsCounts],"Mathlib source not found"]
Out[8]=
| |||||||||||||||||||||||||||||||||||||||||||||
Declaration-Level Dependencies
Declaration-Level Dependencies
This graph is file-level: which modules import which. For a finer view - which declarations a single constant depends on - LeanLink offers and the property of a , which trace the proof-term dependencies of one theorem rather than the import structure of whole files.
"CallGraph"
 |
|
 |
|
""