Equation explorer data errors?

Stream: Equational

[Amir Livne Bar-on]

The page for equation 1167
https://teorth.github.io/equational_theories/implications/?1167
shows the wrong equation: x = y ◇ ((z ◇ (y ◇ y)) ◇ y) is actually 1168. and other pages with nearby numbers are off by one too.

[Pace Nielsen]

Also, Equation 1490 is missing (and 1491 seems to off too).

[Vlad Tsyrklevich]

I did a manual binary search and it seems to have a off-by-one starting at 953 (not 952 though), which is odd

[Vlad Tsyrklevich]

This data error seems recent, https://teorth.github.io/equational_theories/implications/implications.js has Equation953 being wrong but it's not wrong on my locally generated copy

[Vlad Tsyrklevich]

OK, scripts/generate_equation_implication_js.py does a poor job of parsing Equations.lean (it doesn't pull out the number, just does it sequentially) and https://github.com/teorth/equational_theories/commit/2f8911375cff8898e6b9ef51cefbc250dbfad95c deletes something from Equations.lean which we should never do

[Vlad Tsyrklevich]

cc @Andrés Goens Could you add back 953 to Equations.lean but commented out? We should never delete from that file (but also the parser should be improved and we should pull them out of the new auto-generated file.)

[Vlad Tsyrklevich]

I have to run to get my day started or I'd do it myself

[Andrés Goens]

sorry, I wasn't aware of the comments hack

[Andrés Goens]

I'm not on a computer right now so I can't duo it either, but I wonder if this should be coordinated/fixed with equational#472?

[Andrés Goens]

but otherwise we can merge the PR equational#481 as a hotfix

[Vlad Tsyrklevich]

Ah I hadn't seen that Carlini had already found and PRd this