Update scripts to use Bruno's equation numbering code.

Stream: Equational

[Emmanuel Osalotioman Osazuwa]

This is a continuation of my post here #Equational > The 'extra' equations @ 💬 .

I found 2 other ruby files where find_equation_id.rb could be applied instead of parsing lean files directly.

• equational_theories/Generated/EquationSearch/src/search.rb to generate a bijective map from equation to id and back.
• scripts/generate_graphviz_graph.rb to generate equation list.

The PR refactor: Apply find_equation_id.rb (ported from find_equation_id.py) to related files addresses this.

@Bruno Le Floch @Vlad Tsyrklevich

[Emmanuel Osalotioman Osazuwa]

For the python code which parse the lean equations files directly I found:

• explore_magma.py
• find_dual.py
• generate_equation_implication_js.py
• generate_cadical.py

They could be addressed with a separate PR to refactor.

[Bruno Le Floch]

There may be some interfaces missing in find_equation_id.py, for instance in applications (to the full spectrum problem, and others) I often needed to get the shape+rhyme of each side separately and found myself writing lhs_rhyme = eq.rhyme[:lhs_order + 1] and rhs_rhyme = eq.rhyme[lhs_order + 1:]. Feel free to modify find_equation_id.py if you find such needs, I have no upcoming changes planned.

[Vlad Tsyrklevich]

Osalotioman said:

This is a continuation of my post here #Equational > The 'extra' equations @ 💬 .

I found 2 other ruby files where find_equation_id.rb could be applied instead of parsing lean files directly.

• equational_theories/Generated/EquationSearch/src/search.rb to generate a bijective map from equation to id and back.
• scripts/generate_graphviz_graph.rb to generate equation list.

The PR refactor: Apply find_equation_id.rb (ported from find_equation_id.py) to related files addresses this.

Neither of these scripts are used, so I'd suggest closing this instead of spending the time to check that the resulting changes work correctly

[Vlad Tsyrklevich]

For the python files you mentioned, I don't know about the cadical script, but the others all seem like good candidates.

[Bruno Le Floch]

The find_dual file should be trivial to implement since find_equation_id knows how to make the dual of an equation. The following seems equivalent (up to some parenthesizing differences):

from find_equation_id import all_eqs
for order in range(5):
    for eq in all_eqs(order):
        dual = eq.dual()
        if eq != dual:
            print(f"| Equation{eq.id}[{eq}] | Equation{dual.id}[{dual}] |")

[Emmanuel Osalotioman Osazuwa]

Vlad Tsyrklevich said:

Neither of these scripts are used, so I'd suggest closing this instead of spending the time to check that the resulting changes work correctly

I have closed the pr since the scripts are no longer used. I will make sure to check where scripts are being used before making changes next time.

Since the scripts are no longer being used though, could we remove them from the project?

I could remove them on my next pr while working on the other scripts that need find_equation_id.py if needed, what do you think?

[Shreyas Srinivas]

Quick question: why are we porting existing and functional scripts to other languages?

[Shreyas Srinivas]

Especially at this late stage

[Shreyas Srinivas]

Also, leaving aside the question of rewriting stuff that has worked well, porting anything from python to ruby appears to be a strict downgrade from my perspective since python is a much more widely known language

[Shreyas Srinivas]

And no we shouldn’t remove scripts that are no longer used, if they were used during the project. This is not an industrial codebase. We need to keep track of what we did and how we did it. We should be able to look back and give decent answers to questions that might come up 10 years from now

[Bruno Le Floch]

A JavaScript version of find_equation_id.py would be useful because it would allow the Equation Explorer (I think it's written in JavaScript?) to show higher-order equation, for which we have some commentary. For ruby, I have no strong opinion. No opinion either on updating old scripts.

[Shreyas Srinivas]

Then the JavaScript version makes sense. The ruby version needs a good reason. And we do not want to delete any scripts please.

[Emmanuel Osalotioman Osazuwa]

Shreyas Srinivas said:

Quick question: why are we porting existing and functional scripts to other languages?

Especially at this late stage

I think this issue Update scripts to use Bruno's equation numbering code will give more insight into that.

[Emmanuel Osalotioman Osazuwa]

Shreyas Srinivas said:

Also, leaving aside the question of rewriting stuff that has worked well, porting anything from python to ruby appears to be a strict downgrade from my perspective since python is a much more widely known language

I won't really say its a downgrade since the ruby code does not replace something the python code was already doing.

[Emmanuel Osalotioman Osazuwa]

Shreyas Srinivas said:

And no we shouldn’t remove scripts that are no longer used, if they were used during the project. This is not an industrial codebase. We need to keep track of what we did and how we did it. We should be able to look back and give decent answers to questions that might come up 10 years from now

Removing scripts that are no longer in use now does not stop people 10 years from now from seeing those scripts as GitHub keeps a snapshot of everything on every commit. I'm not against removing/leaving them though, it was just a suggestion so our focus is only on things that are actually being used in the project.

[Shreyas Srinivas]

I still think we should leave the scripts we used to track progress in our project as it is.

[Shreyas Srinivas]

I can see the benefit of not parsing lean code to extract equation numbers. We can have both scripts in place. Do put a comment on top of both files explaining why there are two of them, which of them is currently being used, why the switch etc.

[Shreyas Srinivas]

It is true that github will store snapshots forever, but searching through them, even with git blame is tedious.

[Emmanuel Osalotioman Osazuwa]

Okay