transitive deps of a def?

Stream: Is there code for X?

[Alok Singh]

the idea is to extract the necessary code to make a self-contained runnable example.

Say we have code to sum a function like

def sum (xs: List Int) : Int := xs.foldl (. + . ) 0

Then running the desired code would give a file that exposes the definitions of foldl and maybe of List.

This is for verilib.org, to allow 'atomizing' code so people can pull out single verified definitions instead of a whole project, at the cost of a bunch of essentially copy-pasted code coming along for the ride.

[Chris Bailey]

https://leanprover-community.github.io/mathlib4_docs/Lean/Util/FoldConsts.html#Lean.Expr.getUsedConstants

[Chris Bailey]

The ones that work on an element of Lean.ConstantInfo are more specifically "of a def".

[Chris Bailey]

May be more helpful since it's not obvious how to get names to resolve:

import Lean
open Lean Meta Elab
syntax "#go" ident : command

elab "#go" n:ident : command => do
  match (← Lean.resolveGlobalConst n) with
  | [] => throwError s!"no declar found for {n}"
  | hd :: _ =>
  let constInfo ← Lean.getConstInfo hd
  let deps := constInfo.getUsedConstantsAsSet
  logInfo s!"deps := {deps.toArray}"

#go Nat.mul

[Adam Topaz]

That’s not the transitive deps, just the immediate deps

[Johan Commelin]

The ImportGraph package has some helper functions for the transitive closure of deps

[Adam Topaz]

Here is the relevant function: https://github.com/leanprover-community/import-graph/blob/ed3b856bd8893ade75cafe13e8544d4c2660f377/ImportGraph/RequiredModules.lean#L65

[Adam Topaz]

or for a single name instead of a NameSet: https://github.com/leanprover-community/import-graph/blob/ed3b856bd8893ade75cafe13e8544d4c2660f377/ImportGraph/RequiredModules.lean#L81

[Chris Bailey]

Adam Topaz said:

That’s not the transitive deps, just the immediate deps

Touche; it should recursively map over the results. I wasn't aware there was an import graph library, that's good to know.

[Alok Singh]

Works well (thanks Johan and Adam), now I'm looking to get line/col numbers for a definition.

[Alok Singh]

Is there a function that does this? Given a declaration, extract the line/column/file name where it was defined?

[Adam Topaz]

This info will be present in the info trees.

[Alok Singh]

Thanks, digging into how to construct/extract such a tree now. I found https://github.com/adamtopaz/lean_extras (how appropriate) and am reading through it now.

[Damiano Testa]

There was also this previous thread.