feat(scripts): scrape typeclass hierarchy into json

[jcommelin]

Co-authored by: Floris van Doorn fpvdoorn@gmail.com

---

Sample output: https://gist.github.com/46f68be10416f645241a0deb4da66327

[bryangingechen]

Maybe this should be part of doc-gen?

[jcommelin]

Fine with me... let's put it there once we are happy with the script.
I just made a PR so that the script doesn't get lost.

[urkud]

Could you please upload the output?

And while you're at it, it would be nice to have a table with columns nat, int, rat, real, nnreal, ennreal (what else?), rows corresponding to various classes and ✓ at intersections if we have an instance?

[jcommelin]

(what else?)

complex

Sample output: https://gist.github.com/46f68be10416f645241a0deb4da66327

[urkud]

Output LGTM. Didn't try to understand the code.

[alexjbest]

Is the format of this meant as input for something specific? If so we could say what in the code so people understand the format.

It doesn't seem to match https://jsongraphformat.info/ so if this is just a random format at the moment we could tweak this to match that, might make it easier to use this data in different places in future.

[robertylewis]

Is the format of this meant as input for something specific? If so we could say what in the code so people understand the format.

Seconded. Regardless, I'd propose moving this to doc_gen where we can integrate something to generate a pretty picture for the docs pages.

[bryangingechen]

@jcommelin do you mind moving this to https://github.com/leanprover-community/doc-gen ? You can just put typeclass_stats.lean in src/ for now. Then we can discuss / work on it further there.

[jcommelin]

@bryangingechen Voila: leanprover-community/doc-gen#52