Topological sort of Mathlib modules/files

Stream: general

[Yakov Pechersky]

I'm thinking about how to go about a refactor of a definition. I am planning to grep for occurrences of the definition, and work backwards from the leaves. To do this, I'd love to have a topological sort of the modules I care about.

Is there some way to plug into "longest pole" or any other introspecting program to achieve this?

I'm imagining either generating the full topo-sort of all Mathlib modules, and then I rg -f using my subset, or having the application take my subset of interest and calculating the topo-sort of those.

[Johan Commelin]

#!/usr/bin/env python3

import sys
import subprocess

def read_input_files():
    return [line.strip() for line in sys.stdin]

def extract_imports(file):
    imports = []
    with open(file, 'r') as f:
        for line in f:
            if line.startswith('import Mathlib.'):
                import_path = line.strip().replace('import ', '').replace('.', '/') + '.lean'
                imports.append(import_path)
    return imports

def get_all_files():
    result = subprocess.run(
        ['git', 'ls-files'],
        capture_output=True,
        text=True,
        check=True
    )
    return [line for line in result.stdout.splitlines() if line.startswith('Mathlib/') and line.endswith('.lean')]

def build_dependency_graph(all_files):
    dep_graph = []
    for file in all_files:
        imports = extract_imports(file)
        for imp in imports:
            dep_graph.append(f"{file} {imp}")
    return dep_graph

def tsort(dep_graph):
    result = subprocess.run(
        ['tsort'],
        input='\n'.join(dep_graph),
        capture_output=True,
        text=True,
        check=False
    )
    return result.stdout.splitlines()

def main():
    input_files = read_input_files()
    all_files = get_all_files()
    dep_graph = build_dependency_graph(all_files)
    sorted_files = tsort(dep_graph)

    if not input_files:
        print('\n'.join(sorted_files))
    else:
        input_files_set = set(input_files)
        filtered_sorted_files = [file for file in sorted_files if file in input_files_set]
        print('\n'.join(filtered_sorted_files))

if __name__ == "__main__":
    main()

[Damiano Testa]

If you have the oleans, I also wrote something like this in lean. Probably, searching for sort_imports may return something useful (I'm on mobile).

[Eric Wieser]

import-graph can surely handle this too?

[Yakov Pechersky]

Thanks! Johan's script kind of(?) worked:

$ git grep -w Valued | rg -v import | cut -d: -f1 | rg ".lean" | sort -u | python tsort.py
Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
Mathlib/Topology/Algebra/Valued/WithVal.lean
Mathlib/Topology/Algebra/Valued/ValuedField.lean
Mathlib/Topology/Algebra/Valued/NormedValued.lean
Mathlib/Topology/UniformSpace/Ultra/Basic.lean <-- Valued only appears in a comment here
Mathlib/Topology/Algebra/Valued/ValuationTopology.lean <-- I would imagine this should have been a "root"
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
Mathlib/NumberTheory/FunctionField.lean
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
Mathlib/Combinatorics/Optimization/ValuedCSP.lean
Mathlib/RingTheory/LaurentSeries.lean
Mathlib/NumberTheory/NumberField/FinitePlaces.lean

[Eric Wieser]

https://stackoverflow.com/a/72753207 implies a very silly hack for supporting this order in vscode search:

• Run a stupid bash script that sorts the files, then sets the modified time to 1970 + n seconds
• Use vscode search

[Damiano Testa]

This is what I had in mind, I think:

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Sort.20lines.20by.20import.20order.20of.20files/near/478346802

[Yakov Pechersky]

Awesome, thank you!

Mathlib.Topology.Algebra.Valued.ValuationTopology
Mathlib.Topology.Algebra.Valued.NormedValued
Mathlib.Topology.Algebra.Valued.ValuedField
Mathlib.Topology.Algebra.Valued.WithVal
Mathlib.RingTheory.DedekindDomain.AdicValuation
Mathlib.FieldTheory.RatFunc.AsPolynomial
Mathlib.NumberTheory.NumberField.FinitePlaces
Mathlib.RingTheory.LaurentSeries
Mathlib.Topology.UniformSpace.Ultra.Basic
Mathlib.NumberTheory.FunctionField
Mathlib.Topology.Algebra.Valued.LocallyCompact
Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

[Yakov Pechersky]

hmm I'm still surprised to see Ultra.Basic so far down the list