list of files that build

Stream: lean4

[Johan Commelin]

How can I ask lean (or lake) for a list of files that build without errors?
I'm refactoring mathlib, and would like to benchmark the part that builds against the corresponding part on master

[Kim Morrison]

@Mac Malone? As far as I'm aware this isn't currently possible.

[Mac Malone]

Unfortunately, this is not information available from the Lake CLI. :sad: Lake can get this information, so if you are comfortable wriritng a Lean program that uses the API you could get it. But that may be more hassle than it is worth.

[Alex J. Best]

Could you just do some shell scripting to run lake build on each file in turn and print the list of those with 0 exit code (maybe chatgpt could write this in an instant?)

[Julian Berman]

That will re-build every broken file with n dependents n times right?

[Mac Malone]

Also, you could potentially deduce which files failed from the output of lake build and then subtract those from a list of all files in mathlib to get the set of files which build.

[Johan Commelin]

Together with copilot I came up with the following script

import os
import sys
import subprocess
import networkx as nx
from collections import defaultdict
import time

# Traverse the repository to find all .lean files and parse their import statements
dependencies = defaultdict(list)
for root, dirs, files in os.walk('./Mathlib'):
    for file in files:
        if file.endswith('.lean'):
            filepath = os.path.join(root, file)
            index = filepath[2:].replace('/', '.').replace('.lean', '')
            with open(filepath, 'r') as f:
                for line in f:
                    if line.startswith('import '):
                        dependencies[index].append(line.split(' ')[1].strip())
                    elif line.startswith('/-!'):
                        break

# Create a graph from the dependencies
G = nx.DiGraph(dependencies)

# Perform a topological sort on the graph
try:
    sorted_files = [file for file in nx.topological_sort(G) if file.startswith('Mathlib')]
    # sorted_files.reverse()
except nx.NetworkXUnfeasible:
    print("Graph contains a cycle:", file=sys.stderr)
    cycle = nx.simple_cycles(G)
    print(next(cycle))
    exit()

# Attempt to build each file in the sorted order
successful_files = []
for file in sorted_files:
  # Skip building the file if any of its dependencies weren't successfully built
  if any(dependency not in successful_files for dependency in G.predecessors(file)):
    continue
  try:
    print("Attempting to build", file, file=sys.stderr)
    subprocess.check_call(['lake', 'build', file], stdout=sys.stderr, stderr=sys.stderr)
    successful_files.append(file)
    print(file)
  except subprocess.CalledProcessError:
    pass

[Johan Commelin]

It doesn't seem to work. It still starts building all of Mathlib, after iterating through the first ~10 items of sorted_files.

[Johan Commelin]

It's almost as if that topological sort didn't really work

[Damiano Testa]

Is the idea that you want to build Mathlib and then find this out, or you would like to do this with the data of the oleans?

[Damiano Testa]

You could see what lake exe cache get downloads and the missing oleans (or the leaves that you download that are not actual leaves) would be the broken files, right?

[Johan Commelin]

@Damiano Testa I don't really care about the method. I have a copy of mathlib in which ~500 files build without error. I would like to get the explicit list of those filenames.

[Johan Commelin]

If this can be done in < 1 minute, that would be really cool.

[Mario Carneiro]

if you are willing to rebuild from scratch you can just clear the build files and then see what files exist when lake is done

[Johan Commelin]

But I can of course resort to "throw away all .oleans, attempt a build, check which oleans have been succesfully written"

[Johan Commelin]

Yes, I'm starting to consider that. But it feels wasteful. And it means I can't iterate often.

[Mario Carneiro]

well as long as it only grows monotonically you can reuse the results

[Mario Carneiro]

what order do you get when running the above script?

[Johan Commelin]

This is the first 20 files:

['Mathlib.Util.Superscript', 'Mathlib.Util.Time', 'Mathlib.Util.AssertNoSorry', 'Mathlib.Util.SleepHeartbeats', 'Mathlib.Util.LongNames', 'Mathlib.Util.AddRelatedDecl', 'Mathlib.Util.IncludeStr', 'Mathlib.Util.Export', 'Mathlib.Util.TermBeta', 'Mathlib.Data.List.Func', 'Mathlib.Data.List.ProdSigma', 'Mathlib.Data.List.ToFinsupp', 'Mathlib.Data.List.Intervals', 'Mathlib.Data.List.AList', 'Mathlib.Data.List.Sections', 'Mathlib.Data.List.Lemmas', 'Mathlib.Data.List.DropRight', 'Mathlib.Data.List.Card', 'Mathlib.Data.List.Sym', 'Mathlib.Data.List.Destutter']

[Johan Commelin]

Mario Carneiro said:

well as long as it only grows monotonically you can reuse the results

Right, but as is often the case with refactors, I regularly jump back to fix things lower in the hierarchy.

[Mario Carneiro]

it was looking good until Mathlib.Data.List.Func

[Mario Carneiro]

I suspect that all of the ones that came before it have no mathlib imports at all

[Mario Carneiro]

so it could also be an issue in the import parsing

[Johan Commelin]

Yeah, but I don't see the bug

[Johan Commelin]

Also:

>>> print(dependencies['Mathlib.Data.List.Func'])
['Mathlib.Data.Nat.Order.Basic']

[Mario Carneiro]

and print(dependencies['Mathlib.Data.Nat.Order.Basic']) is also something?

[Johan Commelin]

Yes

['Mathlib.Algebra.Order.Ring.Canonical', 'Mathlib.Data.Nat.Basic', 'Mathlib.Init.Data.Nat.Bitwise']

[Mario Carneiro]

Oh I think I see the issue

if any(dependency not in successful_files for dependency in G.predecessors(file)):

this will return true for any file which has a non-mathlib dependency (recall that non-mathlib files are in the graph G)

[Johan Commelin]

Ooh, good catch!

[Johan Commelin]

This is the version of the script that I'm currently using:

import os
import sys
import subprocess
import networkx as nx
from collections import defaultdict
import time

# Traverse the repository to find all .lean files and parse their import statements
dependencies = defaultdict(list)
for root, dirs, files in os.walk('./Mathlib'):
    for file in files:
        if file.endswith('.lean'):
            filepath = os.path.join(root, file)
            index = filepath[2:].replace('/', '.').replace('.lean', '')
            with open(filepath, 'r') as f:
                for line in f:
                    if line.startswith('import '):
                        dep = line.split(' ')[1].strip()
                        if dep.startswith('Mathlib'):
                            dependencies[index].append(dep)
                    elif line.startswith('/-!'):
                        break

# Create a graph from the dependencies
G = nx.DiGraph(dependencies)

# Perform a topological sort on the graph
try:
    sorted_files = [file for file in nx.topological_sort(G) if file.startswith('Mathlib')]
    sorted_files.reverse()
except nx.NetworkXUnfeasible:
    print("Graph contains a cycle:", file=sys.stderr)
    cycle = nx.simple_cycles(G)
    print(next(cycle))
    exit()

# Attempt to build each file in the sorted order
successful_files = []
for i, file in enumerate(sorted_files):
  # Skip building the file if any of its dependencies weren't successfully built
  if any(dependency not in successful_files for dependency in dependencies[file]):
    continue
  try:
    # print("Attempting to build", file, file=sys.stderr)
    subprocess.check_call(['lake', 'build', file], stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL)
    successful_files.append(file)
    print(file)
  except subprocess.CalledProcessError:
    pass

[Damiano Testa]

More generally, I have often wanted some tooling for finding out future dependencies of current declarations.

Even just something as simple as scanning ileans, looking for usages of a specific declaration would be beneficial for refactors and also for giving better automation for breaking changes.

[Marc Huisinga]

Damiano Testa said:

More generally, I have often wanted some tooling for finding out future dependencies of current declarations.

Even just something as simple as scanning ileans, looking for usages of a specific declaration would be beneficial for refactors and also for giving better automation for breaking changes.

Does the call hierarchy do some of what you want? (Right click on an identifier and select "Show call hierarchy")

[Mario Carneiro]

you can also use the "go to definition" action on a definition, where it means "find references" instead

[Damiano Testa]

@Marc Huisinga and @Mario Carneiro I knew of neither of these functionalities and they are both excellent, thanks!

[Marc Huisinga]

That's what the .ilean files were added for originally :-)

[Damiano Testa]

Thanks for the further information! Btw, is there a description of what the ileans encode now? A few weeks ago, they simply had info like (roughly) "c:decl_name:usages{[coordinates of begin end usages],definition[coordinates of definition, if available]]}".

What do they contain now?

[Marc Huisinga]

The corresponding Lean type for .ilean files is at Lean.Server.Ilean in Lean/Server/References.lean.
It's still a map from an identifier (on master this is a combination of a module name and an identifier name to disambiguate conflicting identifier names from separate modules) to its definition / usages, where both definition and usages now also store information about the parent declaration of each reference.

The JSON format has changed a bit, though.

[Damiano Testa]

Ok, when I'll try to use it, I will try to avoid looking at the ilean explicitly!

Btw, I often would like to have information about where each declaration begins/ends. For instance, something that would also take into account doc-strings and attributes for lemmas. Is this available as well?

[Damiano Testa]

E.g. for

/-- I am a docstring.
Spread over several lines -/
@[simp]
lemma name {n : Nat} : n + 0 = n := by
  have := 0
  simp

it would begin at the /-- and end at simp.