leancrawler

Stream: general

[Daniel Selsam]

@Patrick Massot What is the status of leancrawler? I would like to generate a visualization of the instance graph across mathlib & friends, and I am wondering whether to build on leancrawler.

[Bryan Gin-ge Chen]

I played with it about 2 months ago; I had to make some minor (but straightforward) changes for compatibility with the latest mathlib though.

edit: see this PR

[Daniel Selsam]

@Bryan Gin-ge Chen Thanks, so should I start with your compatibility branch?

[Bryan Gin-ge Chen]

Sure, try it out and let me know if it works. This crawling script might also be helpful: https://gist.github.com/bryangingechen/e1b460d146549df09df4b5a4a9b2656f (you'll have to edit the paths for your computer)

[Daniel Selsam]

@Bryan Gin-ge Chen Thanks, will do.

[Patrick Massot]

Leancrawler is pretty hacky, it should be redone by someone who actually knows about programming in general, and Lean meta-programming in particular. But last time I checked it was still usable. It was used to produce the big picture at https://leanprover-community.github.io/lean-perfectoid-spaces/

[Patrick Massot]

I'll have a look at Bryan's PR when I'll find some time (which is really rare those days).

[Daniel Selsam]

@Patrick Massot

It was used to produce the big picture

Very cool! Thanks for sharing.