Gauss summation rendering

[thery]

In the paper Untangling Mechanized Proofs there is some nice math rendering for the proof of Gauss. How is it possible to build this locally? I've found the file hyps.rst but don't know which incantation is needed in order to produce the nice outout.

[cpitclaudel]

The source of the example used in the paper is here: https://alectryon-paper.github.io/snippets/nsum-gauss.rst The rendering is here: https://alectryon-paper.github.io/snippets/nsum-gauss.html

I pushed a simplified standalone version here: https://raw.githubusercontent.com/cpitclaudel/alectryon/master/recipes/mathjax.rst ; does it work for you?

[thery]

does it work for you?

Yep :+1:

Then, we add notations to print LaTeX code (this is only one way to do it; another way would be to parse Coq's output to reconstruct LaTeX)

is there somewhere I can find an example of this?

[thery]

Tried the Notation version on an example of mathcomp that uses binomial, product, summation and polynomial : It looks really good I think : digit :smile: Still I had some problems

• some formulae go outside the box.
• many theorems of mathcomp use "_" as a separator. So I had to write lots of trivial notation so that "_" is understood as subscript in latex
• I don't know how to render variable p1, p2 as p_1 p_2.

Is there something that can be done?

[cpitclaudel]

Incredible, that looks awesome!

some formulae go outside the box.

https://docs.mathjax.org/en/latest/output/linebreaks.html says that MathJax 3 doesn't yet support automatic line breaks, but I think MathJax 2 does — maybe we should try that? See also https://github.com/mathjax/MathJax/issues/2312

many theorems of mathcomp use "" as a separator. So I had to write lots of trivial notation so that "" is understood as subscript in latex

I think you might be able to do that post-processing in javascript of python, without using notations — maybe? I did something like that before to add space between the variables in a forall:

        spans.forEach(function (e) {
            var text = e.innerText; // ← Arbitrary transformations here on innerText
            var node = document.createTextNode('\\[' + text + '\\]');
            e.parentNode.replaceChild(node, e);
        });

I don't know how to render variable p1, p2 as p_1 p_2.

Do you mean in the code or in the rendered math? My best guess would be JS post-processing or Python post-processing.

[cpitclaudel]

is there somewhere I can find an example of this?

Not yet, no (well, maybe the example with the game of life, which does trivial parsing to split a list of board states; I've been working on it for separation logic proofs.

[thery]

Thanks,

I've managed to somewhat reduce the overboxing by adding a newline when displaying a forall. For the post-processing, too difficult for me as I don't know much the technology.

Thanks again

[cpitclaudel]

Happy to look into the post-processing — can you give me a concrete example so I know exactly what to look for? Thanks for the cool experiments!

[thery]

In the theorems of fp.rst i would like variables like p1 and p2 to be p₁ and p₂