The MagmaEgg example figure is truncated

Stream: Equational

[Bruno Le Floch]

The figure magma-egg-example.png, that we use in Figure 11 in the paper, is truncated and ends with (T (T h6 (h v7 v1 v0)) (C (C (R v1) instead of continuing on for one more line. The details of this expression are not very useful, but I think it is jarring for the reader that the proof is cut short in such a clear way. I cannot regenerate this figure with the same color scheme. Can someone regenerate it, perhaps @Marcus Rossel who seems to have generated the initial version?

[Emmanuel Osalotioman Osazuwa]

Does this work?:

magma-egg-example.png

https://github.com/teorth/equational_theories/pull/1402

[Emmanuel Osalotioman Osazuwa]

My font is a little bit off with the l character, trying to see if I can fix it.

[Bruno Le Floch]

Thanks! In your PR, maybe make the resolution better? It got basically halved by your change, which might be too much, I'm not sure.

The font is not a problem. If we want consistency between Figures 10 and 11, we could change Figure 10 (vampire-example.png) to your font as well; please decide whether to include it in your PR (the Lean source code is at the end of equational_theories/Generated/VampireProven/Proofs13.lean).

Since we're updating figures, can you also include the new Equation Explorer screenshot to replace GUI-equation-explorer.png (Figure 16)? I double-checked all the statements in that commentary.

[Emmanuel Osalotioman Osazuwa]

Yes, I tried finding the vscode theme @Marcus Rossel used, but I couldn't seem to find the right one, so I used a python script to generate the image instead.
The width and height were automatically calculated based on other factors, trying to get the width and height to be set at the top of the script so other factors can be calculated from it instead now.

I think it would be nice to have consistent font.

Yes, I'll add the updated GUI-equation-explorer.png photo.

[Emmanuel Osalotioman Osazuwa]

I'v updated the PR so the image has the same resolution as the previous one.

[Emmanuel Osalotioman Osazuwa]

I'll add the other changes in a bit.

[Emmanuel Osalotioman Osazuwa]

The font adjustment seems to have worked as the new image font looks close to what was previously there, so I don't think there will be any need to update vampire-example.png, unless you feel there is need to, then I can include it in my PR.

[Bruno Le Floch]

I think it's find not to change vampire-example.png since it is on a different page anyways. In any case we also have inconsistencies with Figure 5 and 6 whose contents are similar to the two figures we are discussing.

[Emmanuel Osalotioman Osazuwa]

I've pushed all the changes, you can go through the PR again now:

https://github.com/teorth/equational_theories/pull/1402

I put in a complete image of the page for GUI-equation-explorer.png instead of a truncated one.

[Marcus Rossel]

Hey, sorry for the delayed response. The images I had used for the figures were just screenshots of Github's file view. I think the best option would be to use the latex minted package to format code, as there are also code examples in Section 3 which currently do not look too nice. I'll post a PR for that.

[Bruno Le Floch]

Thanks. No rush though, as this will be for a second version of the paper.

[Marcus Rossel]

https://github.com/teorth/equational_theories/pull/1406