multiple transitive closure computation scripts

Stream: Equational

[Andrés Goens]

There seems to be three different ways of computing the transitive closure of implications and I've lost the overview of which one is which (or why there's three different ones). There's:

• scripts/extract_implications.lean I thought this was the canonical one, as it actually checks the Lean implications, and it seem to be used by generate_dashboard.py
• scripts/transitive_closure.rb which seems to be used by graph.rb and generate_graphviz_graph.rb
• scripts/process_implications.py which seems to be used by generate_imaghe.py and generate_most_wanted_list.py.

Is it just three concurrent efforts to do this? Can we agree one a single one that's going to be the ground truth?

(I'm asking for equational#174 to know where we should calculate this, but I think it's a more general question)

[Vlad Tsyrklevich]

I think ground truth should be lake exe extract_implications --closure, but the others are still useful for tooling and re-computing things so they should stick around

[Amir Livne Bar-on]

Author of process_implications here. Everything it does is included in the extract_implications.
I looked at the 2 scripts that import it, they only use it for parsing, which is provided by "extract_implication raw". And actually, both scripts only calculate the transitive closure of implications and not of non-implications, so they better use "extract_implications outcomes" instead to get that closure too.

[Vlad Tsyrklevich]

yeah so the ruby and python implementation authors both say use extract_implications as ground truth