lake exe graph

Stream: mathlib4

[Yury G. Kudryashov]

I tried to run lake exe graph and got

uncaught exception: could not find native implementation of external declaration 'UInt64.ofNatCore' (symbols 'l_UInt64_ofNatCore___boxed' or 'l_UInt64_ofNatCore')

[Yury G. Kudryashov]

OS: NixOS Linux

[Yury G. Kudryashov]

@Scott Morrison :up:

[Scott Morrison]

I doubt this is due to anything specific to graph. Could you try minimizing ImportGraph/Main.lean, seeing if the error goes away as you remove dependencies?

[Yury G. Kudryashov]

Minimized to

/-
Copyright (c) 2023 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import Mathlib.Util.Imports
import Mathlib.Lean.IO.Process

/-!
# `lake exe graph`

This is a replacement for Lean 3's `leanproject import-graph` tool.
-/

open Lean Meta

/-- Write an import graph, represented as a `NameMap (Array Name)` to the ".dot" graph format. -/
def asDotGraph (_ : NameMap (Array Name)) (_ := "import_graph") : String := ""

open Lean Core System

-- Next two declarations borrowed from `runLinter.lean`.

instance : ToExpr FilePath where
  toTypeExpr := mkConst ``FilePath
  toExpr path := mkApp (mkConst ``FilePath.mk) (toExpr path.1)

elab "compileTimeSearchPath" : term =>
  return toExpr (← searchPathRef.get)

open IO.FS IO.Process in
/-- `lake exe graph` -/
def main : IO Unit := do
  searchPathRef.set compileTimeSearchPath
  let _ ← unsafe withImportModules [{module := `Mathlib}] {} (trustLevel := 1024) fun env =>
    return asDotGraph env.importGraph

[Mauricio Collares]

Try setting supportInterpreter := true in the lake_exe graph section of the lakefile

[Yury G. Kudryashov]

Does it switch from "compile&run" to "interpret"? If yes, then this sounds like a workaround, not a solution.

[Yury G. Kudryashov]

I mean, probably there is a bug in lake or lean behind this and while we can run small executables like graph in interpreted mode, the bug may appear later in a larger executable where running it in the interpreted mode will not be desirable.

[Sebastian Ullrich]

Yury G. Kudryashov said:

Does it switch from "compile&run" to "interpret"? If yes, then this sounds like a workaround, not a solution.

It does not: https://github.com/leanprover/lake#binary-executables

[Yury G. Kudryashov]

Thank you!

[Yury G. Kudryashov]

I added supportInterpreter := true. Now it works better but it needs oleans. Is this intentional? Lake should have all the information about dependencies somewhere. Can't we just ask it?

[Mario Carneiro]

What do you mean? Anything that uses withImportModules or similar has to read olean files on disk. These are found via the search path, but since you are using a compile time search path it will only work if the program is run from the project root and the files are in the same place as they were at compile time

[Yury G. Kudryashov]

I mean that lake somehow knows dependencies of all files before they're compiled. I wonder if we can ask it instead about this information instead of whatever API is used now.

[Arthur Paulino]

I think Lake doesn't have an API to build the dependency graph out of the box.

One possibility, however, is doing what Cache does to figure out (and traverse) the dependency tree. It basically parses text files. You can look at the source code for the hashing routine.

[Yury G. Kudryashov]

So, lake parses source files, builds the dependency graph but doesn't have an API to query this information?

[Arthur Paulino]

Yes

[Yury G. Kudryashov]

So, the proper fix is to add this API to lake?

[Arthur Paulino]

It's not needed by Lake. Lake does its job by traversing dependencies on demand, like Cache

[Arthur Paulino]

Unless there's a design decision to refactor Lake so it precomputes the whole DAG before doing anything. Then it would make sense to add such API (since it's needed)

[Yury G. Kudryashov]

But it has functions like "give me all dependencies of this file" or "give me all goals in this module".

[Arthur Paulino]

Yes

[Mario Carneiro]

lean already has the API, Lean.parseImports'

[Yury G. Kudryashov]

Why doesn't withImportGraph use this?

[Mario Carneiro]

:shrug:

[Mario Carneiro]

I don't see a withImportGraph function in mathlib4, lean4 or lake

[Yury G. Kudryashov]

I'm sorry, it doesn't exist.

[Yury G. Kudryashov]

I mean, why doesn't docs#Lean.Environment.importGraph parse files instead of using oleans.

[Mario Carneiro]

because it's way more expensive?

[Mario Carneiro]

if you already have oleans it's probably better to use them than to parse text files

[Mario Carneiro]

I think I timed this at one point

[Eric Wieser]

And if you don't have oleans then you don't have a guarantee that your imports exist

[Eric Wieser]

Or that the graph they form is acyclic

[Yury G. Kudryashov]

Thank you for the explanation.

[Sorawee Porncharoenwase]

I tried lake exe graph. While it generates a dot file for my project dependencies (Mathlib, etc) fine, it doesn't generate entries for my project itself. How do I make it recognize the module in my project?

Note that my .olean files are under build/lib. Do I need to specify this path anywhere?

[Mario Carneiro]

Sorawee Porncharoenwase said:

Note that my .olean files are under build/lib. Do I need to specify this path anywhere?

unlikely, most lean processing tools already know this and should be able to find the oleans without any additional hints as long as they are run using lake env, lake exe, or lake run

[Mario Carneiro]

looking at the code it appears that if you don't specify a main module it defaults to Mathlib

[Mario Carneiro]

lake exe graph --to MyProject seems to work

[Sorawee Porncharoenwase]

I read the the --help page and thought that : is a part of the command-line syntax, and so I wrote lake exe graph --to : MyProject. /facepalm

Anyhow, lake exe graph --to MyProject doesn't work either (empty digraph), but I now know why: I have

globs := #[`MyProject, .submodules `MyProject]

in lakefile.lean, and MyProject.lean is essentially an empty file. If I directly specify a path to a module that has actual Lean content, it works as expected!

So I guess the globs trick doesn't play well with lake exe graph, and it's better to generate a main file that imports everything instead.

[Mario Carneiro]

that sounds like it is working as expected

[Mario Carneiro]

if the MyProject module doesn't have any dependencies, then you should just get a single node

[Sorawee Porncharoenwase]

Right. And thank you! Really appreciate the help.

[Patrick Massot]

How is lake exe graph meant to work in a project depending on mathlib. I was expecting it to generate a graph of the project file, excluding mathlib, but it doesn't. @Scott Morrison

[Patrick Massot]

Nevermind, I noticed this topic already existed and contains the answer. So let's turn this into a documentation question. How is this meant to be documented?

[Kevin Buzzard]

(on the linux app when you start a topic which already exists, a right-arrow appears by the topic and if you click on it you can see previous messages sent to the topic. This is a relatively recent addition)

[Scott Morrison]

Can we access the name of the current project?

[Scott Morrison]

@Patrick Massot #7738

[Patrick Massot]

I don't understand the new doc, or the option name really.

[Patrick Massot]

I would rather expect that --from would achieve this.

[Scott Morrison]

I have always understood import graphs to have edges consistent with the "upstream" and "downstream" naming scheme: i.e. edges point to downstream files, from upstream files.

[Scott Morrison]

But maybe you have the opposite orientation in mind?

[Scott Morrison]

The root files of a project should appear at the top of the displayed graph, and the most complicated at the bottom, and the edges should point down the screen.

[Scott Morrison]

hence --to MyProject

[Scott Morrison]

Ideally someone would move graph out of Mathlib into its own project depending only on Std and Cli, so that it is usable elsewhere.

[Scott Morrison]

In the same PR, I just added a more helpful message if graphviz is missing.

[Patrick Massot]

I agree with all that, but I don't understand why --to MyProject removes Mathlib which is way upstream of MyProject.

[Scott Morrison]

ah, this happened in #6151. Initially it was proposed as a --noDeps flag, but I suggested, apparently incorrectly, that it would be better as a default.

[Scott Morrison]

Would you like me to switch that?

[Scott Morrison]

I had assumed that Mathlib was so enormous that no one would ever want to see all of it.

[Patrick Massot]

Oh I agree that --noDeps is a good default.

[Patrick Massot]

And now I understand your sentence!

[Scott Morrison]

Let me know if I should further change the docs!

[Patrick Massot]

I think part of my confusion is that I'm not used to the Mathlib module being all of Mathlib, and same with MyProject.

[Patrick Massot]

But I don't have a clearer wording.

[Patrick Massot]

Maybe I'm simply a bit tired.

[Scott Morrison]

Yes. I'm a bit worried that encouraging people to use globs rather than a file that imports everything is bifurcating our standard setups, and this is going to bite us down the track.

[Scott Morrison]

But I appreciate that having to maintain a file that imports everything is beyond tedious.

[Patrick Massot]

Another question: is there a way to discover the existence of this graph function?

[Patrick Massot]

It's not only tedious, it's also not clear at all for beginners.

[Scott Morrison]

I guess it is mentioned in the lakefile.lean as

lean_exe graph where
  root := `ImportGraph.Main

but otherwise: no, not at all. :-)

[Scott Morrison]

Part of the answer here is: it should be its own repo, separate from Mathlib, with a README

[Scott Morrison]

Otherwise, what should we add?

[Patrick Massot]

No lake exe --list or lake exe --help?

[Scott Morrison]

There should be a doc-string in the lakefile. (In fact, that should be a requirement!!)

[Patrick Massot]

I mean lake should have a command listing everything you can put after exe in the current project.

[Patrick Massot]

And maybe it has this command.

[Scott Morrison]

lean4#2708

[Scott Morrison]

@Mac Malone, is there any way we can run the linter on the lakefile.lean itself? e.g. here it would be nice if I had not been allowed to add this exe without a doc-string.

[Scott Morrison]

#7738 now includes doc-strings on all the lean_exe declarations in our lakefile

[Patrick Massot]

/-- `lake exe cache` retrieves precompiled `.olean` files from a central server. -/ is a bit too simple.

[Patrick Massot]

lake exe cache alone does nothing, right?

[Scott Morrison]

Good point. It prints a help message! I will change to doc-string to include get, on the basis that this is 99.9% of usage.

[Mac Malone]

Scott Morrison said:

Mac Malone, is there any way we can run the linter on the lakefile.lean itself? e.g. here it would be nice if I had not been allowed to add this exe without a doc-string.

I would think you could run it on lakefile.lean the same way you run it on any other Lean file. Has that not worked?

[Scott Morrison]

@Mac Malone, sorry, should have included that:

% lake exe runMathlibLinter lakefile
uncaught exception: unknown package 'lakefile'

[Mac Malone]

@Scott Morrison Oh, so the linter imports modules oleans rather than elaborating the lean files? In that case, it could probably read the module data of the top-level olean directly rather than importing it to support loading lakefile.olean (since we almost definitely do not want the lakefiles to generally be in the LEAN_PATH) .

[Scott Morrison]

Hmm, I see. Low priority, I guess. :-)

[Utensil Song]

Is the result of lake exe graph published somewhere for Mathlib? Is it expected to generate something like Dependency graph in blueprint, i.e. assigning background colors and border colors according to whether it's sorry-free or whether all its prerequisites are sorry-free?

image.png

[Utensil Song]

Oh, so far it seems to be only about modules, not declarations.

[Scott Morrison]

@Utensil Song, there are no sorries in Mathlib! :-)

[Scott Morrison]

lake exe graph for all of Mathlib is already extremely large and unreadable, at the module level. I can't imagine what the 150000 declaration graph would look like ...

[Utensil Song]

Scott Morrison said:

Utensil Song, there are no sorries in Mathlib! :-)

Yes, but I thought we are also talking about formalization projects that depend on Mathlib.

Scott Morrison said:

lake exe graph for all of Mathlib is already extremely large and unreadable, at the module level. I can't imagine what the 150000 declaration graph would look like ...

Also inspired by this topic, no one wants a full graph, but a graph with branch pruning (only the transitively used declarations, not the unused ones imported along with them, and you can select from or to which module level that you are interested) would be quite useful, even for Mathlib.

[Kevin Buzzard]

There will be plenty of sorries in FLT corresponding to hard theorems from pre-Wiles which we will be initially ignoring

[Kevin Buzzard]

I think a nice red "we are cheating here" would be fine

[Kevin Buzzard]

Oh except I wouldn't want that to pollute "we are currently working on this and will finish in a few months"