graphs: tc hierarchy

Stream: general

[Johan Commelin]

@Floris van Doorn you had some scripts that generated graphs of the type class hierarchy. Is that right? Do you still have them somewhere?

[Johan Commelin]

If so, we can probably teach them to output json.

[Floris van Doorn]

Yes, and I put it here: https://gist.github.com/fpvandoorn/4d4c52322d7eb661e5154f9a732754d4

It currently produces output like this:

partial_order:
  File: C:\Users\Floris\.elan\toolchains\leanprover-community-lean-3.14.0\lib\lean\library\init\algebra\order.lean
  Line: 26
  Type: class
semilattice_inf_bot_of_bounded_lattice:
  File: d:\projects\mathlib\src\order\bounded_lattice.lean
  Line: 250
  Type: instance
  Source: bounded_lattice
  Target: semilattice_inf_bot
group.to_has_inv:
  File: d:\projects\mathlib\src\algebra\group\basic.lean
  Line: 219
  Type: instance
  Source: group
  Target: has_inv
order_bot:
  File: d:\projects\mathlib\src\order\bounded_lattice.lean
  Line: 94
  Type: class
[...]

It shouldn't be hard to modify the output.

It currently mostly prints "the algebraic hierarchy". This means instances and classes that have at most 1 argument that is not a type-class argument (within square brackets), and the instances can only be forgetful instances (where the conclusion is a class applied to a variable).

[Floris van Doorn]

What is the output you want, and how do you want to use it? Automatically generating a graph would be nice.

[Johan Commelin]

The idea would be to automatically generated an interactive graph using d3.js

[Johan Commelin]

So the output should probably be some sort of json, although Patrick also linked to a package that can convert .dot files into d3 graphs.

[Johan Commelin]

@Bryan Gin-ge Chen The output of the script by Floris (see above) is yaml... is that ok for you? I guess we can easily postprocess that into suitable json, right?

[Bryan Gin-ge Chen]

Yes, it shouldn't be too hard to postprocess. I bet the script could be modified to output JSON pretty easily too though.

[Johan Commelin]

Right, that's what I thought. What kind of JSON format are we looking for?

[Bryan Gin-ge Chen]

For experimentation we can just go with whatever's quickest to implement.

[Johan Commelin]

Should it look like

[ # a list of edges
{ source : 'group', target: 'monoid' },
{ blabbla },
]

[Bryan Gin-ge Chen]

Yeah, I think that would work fine (modulo correct JSON syntax :wink: )

[Johan Commelin]

/me doesn't really know json

[Johan Commelin]

I'll try to hack the output into that form once my kids are in bed

[Bryan Gin-ge Chen]

No worries, I probably won't have time to play around with graphs until the weekend, and I can probably quickly do this myself then.

[Floris van Doorn]

There's also the question what you want the content of the graph to be exactly. The algebraic hierarchy? All type-classes?
I think currently my script gives you a bit more than the algebraic hierarchy. It gives you all "unary type-classes" but I think there are also some typeclasses with argument m : Type u -> Type u which you might want to remove.

[Johan Commelin]

I was thinking initially just all type classes...

[Johan Commelin]

But maybe you get lots of junk then?

[Floris van Doorn]

Well, if your idea is to get a graph similar to the one in the mathlib paper, then I recommend just using the algebraic hierarchy + "forgetful" instances. For other classes/instances it's a lot less clear what arrows to draw.
What arrows represent group A -> group B -> group (A x B) or decidable_eq A -> decidable_eq (list A) or decidable_eq real?

[Johan Commelin]

Hmmm, I hadn't really thought about the edges, I think. Your suggestion sounds good to me.

[Johan Commelin]

I'm going to try to generate an update version of this graph for the workshop

[Johan Commelin]

Now it would be great if we could reuse some sphere eversion machinery (@Patrick Massot) to create a clickable version that takes you to the corresponding page in the docs.

[Patrick Massot]

That part is very easy. The tricky part is to have a meaningful manageable graph to display.

[Johan Commelin]

I just ran the script by Floris. It generates a graph with 120 edges.

[Johan Commelin]

Oops, that's wrong

[Johan Commelin]

My new count is about 520 nodes and 400 edges. Which still seems weird.

[Johan Commelin]

I'm trying to make the script by Floris output two JSON lists, one with nodes, and one with edges. But I'm bad at meta stuff. Here is what I have so far:

import algebra.group.defs

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

def file_to_topic : string → string :=
λ s, (s.split_on '/').head

structure item :=
(file : string)
(line : string)
(name : string)
(topic : string := file_to_topic file)

structure node extends item.

namespace node

def jsonify : node → string :=
λ n,
"{ name : " ++ n.name ++ ",\n" ++
  "topic : " ++ n.topic ++ ",\n" ++
  "file : " ++ n.file ++ ",\n" ++
  "line : " ++ n.line ++ " }\n"

instance : has_to_string node := ⟨jsonify⟩

end node

structure edge extends item :=
(source : string)
(target : string)

namespace edge

def jsonify : edge → string :=
λ e,
"{ name : " ++ e.name ++ ",\n" ++
  "topic : " ++ e.topic ++ ",\n" ++
  "source : " ++ e.source ++ ",\n" ++
  "target : " ++ e.target ++ ",\n" ++
  "file : " ++ e.file ++ ",\n" ++
  "line : " ++ e.line ++ " }\n"

instance : has_to_string edge := ⟨jsonify⟩

end edge

/- parses information about `decl` if it is an instance or a class. -/
meta def parse_decl (env : environment) (decl : declaration) :
  tactic (option (node ⊕ edge)) :=
let name := decl.to_name in
do
    if (env.decl_olean name).is_some
    then do
      olean_file ← env.decl_olean name,
      let I : item :=
      { name := to_string name,
        file := olean_file,
        line := pos_line (env.decl_pos name) },
      is_c ← tactic.has_attribute `class name,
      if is_c.1 then
        let N : node := { .. I } in
        return (some (sum.inl N))
      else do
      is_i ← tactic.has_attribute `instance name,
      if is_i.1 then do
        (l, tgt) ← return decl.type.pi_binders,
        guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit),
        guard (tgt.get_app_args.head.is_var && l.ilast.type.get_app_args.head.is_var),
        let src := to_string l.ilast.type.erase_annotations.get_app_fn.const_name,
        let tgt := to_string tgt.erase_annotations.get_app_fn.const_name,
        guard (src ≠ tgt),
        let E : edge := { name := to_string name, source := src, target := tgt, .. I },
        return (some (sum.inr E))
      else do return none
    else do return none

variables {α β : Type*}

def list.remove_none : list (option α) → list α
| []            := []
| (none :: l)   := l.remove_none
| (some a :: l) := a :: l.remove_none

def list.split_sum : list (α ⊕ β) → (list α) × (list β)
| []  := ([], [])
| ((sum.inl a) :: l) := let L := l.split_sum in ((a :: L.1), L.2)
| ((sum.inr b) :: l) := let L := l.split_sum in (L.1, (b :: L.2))

/-- prints information about unary classes and forgetful instances in the environment.
  It only prints instances and classes that have at most 1 argument
  that is not a type-class argument (within square brackets),
  and the instances can only be forgetful instances
  (where the conclusion is a class applied to a variable) -/
meta def print_content : tactic unit :=
do curr_env ← get_env,
   o ← (curr_env.fold list.nil list.cons).mmap (parse_decl curr_env),
   trace (to_string o.remove_none.split_sum),
   skip

meta def test : tactic unit :=
do curr_env ← get_env,
   d ← get_decl `comm_monoid,
   trace (to_string d.to_name),
   o ← parse_decl curr_env d,
   trace (to_string o),
   skip

run_cmd test

run_cmd print_content

[Johan Commelin]

If someone could help, that would be awesome.

[Johan Commelin]

The idea is to be able to generate interactive graphs that will link to the correct docs.
We might need to tweak the info that we save in the nodes and edges.
Also, I want items to have a "topic" so that you can easily hide all the nodes that come from the subdirectory src/algebra, and focus on src/topology, etc...

[Johan Commelin]

(The full graph will be too large to be useful.)

[Rob Lewis]

tactic.has_attribute returns a bool and a nat. The bool isn't whether the attribute is there or not, it's whether the attribute is persistent (non-local). has_attribute will fail if the attribute isn't there.

[Johan Commelin]

Aha... so what do I do now?

[Rob Lewis]

You can use succeeds if you don't actually need the output of has_attribute, which I don't think you do.

[Johan Commelin]

Is there some sort of success thing? That I should prepend?

[Johan Commelin]

I now have, but it still doesn't seem to work

import algebra.group.defs

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

def file_to_topic : string → string :=
λ s, (s.split_on '/').head

structure item :=
(file : string)
(line : string)
(name : string)
(topic : string := file_to_topic file)

structure node extends item.

namespace node

def jsonify : node → string :=
λ n,
"{ name : " ++ n.name ++ ",\n" ++
  "topic : " ++ n.topic ++ ",\n" ++
  "file : " ++ n.file ++ ",\n" ++
  "line : " ++ n.line ++ " }\n"

instance : has_to_string node := ⟨jsonify⟩

end node

structure edge extends item :=
(source : string)
(target : string)

namespace edge

def jsonify : edge → string :=
λ e,
"{ name : " ++ e.name ++ ",\n" ++
  "topic : " ++ e.topic ++ ",\n" ++
  "source : " ++ e.source ++ ",\n" ++
  "target : " ++ e.target ++ ",\n" ++
  "file : " ++ e.file ++ ",\n" ++
  "line : " ++ e.line ++ " }\n"

instance : has_to_string edge := ⟨jsonify⟩

end edge

/- parses information about `decl` if it is an instance or a class. -/
meta def parse_decl (env : environment) (decl : declaration) :
  tactic (option (node ⊕ edge)) :=
let name := decl.to_name in
do
    if (env.decl_olean name).is_some
    then do
      olean_file ← env.decl_olean name,
      let I : item :=
      { name := to_string name,
        file := olean_file,
        line := pos_line (env.decl_pos name) },
      is_c ← succeeds (tactic.has_attribute `class name),
      if is_c then
        let N : node := { .. I } in
        return (some (sum.inl N))
      else do
      is_i ← succeeds (tactic.has_attribute `instance name),
      if is_i then do
        (l, tgt) ← return decl.type.pi_binders,
        guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit),
        guard (tgt.get_app_args.head.is_var && l.ilast.type.get_app_args.head.is_var),
        let src := to_string l.ilast.type.erase_annotations.get_app_fn.const_name,
        let tgt := to_string tgt.erase_annotations.get_app_fn.const_name,
        guard (src ≠ tgt),
        let E : edge := { source := src, target := tgt, .. I },
        return (some (sum.inr E))
      else do return none
    else do return none

variables {α β : Type*}

def list.remove_none : list (option α) → list α
| []            := []
| (none :: l)   := l.remove_none
| (some a :: l) := a :: l.remove_none

def list.split_sum : list (α ⊕ β) → (list α) × (list β)
| []  := ([], [])
| ((sum.inl a) :: l) := let L := l.split_sum in ((a :: L.1), L.2)
| ((sum.inr b) :: l) := let L := l.split_sum in (L.1, (b :: L.2))

/-- prints information about unary classes and forgetful instances in the environment.
  It only prints instances and classes that have at most 1 argument
  that is not a type-class argument (within square brackets),
  and the instances can only be forgetful instances
  (where the conclusion is a class applied to a variable) -/
meta def print_content : tactic unit :=
do curr_env ← get_env,
   o ← (curr_env.fold [] list.cons).mmap (parse_decl curr_env),
   trace (to_string o.remove_none.split_sum),
   skip

meta def test : tactic unit :=
do curr_env ← get_env,
   d ← get_decl `comm_monoid.to_comm_semigroup,
   trace (to_string d.to_name),
   o ← parse_decl curr_env d,
   trace (to_string o),
   skip

run_cmd test

run_cmd print_content

[Johan Commelin]

This bit

meta def print_content : tactic unit :=
do curr_env ← get_env,
   o ← (curr_env.fold [] list.cons).mmap (parse_decl curr_env),
   skip

gives an error

[Johan Commelin]

failed
state:
⊢ true

[Anne Baanen]

It looks like the line guard (tgt.get_app_args.head.is_var && l.ilast.type.get_app_args.head.is_var), is the one that fails. What is the goal of that check?

[Johan Commelin]

I don't know... it was there in Floris's version

[Anne Baanen]

I'm guessing then that it detects declarations that we don't want to process. In that case, the issue is that the first failing declaration aborts the whole command, so we want to wrap the command in a <|> return none. Let's see if it helps...

[Johan Commelin]

Without the guards it works!

[Johan Commelin]

import algebra.group.defs

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

def file_to_topic : string → string :=
λ s, (s.split_on '/').head

structure item :=
(file : string)
(line : string)
(name : string)
(topic : string := file_to_topic file)

structure node extends item.

namespace node

def jsonify : node → string :=
λ n,
"{ name : " ++ n.name ++ ",\n" ++
  "topic : " ++ n.topic ++ ",\n" ++
  "file : " ++ n.file ++ ",\n" ++
  "line : " ++ n.line ++ " }\n"

instance : has_to_string node := ⟨jsonify⟩

end node

structure edge extends item :=
(source : string)
(target : string)

namespace edge

def jsonify : edge → string :=
λ e,
"{ name : " ++ e.name ++ ",\n" ++
  "topic : " ++ e.topic ++ ",\n" ++
  "source : " ++ e.source ++ ",\n" ++
  "target : " ++ e.target ++ ",\n" ++
  "file : " ++ e.file ++ ",\n" ++
  "line : " ++ e.line ++ " }\n"

instance : has_to_string edge := ⟨jsonify⟩

end edge

/- parses information about `decl` if it is an instance or a class. -/
meta def parse_decl (env : environment) (decl : declaration) :
  tactic (option (node ⊕ edge)) :=
let name := decl.to_name in
do
    if (env.decl_olean name).is_some
    then do
      olean_file ← env.decl_olean name,
      let I : item :=
      { name := to_string name,
        file := olean_file,
        line := pos_line (env.decl_pos name) },
      is_c ← succeeds (tactic.has_attribute `class name),
      if is_c then
        let N : node := { .. I } in
        return (some (sum.inl N))
      else do
      is_i ← succeeds (tactic.has_attribute `instance name),
      if is_i then do
        (l, tgt) ← return decl.type.pi_binders,
        -- guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit),
        -- guard (tgt.get_app_args.head.is_var && l.ilast.type.get_app_args.head.is_var),
        let src := to_string l.ilast.type.erase_annotations.get_app_fn.const_name,
        let tgt := to_string tgt.erase_annotations.get_app_fn.const_name,
        -- guard (src ≠ tgt),
        let E : edge := { source := src, target := tgt, .. I },
        return (some (sum.inr E))
      else do return none
    else do return none

variables {α β : Type*}

def list.remove_none : list (option α) → list α
| []            := []
| (none :: l)   := l.remove_none
| (some a :: l) := a :: l.remove_none

def list.split_sum : list (α ⊕ β) → (list α) × (list β)
| []  := ([], [])
| ((sum.inl a) :: l) := let L := l.split_sum in ((a :: L.1), L.2)
| ((sum.inr b) :: l) := let L := l.split_sum in (L.1, (b :: L.2))

/-- prints information about unary classes and forgetful instances in the environment.
  It only prints instances and classes that have at most 1 argument
  that is not a type-class argument (within square brackets),
  and the instances can only be forgetful instances
  (where the conclusion is a class applied to a variable) -/
meta def print_content : tactic unit :=
do curr_env ← get_env,
   o ← (curr_env.fold [] list.cons).mmap (parse_decl curr_env),
   let (ns, es) := o.remove_none.split_sum,
   trace (to_string ns),
   trace (to_string es),
   skip

meta def test : tactic unit :=
do curr_env ← get_env,
   d ← get_decl `comm_monoid.to_comm_semigroup,
   trace (to_string d.to_name),
   o ← parse_decl curr_env d,
   trace (to_string o),
   skip

run_cmd test

run_cmd print_content

[Johan Commelin]

Anne Baanen said:

I'm guessing then that it detects declarations that we don't want to process. In that case, the issue is that the first failing declaration aborts the whole command, so we want to wrap the command in a <|> return none. Let's see if it helps...

Ooh, that makes sense. Because I do indeed get garbage output if I simply comment out the guard.

[Johan Commelin]

I don't know exactly where to put the <|> return none. Would be delighted if you show me.

[Anne Baanen]

I tried to put it around the call to parse_decl:

meta def print_content : tactic unit :=
do curr_env ← get_env,
   o ← (curr_env.fold [] list.cons).mmap (λ x, parse_decl curr_env x <|> pure none),
   trace (to_string o.remove_none.split_sum),
   skip

[Anne Baanen]

Then I get output like:

([{ name : partial_order,
topic : ,
file : /home/arch/arb/.elan/toolchains/leanprover-community-lean-3.17.0/lib/lean/library/init/algebra/order.lean,
line : 26 }
, { name : has_coe_t_aux,
topic : ,
file : /home/arch/arb/.elan/toolchains/leanprover-community-lean-3.17.0/lib/lean/library/init/coe.lean,
line : 123 }
, { name : is_cond_left_inv,
topic : ,
file : /home/arch/arb/.elan/toolchains/leanprover-community-lean-3.17.0/lib/lean/library/init/algebra/classes.lean,
line : 55 }
, { name : is_total,
topic : ,
file : /home/arch/arb/.elan/toolchains/leanprover-community-lean-3.17.0/lib/lean/library/init/algebra/classes.lean,
line : 95 }
, ...

[Johan Commelin]

Yup, same here...

[Johan Commelin]

Now, all we need is a way to turn a filename into a topic

[Johan Commelin]

Probably split_on '/', end then take the first thing after src, or after library.

[Johan Commelin]

And for nice links to docs#foobar we probably need to save more stuff, like the full name.

[Johan Commelin]

Or maybe name is already the full name... I don't know.

[Anne Baanen]

Johan Commelin said:

Probably split_on '/', end then take the first thing after src, or after library.

def file_to_topic : string → string :=
λ xs, ".".intercalate ((xs.split_on '/').drop_while (λ x, x ≠ "library" ∧ x ≠ "src")).tail.init

[Anne Baanen]

Maps "/home/arch/arb/.elan/toolchains/leanprover-community-lean-3.17.0/lib/lean/library/init/algebra/classes.lean" to init.algebra

[Johan Commelin]

Cool!

[Johan Commelin]

We'll have to play a bit with the exact value of this function, I guess. But this is a good start.

[Johan Commelin]

This script should not be run by people that have a username library or src :wink:

[Johan Commelin]

I'm reasonably happy with this version:

import algebra.group.defs

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

def prepare_filename₁ : string → list string :=
λ xs, ((xs.split_on '/').drop_while (λ x, x ≠ "library" ∧ x ≠ "src"))

def prepare_filename₂ : list string → list string
| ("library" :: l) := ("core" :: l)
| ("src" :: l)     := l
| _                := []

def filename : string → string :=
"/".intercalate ∘ prepare_filename₂ ∘ prepare_filename₁

def topic : string → string :=
list.head ∘ prepare_filename₂ ∘ prepare_filename₁

structure item :=
(file : string)
(line : string)
(name : string)
(topic : string)

structure node extends item.

namespace node

def jsonify : node → string :=
λ n,
"{ name : " ++ n.name ++ ",\n" ++
  "topic : " ++ n.topic ++ ",\n" ++
  "file : " ++ n.file ++ ",\n" ++
  "line : " ++ n.line ++ " }\n"

instance : has_to_string node := ⟨jsonify⟩

end node

structure edge extends item :=
(source : string)
(target : string)

namespace edge

def jsonify : edge → string :=
λ e,
"{ name : " ++ e.name ++ ",\n" ++
  "topic : " ++ e.topic ++ ",\n" ++
  "source : " ++ e.source ++ ",\n" ++
  "target : " ++ e.target ++ ",\n" ++
  "file : " ++ e.file ++ ",\n" ++
  "line : " ++ e.line ++ " }\n"

instance : has_to_string edge := ⟨jsonify⟩

end edge

/- parses information about `decl` if it is an instance or a class. -/
meta def parse_decl (env : environment) (decl : declaration) :
  tactic (option (node ⊕ edge)) :=
let name := decl.to_name in
do
    if (env.decl_olean name).is_some
    then do
      olean_file ← env.decl_olean name,
      let I : item :=
      { name := to_string name,
        file := filename olean_file,
        line := pos_line (env.decl_pos name),
        topic := topic olean_file },
      is_c ← succeeds (tactic.has_attribute `class name),
      if is_c then
        let N : node := { .. I } in
        return (some (sum.inl N))
      else do
      is_i ← succeeds (tactic.has_attribute `instance name),
      if is_i then do
        (l, tgt) ← return decl.type.pi_binders,
        -- guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit),
        -- guard (tgt.get_app_args.head.is_var && l.ilast.type.get_app_args.head.is_var),
        let src := to_string l.ilast.type.erase_annotations.get_app_fn.const_name,
        let tgt := to_string tgt.erase_annotations.get_app_fn.const_name,
        -- guard (src ≠ tgt),
        let E : edge := { source := src, target := tgt, .. I },
        return (some (sum.inr E))
      else do return none
    else do return none

variables {α β : Type*}

def list.remove_none : list (option α) → list α
| []            := []
| (none :: l)   := l.remove_none
| (some a :: l) := a :: l.remove_none

def list.split_sum : list (α ⊕ β) → (list α) × (list β)
| []  := ([], [])
| ((sum.inl a) :: l) := let L := l.split_sum in ((a :: L.1), L.2)
| ((sum.inr b) :: l) := let L := l.split_sum in (L.1, (b :: L.2))

/-- prints information about unary classes and forgetful instances in the environment.
  It only prints instances and classes that have at most 1 argument
  that is not a type-class argument (within square brackets),
  and the instances can only be forgetful instances
  (where the conclusion is a class applied to a variable) -/
meta def print_content : tactic unit :=
do curr_env ← get_env,
   o ← (curr_env.fold [] list.cons).mmap (λ x, parse_decl curr_env x <|> pure none),
   let (ns, es) := o.remove_none.split_sum,
   trace "{ nodes : \n",
   trace (to_string ns),
   trace ",\n  edges :\n",
   trace (to_string es),
   trace "}",
   skip

meta def test : tactic unit :=
do curr_env ← get_env,
   d ← get_decl `comm_monoid.to_comm_semigroup,
   trace (to_string d.to_name),
   o ← parse_decl curr_env d,
   trace (to_string o),
   skip

-- run_cmd test

run_cmd print_content

[Johan Commelin]

See https://gist.github.com/jcommelin/da4a87f4d7d87b6e11e3308b5ba97771 for the output

[Johan Commelin]

@Bryan Gin-ge Chen Is this the type of json file that you could turn into a nice D3 graph?

[Bryan Gin-ge Chen]

Almost! Just add double quotes around the key names and any string values.

[Johan Commelin]

Ok, cool! Let me try that.

[Johan Commelin]

@Bryan Gin-ge Chen Voila: https://gist.github.com/cffe869fe6ba0f154b15d45a2e4a08f2

[Bryan Gin-ge Chen]

SyntaxError: JSON.parse: unexpected character at line 580 column 11 of the JSON data. Something is still wrong, let me check...

[Johan Commelin]

#3307 contains the script that I'm using.

[Bryan Gin-ge Chen]

Ah, line 580 looks like this: "line" : }. Maybe if there's no line data you'll want to put null there? Or just skip the line field entirely?

[Johan Commelin]

Aah, there is an empty "line"

[Johan Commelin]

Hmm, whatever you think is best.

[Bryan Gin-ge Chen]

I haven't been following, what would an empty line mean?

[Johan Commelin]

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

[Johan Commelin]

We can turn the "" into "null".

[Bryan Gin-ge Chen]

Yeah, that would work.

[Johan Commelin]

I have no idea what it means that p is none...

[Johan Commelin]

@Bryan Gin-ge Chen https://gist.github.com/6d9da8c35a91cacb4a70d5c390c1d17f

[Johan Commelin]

Ooh, that's the script

[Johan Commelin]

https://gist.github.com/6e16f71a163a1dd42a1f9b3ec23f6a9b

[Johan Commelin]

That's updated output

[Bryan Gin-ge Chen]

OK, it parsed! I'll see what I can do later (possibly the weekend). I might prioritize looking at the Live Share stuff first though.

[Johan Commelin]

Ooh, Live Share would be awesome!

[Johan Commelin]

(I still didn't get it to work on my setup, though. Stupid MS sign-in page.)

[Johan Commelin]

I imagine something like https://observablehq.com/@peatroot/interacting-with-directed-acyclic-graphs, where we can hide nodes and edges depending on which topics are selected as "visible".
(I got that link from Bryan, in another thread.)

[Floris van Doorn]

Johan Commelin said:

I don't know... it was there in Floris's version

The goal of my script was to only print unary type classes and forgetful instances between them.

These guards were there to filter out instances that did not fall into this category.
The way my script was setup was that failing means the declaration was skipped.

[Floris van Doorn]

Is a class like src#is_idempotent a class you want to print in your graph?

[Floris van Doorn]

Or an instance like src#nat.has_mod?

[Johan Commelin]

I think I don't really care about those

[Johan Commelin]

I would prefer to get a graph containing things like group, field, topological_space, normed_space, metric_space, topological_monoid, etc...

[Johan Commelin]

But exactly how to characterise those... I dunno

[Floris van Doorn]

That's what my script did, and what those guard expressions did.
I'll modify your script to filter them out.

[Johan Commelin]

To filter what out?

[Johan Commelin]

@Floris van Doorn I think I want basically what your script did. And it seemed that it's what I have now... after Anne debugged it for me.

[Floris van Doorn]

But your script also outputs a bunch of "junk", like the class and instance I mentioned above.

[Johan Commelin]

Aha... no idea why it does that

[Floris van Doorn]

because you removed those guard expressions.

[Johan Commelin]

Ooh, lol... I forgot to uncomment the guards

[Johan Commelin]

This is how it starts after uncommenting them

{ "nodes" :

[{ "name" : "partial_order",
"topic" : "core",
"file" : "core/init/algebra/order.lean",
"line" : 26 }
, { "name" : "has_coe_t_aux",
"topic" : "core",
"file" : "core/init/coe.lean",
"line" : 123 }
, { "name" : "is_cond_left_inv",
"topic" : "core",
"file" : "core/init/algebra/classes.lean",
"line" : 55 }
, { "name" : "is_total",
"topic" : "core",
"file" : "core/init/algebra/classes.lean",
"line" : 95 }
, { "name" : "has_ssubset",
"topic" : "core",
"file" : "core/init/core.lean",
"line" : 340 }
, { "name" : "has_andthen",
"topic" : "core",
"file" : "core/init/core.lean",
"line" : 334 }
, { "name" : "is_cond_right_inv",
"topic" : "core",
"file" : "core/init/algebra/classes.lean",
"line" : 58 }

[Johan Commelin]

Is there a reasonable way to filter out has_coe_t_aux? Or does is quack too much like a group or a topological monoid?

[Floris van Doorn]

It shouldn't be there, since it has two arguments. I think my original script filtered those out.

[Floris van Doorn]

Things like has_mul and the like will of course be printed.

[Floris van Doorn]

Just checked, my original script doesn't print has_coe_t_aux.

[Johan Commelin]

Ok... I clearly blundered.

[Floris van Doorn]

The line

guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit),

was there for both instances and classes, you removed it for classes. You can probably put it back, and it should filter those out.

[Johan Commelin]

thanks!

[Johan Commelin]

I pushed to the PR

[Johan Commelin]

Output now starts with

{ "nodes" :

[{ "name" : "partial_order",
"topic" : "core",
"file" : "core/init/algebra/order.lean",
"line" : 26 }
, { "name" : "has_ssubset",
"topic" : "core",
"file" : "core/init/core.lean",
"line" : 340 }
, { "name" : "add_comm_group",
"topic" : "algebra",
"file" : "algebra/group/defs.lean",
"line" : 301 }
, { "name" : "add_left_cancel_semigroup",
"topic" : "algebra",
"file" : "algebra/group/defs.lean",
"line" : 106 }
, { "name" : "comm_group",
"topic" : "algebra",
"file" : "algebra/group/defs.lean",
"line" : 298 }

[Johan Commelin]

That looks quite promising.

[Floris van Doorn]

If you add guard l.head.type.is_sort (for both instances and classes), that should filter out things like monad.

[Johan Commelin]

Aha... I'm not sure if we want that... would it kill too much?

[Floris van Doorn]

I don't think so, what class on Type* -> Type* do you want to include in your graph?

[Johan Commelin]

Well, maybe we want to allow all the monad and functor etc..., because if you can easily switch them off using the topic field, why not support them?