jixia

Stream: general

[Riccardo Brasca]

This is a thread to discuss jixia. See the announcement.

[Riccardo Brasca]

@Tony Beta Lambda can this tool be used to visualize a dependency graph of a given declaration?

[Tony Beta Lambda]

Riccardo Brasca said:

Tony Beta Lambda can this tool be used to visualize a dependency graph of a given declaration?

It can generate all the data needed for such visualization. For the actual visualization I recommend lean-graph.

[Ruben Van de Velde]

Hmm, that might be an interesting use case for distinguishing theorems from lemmas

[Riccardo Brasca]

I am still looking for something that makes easy to find unused declaration in a project (wrt to a final goal). Maybe this can help...

[Yaël Dillies]

@Sky Wilshaw has written that something

[Sky Wilshaw]

I wrote some stuff here: https://github.com/leanprover-community/con-nf/blob/main/DependencyGraph.lean

[Sky Wilshaw]

I didn't intend for this to be used outside of the Con(NF) project so some tweaking will need to be done before it's usable

[Riccardo Brasca]

Thanks!! I am having a look

[Riccardo Brasca]

Can you explain (briefly) how to use it?

[Sky Wilshaw]

The way it currently works is that if you replace import ConNF with import <your_project> and write #unseen at the end of the file, it'll do all the calculations and tell you what's not currently used.

[Sky Wilshaw]

This isn't ideal, but works enough for my purposes - I have a CI step that manually appends #unseen to that file and reads off its output.

[Sky Wilshaw]

It's not written in there by default because computing unseen defs takes quite a long time, so I didn't want to have it run unless it really needs to.

[Riccardo Brasca]

I guess I have to replace ConNF with the name of my project everywhere in the script, right?

[Sky Wilshaw]

I think so, yes.

[Riccardo Brasca]

It seems it works, thanks a lot!!

[Riccardo Brasca]

I am not an expert but I am sure this is something can be useful for a lot of people.

[Riccardo Brasca]

Are you interested in improving it? For example I think it lists declarations generated by simps, that cannot be removed. Note that I am not complaining (quite the opposite!), but if you or someone else is interested we can make it an "official" mathlib script.

[Sky Wilshaw]

I don't think I know enough yet about Lean meta stuff to do a good job of cleaning this up and making it more generally usable - I just haven't really had the time to learn it properly. In the meantime, if anyone else with more knowledge is interested, feel free to give it a shot.

[Kim Morrison]

@Riccardo Brasca, @Sky Wilshaw, it would be lovely if this functionality could be added to the existing import-graph repository, which Mathlib already depends on.

[Tony Beta Lambda]

Riccardo Brasca said:

I am still looking for something that makes easy to find unused declaration in a project (wrt to a final goal). Maybe this can help...

Yes, it is possible with the data provided by jixia. The dependency relation is computed per "symbol", which can be linked to "declaration" by the equation symbol.name == declaration.fullname.

1. Find your declaration's fullname.
2. Compute its transitive dependencies with data in .sym.json files.
3. Find all relevant declarations.

We are limiting the scope of jixia to extracting info from a lean project for interoperability with other tools, so this won't be part of jixia. But we are planning to write a set of useful scripts (most likely in python) to work with data generated by jixia, and this can be one of them.