Structured Typesetting

[Thierry Arnoux]

Hi all,

I see from previous posts that Norm is especially careful about the
typesetting and representation of the Metamath language.
In order to be even nearer to representations mathematicians are
familiar with, I've been experimenting with MathML. Here are some results:
http://arnoux.ch/thierry/metamath/mathml/cubic.html
http://arnoux.ch/thierry/metamath/mathml/0.999....html
http://arnoux.ch/thierry/metamath/mathml/itgparts.html
http://arnoux.ch/thierry/metamath/mathml/wallispi.html
http://arnoux.ch/thierry/metamath/mathml/arisum2.html
(If everything goes well, in those pages, MathJax shall take the MathML
provided and display it in SVG, even in browsers which don't support MathML)

Unlike current type settings (LaTEX, Gif HTML and Unicode-HTML) which
translate statements token by token, I'm matching the structure of the
statements - they can be viewed as a tree - against a list of schemes,
and apply substitutions. This allows for complex schemes, and may also,
with the correct schemes, allow for precedence rules to remove
unnecessary brackets.

This is still a work in progress and even in these few examples there
are still some mistakes I need to fix. If you're curious, I can share
the code (still buggy); I also attach the list of rules I've applied -
which also still needs refining. Right now brackets are sometimes still
missing (e.g. for powers of fractions).

I originally had the fear that this representation might hide too many
of the internal proof steps (like e.g. for associativity), but right
now, and for the examples I've taken, it does not seem it's the case.
_
Thierry

[David A. Wheeler]

On Mon, 17 Jul 2017 02:51:37 +0800, Thierry Arnoux <thierry...@gmx.net> wrote:
> ... In order to be even nearer to representations mathematicians are

> familiar with, I've been experimenting with MathML. Here are some results:
> http://arnoux.ch/thierry/metamath/mathml/cubic.html

I find the expressions themselves to be rather pretty. On Firefox there are a number
of problems (overly tall/wide cells), but I presume those are just problems from an
incomplete experiment & can be fixed.

It'd take a bit of work to do a good job
with this, but it is an interesting experiment.

> This is still a work in progress and even in these few examples there
> are still some mistakes I need to fix. If you're curious, I can share

> the code (still buggy); ...

We'll want to find a way to have high confidence in the display.
Ways to make the rules simple & "obviously correct" would help.

> I originally had the fear that this representation might hide too many
> of the internal proof steps (like e.g. for associativity), but right
> now, and for the examples I've taken, it does not seem it's the case.

I worry about that too. As long as you're just reformatting that shouldn't happen.
Replacing (...) is also okay *if* it's replaced with another visual cue (e.g., horizontal
fraction lines that also provide grouping), but if it usually just represents
information in a 1-to-1 way it shouldn't be a problem.

We could also make the "GIF" version the more direct mapping,
and the "Unicode" the "pretty" version that also uses MathML.
Then someone could select "GIF" to ensure that they see a more direct mapping.

--- David A. Wheeler

[Mario Carneiro]

On Sun, Jul 16, 2017 at 8:16 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Mon, 17 Jul 2017 02:51:37 +0800, Thierry Arnoux <thierry...@gmx.net> wrote:
> ... In order to be even nearer to representations mathematicians are
> familiar with, I've been experimenting with MathML. Here are some results:
>      http://arnoux.ch/thierry/metamath/mathml/cubic.html

I find the expressions themselves to be rather pretty.  On Firefox there are a number
of problems (overly tall/wide cells), but I presume those are just problems from an
incomplete experiment & can be fixed.

It'd take a bit of work to do a good job
with this, but it is an interesting experiment.

> This is still a work in progress and even in these few examples there
> are still some mistakes I need to fix. If you're curious, I can share
> the code (still buggy); ...

We'll want to find a way to have high confidence in the display.
Ways to make the rules simple & "obviously correct" would help.

> I originally had the fear that this representation might hide too many
> of the internal proof steps (like e.g. for associativity), but right
> now, and for the examples I've taken, it does not seem it's the case.

I worry about that too.  As long as you're just reformatting that shouldn't happen.
Replacing (...) is also okay *if* it's replaced with another visual cue (e.g., horizontal
fraction lines that also provide grouping), but if it usually just represents
information in a 1-to-1 way it shouldn't be a problem.

I'm willing to compromise on this (1-to-1 mapping) in edge cases. For presentation, nice display trumps unambiguity - we always have the other display methods available if users want a more precise readout. That said, I don't see any cases in the examples where ambiguity could potentially be a problem. For associativity, the usual way to solve the problem is to have a defined precedence and associativity for each operator, so (a+b)+c is printed as a+b+c and a+(b+c) is printed as is.

Mario

[Mario Carneiro]

Overall, I'm very pleased with this test, and I think the general approach is sound. The time taken to render MathJax is a major limitation, though - Metamath web pages often contain 800+ formulas, and it takes almost 30 seconds to render the test pages on my browser.

I think a proper precedence printer is needed to get the parentheses right, though, for example in cases like (sin x)^n which is printed ambiguously without parentheses, or all the various combinations of + - x. / . The printer needs to parse the math expression (as mmj2 does) to get a syntax tree, then render each node using a table like the .mmts file you've given, and insert parentheses (which are formatted with a special parenthesis entry in the table) whenever the precedence requires it.

Thierry

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[David A. Wheeler]

On Sun, 16 Jul 2017 22:02:50 +0100, Mario Carneiro <di....@gmail.com> wrote:
> I think a proper precedence printer is needed to get the parentheses right...

I don't agree.

I earlier cited the paper “Developer beliefs about binary operator precedence (part 1)”
by Derek M. Jones: http://www.knosof.co.uk/cbook/accu06.html
This paper showed that professional programmers often don't use and
don't understand precedence. A display mechanism shouldn't assume humans
correctly and reliably follow precedence rules, because many do not.
Humans are annoying creatures; they aren't very good at being precise :-).

I think it would be better to always include the source parentheses *except*
in narrow specific conditions where they would be omitted. That's the opposite
of inserting them only when required. Call those places
"auto-grouping" locations:
* When using a horizontal line, there is auto-grouping of the top & of the bottom
* When exponentiating, the exponentiated expression (above) is auto-grouped
* In a root, the two areas (root and inversed exponent) are auto-grouped
* When moving to a special location (e.g., sum's first expression), it's auto-grouped
* when the same operator is used, maybe you can assume left-to-right, so
( ( A F B ) F C ) can instead be shown as ( A F B F C ).
I realize that exponentiation is often right-to-left, but if that's handled separately,
then that's not a problem.
* I can imagine that a few special cases of precedence might make sense, e.g.,
x. over +. But they should be few; even professional programmers often
get "obvious" precedence rules wrong. I would suggest that x. over + or -
should be the only ones to start with.

Most of the visual improvement from the test appears to me to be based on
the use of superscripts, subscripts, fraction bars, and root bars - not from
precedence.

--- David A. Wheeler

[Mario Carneiro]

On Sun, Jul 16, 2017 at 10:36 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Sun, 16 Jul 2017 22:02:50 +0100, Mario Carneiro <di....@gmail.com> wrote:
> I think a proper precedence printer is needed to get the parentheses right...

I don't agree.

I earlier cited the paper “Developer beliefs about binary operator precedence (part 1)”
by Derek M. Jones: http://www.knosof.co.uk/cbook/accu06.html
This paper showed that professional programmers often don't use and
don't understand precedence.  A display mechanism shouldn't assume humans
correctly and reliably follow precedence rules, because many do not.
Humans are annoying creatures; they aren't very good at being precise :-).

I don't buy this argument. Within mathematics, there is a well-established precedence relation for all the common arithmetic operators. The question is whether this generalizes to the rest of metamath without undue memorization stress. I very much doubt we need the 30-some precedence classes used in C, probably 10 or fewer should do the job, even though there are many more operators in Metamath. I will try to break down all the infix and prefix operators in Metamath in a later email to make this a concrete proposal, but for now note that the more esoteric binary operators are best notated by the form Func(x, y) instead of (x Func y), and also for many operators we can set them in "always paren" mode, where disambiguating parentheses are always inserted against any other binop, or any binop in a precedence range.

I don't think we are really disagreeing; I am referring to the algorithm structure, not the result, which may very well have a good deal of parens. But there are some very common binop clashes which will clear up a lot of parens, specifically (written in decreasing precedence order):

function application, specialized ops (using explicit parens around arguments)

^ (always paren ^ against itself)

-u

x. / are left assoc (always paren / against itself)
+ - are left assoc

wff binops

-.

/\, \/ are left assoc (always paren /\ against \/ )

<-> is left assoc

-> is right assoc

There are probably a few more I'm missing, but this should eliminate almost all parens in usual metamath deductions. Yes, it requires some getting used to (even the missing outer parens in the test files was a bit jarring for me), but I think the result will be worth it. Do you have any specific binop pairs in the above list that you think will often be misinterpreted?

Mario

[Mario Carneiro]

One small amendment to that table: -u should always use parens against ^ . If ^ is notated with superscript, this is not as big a deal, but if it is a linear format then -a^b will require too much of the reader to parse correctly.

[David A. Wheeler]

On Mon, 17 Jul 2017 00:44:03 +0100, Mario Carneiro <di....@gmail.com> wrote:
> One small amendment to that table: -u should always use parens against ^ .
> If ^ is notated with superscript, this is not as big a deal, but if it is a
> linear format then -a^b will require too much of the reader to parse
> correctly.

It's not just "too much"; there are disagreements about precedence between systems, and people are often unaware that there are differences.

All spreadsheet programs that I know of do unary "-" *before* exponentiation, including Microsoft Excel and LibreOffice Calc. E.G., put "-1" in cell A1, then in cell A2 calculate =-A1^2. Result: 1. This is *required* by the OpenDocument OpenFormula specification, for example.

The reverse is true for many programming languages. Let's try Python (for example):
a = -1
print (-a**2)
The printed result will be -1.
The same is true for Ruby.

--- David A. Wheeler

[David A. Wheeler]

On Mon, 17 Jul 2017 00:30:31 +0100, Mario Carneiro <di....@gmail.com> wrote:
> I don't buy this argument. Within mathematics, there is a well-established
> precedence relation for all the common arithmetic operators.

It's absolutely true that there's a well-established precedence relation.

But many people don't *correctly* understand them, so I think the use of
precedence should be greatly limited. Particularly if you want a larger readership.

David Hilbert remarked on August 8, 1900:
An old French mathematician said: ‘A mathematical theory is not to
be considered complete until you have made it so clear that you can
explain it to the first man whom you meet on the street.’
http://www.sciencedirect.com/science/article/pii/S0315086016300465

Hidden rules such as precedence rules can *inhibit* clear reading of an
expression's meaning.

> I don't think we are really disagreeing; I am referring to the algorithm
> structure, not the result, which may very well have a good deal of parens.

Fair enough, I'm focusing on the final result.

> x. / are left assoc (always paren / against itself)
> + - are left assoc

I think x. having higher precedence than + and - is the "most safe".
However, a nontrivial number of programmers do *not* know this rule,
and it gets *worse* the further you stray from this.

> -> is right assoc

Would this be automatically widely *understood*? I have my doubts.
It's safer to parenthesize.

> There are probably a few more I'm missing, but this should eliminate almost
> all parens in usual metamath deductions.

The goal shouldn't be to minimize parens, the goal should be to maximize clarity.

I suggest starting with parens in most cases, then *slowly* removing ones
when it's obvious removing them isn't interfering with understanding.
If there's doubt, parenthesize.

--- David A. Wheeler

[Mario Carneiro]

In the logical arena, I don't think I can compromise on at least /\ left assoc, higher precedence than -> right assoc. These are essential for making prop calc sane and are universal conventions (among books that formalize logic to begin with). Remember, I'm not talking about programming conventions at all. (However, it's worth noting that if you have ever done type theory or Haskell / functional programming, you will be very familiar with -> as a right assoc operator.) Furthermore, there is no reason we can't make precedence information easily accessible, similar to the "syntax hints" in the current HTML.

I am fine with introducing mandatory parens whenever there is any significant disagreement about some precedence relation (as in the -u vs ^ case), but there needs to be an *actual* disagreement with some kind of reference, not some vague worry of confused users that haven't been taught any symbolic math. Let's face it: Metamath is really heavy on symbolic notation for math, and the reader *needs to learn it* to read it. We can make it easy for them to learn, but we should be aiming for something that an experienced mathematician with no Metamath training should be able to understand.

Mario

--- David A. Wheeler

[David A. Wheeler]

On Mon, 17 Jul 2017 02:25:04 +0100, Mario Carneiro <di....@gmail.com> wrote:
> In the logical arena, I don't think I can compromise on at least /\ left
> assoc, higher precedence than -> right assoc. These are essential for
> making prop calc sane and are universal conventions (among books that
> formalize logic to begin with).

Sure, I can buy that. Note the reasoning though: These are essentially
universally agreed on *AND* using them has significant benefits for a large
number of expressions. I think those are good criteria.

> Remember, I'm not talking about programming
> conventions at all. (However, it's worth noting that if you have ever done
> type theory or Haskell / functional programming, you will be very familiar
> with -> as a right assoc operator.)

I have done Haskell & functional programming, so I'm familiar with it.
My concern is with everyone else, not me personally.

...

> I am fine with introducing mandatory parens whenever there is any
> significant disagreement about some precedence relation (as in the -u vs ^

> case), but there needs to be an *actual* disagreement ...

I'm concerned about turning this into something like the C extravaganza
where there are ~15 different precedence levels, and in addition,
many levels have many operations. Ugh.

Every precedence rule has a significant mental cost for humans. Those
costs should only be paid when there are very significant benefits
that exceeds the costs. Professional programmers avoid using
many precedence rules, and while that's not exactly the same user group,
it does hint that overuse of precedence rules can lead to many problems.

I think it's better to have a *limited* number of precedence rules where they are
(1) clearly agreed on AND (2) clearly helpful in simplifying a large number of expressions.
I think a good way to get there is to start with a very short list, and only grow it
when a clear benefit is demonstrated. That reduces the risk of gratuitously adding
to the list.

--- David A. Wheeler

[Thierry Arnoux]

Thanks for your encouraging comments!

I've reworked the solution, and I now have something to submit for integration into the metamath program, if we are willing to go in that direction (probably still to be mentioned as experimental, though!).
Attached is the new source code, as a patch to be applied on top of the "0.146 26-Jun-2017" version, including also new source and header files and the current typesetting file.
(is that the right format / the right way to submit a patch for the metamath program?)

Proofs can be exported in MathML format by using e.g. command "SHOW STATEMENT iunid / STS mathml" after having loaded "set.mm".

A concern could be the size of the generated files, as MathML is probably much more verbose than current HTML. Is that an issue? One solution could be to switch to TeX, which would probably be more compact but result in the same output.

On that basis, I will continue on the typesetting definition.

I think a proper precedence printer is needed to get the parentheses right, though, for example in cases like (sin x)^n which is printed ambiguously without parentheses, or all the various combinations of + - x. / . The printer needs to parse the math expression (as mmj2 does) to get a syntax tree, then render each node using a table like the .mmts file you've given, and insert parentheses (which are formatted with a special parenthesis entry in the table) whenever the precedence requires it.

About notation conventions like order of precedence: I think ideally, we should identify an authoritative academic source and refer to it. I found online some editing style guide from the AMS, but those are targeted at editors and only one actually addressed precedence, from the APS. Can anyone recommend such a reference specifically for mathematics?

Here are the references I found on formatting mathematics:

http://forms.aps.org/author/styleguide.pdf (Chapter D. about bracketing, E.)

http://www.ams.org/publications/authors/AMS-StyleGuide-print.pdf
https://www.siam.org/journals/pdf/stylemanual.pdf
http://dlmf.nist.gov/front/introduction
http://dlmf.nist.gov/not/

Your example about (sin x)^n is interesting, though. I think the commonly accepted notation in this case is sin^n x (with n as a superscript of "sin"). It would be easy to add a special rule for this case, and to render e.g. ~ sincossq that way.

Overall, I'm very pleased with this test, and I think the general approach is sound. The time taken to render MathJax is a major limitation, though - Metamath web pages often contain 800+ formulas, and it takes almost 30 seconds to render the test pages on my browser.

About display time: we could e.g. hide proof steps beyond a given depth or length. This would both solve the issue of display time and page size (MathML is quite verbose). This restriction could then be removed in the future when speed and space are cheaper. There are also ways to let MathJax render smaller chunks of MathML code. Yet another option could be to initially hide some proof steps behind a [+] and render them only when the user clicks on it.

I originally had the fear that this representation might hide too many of the internal proof steps (like e.g. for associativity), but right now, and for the examples I've taken, it does not seem it's the case.

I worry about that too.  As long as you're just reformatting that shouldn't happen. Replacing (...) is also okay *if* it's replaced with another visual cue (e.g., horizontal fraction lines that also provide grouping), but if it usually just represents information in a 1-to-1 way it shouldn't be a problem.

I'm willing to compromise on this (1-to-1 mapping) in edge cases. For presentation, nice display trumps unambiguity - we always have the other display methods available if users want a more precise readout. That said, I don't see any cases in the examples where ambiguity could potentially be a problem. For associativity, the usual way to solve the problem is to have a defined precedence and associativity for each operator, so (a+b)+c is printed as a+b+c and a+(b+c) is printed as is.

Shall we add a word of warning on generated pages, like "note that while this representation was translated from Metamath data, there is no one-to-one mapping and the internal Metamath representation may differ significantly." ?

I find the expressions themselves to be rather pretty.  On Firefox there are a number of problems (overly tall/wide cells), but I presume those are just problems from an incomplete experiment & can be fixed.

Things like cell margins can indeed be tuned. I actually like the comfort of the cells as displayed currently, with more spacing, but that could be reduced. Or did you see a specific formula incorrectly displayed ?

Also, the formulas are currently represented centered (like it is the convention for formulas not displayed inline). Shall I adapt back to left-aligned, so that the formulas as intended according to the proof depth?

[Norman Megill]

Thanks.  I will be reviewing your patch over the next few days.

Norm

[Thierry Arnoux]

Thank you Norm!

All, concerning the typesettings:

• Symbols like indexed union U_, indexed intersections I^I , and disjointedness of an indexed collection Disj_ are written with an underline in the "linear" HTML version. Can I remove it in the MathML version, since the x e. A that immediately follows is written as a subscript, and there is no confusion? If so, I could actually even write the x e. A under the symbol and not as a subscript.
  http://arnoux.ch/thierry/metamath/mathml/iundisj.html
  
• I chose to write the complex conjugate ( * ` X ) as a bar over the expression, as this is the standard in mathematics. Any disagreement?
  http://arnoux.ch/thierry/metamath/mathml/cjth.html
  
• For normal function value ( F ` X ), I display F(X). What shall I display for ( F " A ), the image of a set? I see one convention used in Wikipedia is F[A]. Ok to use it? Otherwise, I could use bold brackets to make the difference - but that difference is actually hard to see:
  http://arnoux.ch/thierry/metamath/mathml/dfco2a.html
  

Norm, for the code itself:

• I've chosen to read the input file from an external file, but we could very well include the information inside of a set.mm $t section if you prefer.
• Other math fragments (in comments, in distinct variable list) shall probably be displayed as althtml, since the "STS" method requires to know the type of the math fragment (wff, class..) and that information is not available. Or maybe it could be inferred by trial and error for comments?
  
• The "No typesetting found" message displayed in case of error shall be plain HTML: no need to involve MathML like now - but that's minor.
• I realize the way I allocate the nmbrString buffers for varPos, varStart, varLen is not standard in metamath.exe. Shall I change them for pool allocations (nmbrSpace) ?
• I shall have replaced the "switch(varCount)" by an if statement - looks like I forgot.
• I will have to change the formatting so that I stay within the 80 char per line limit - no problem with that!

_
Thierry

[Mario Carneiro]

On Sun, Jul 23, 2017 at 2:19 PM, Thierry Arnoux <thierry...@gmx.net> wrote:

Thank you Norm!

All, concerning the typesettings:

• Symbols like indexed union U_, indexed intersections I^I , and disjointedness of an indexed collection Disj_ are written with an underline in the "linear" HTML version. Can I remove it in the MathML version, since the x e. A that immediately follows is written as a subscript, and there is no confusion? If so, I could actually even write the x e. A under the symbol and not as a subscript.
  http://arnoux.ch/thierry/metamath/mathml/iundisj.html
  

Absolutely. I don't know whether subscript or underscript placement will look better in most cases; you may just have to play with the settings to find out.

• I chose to write the complex conjugate ( * ` X ) as a bar over the expression, as this is the standard in mathematics. Any disagreement?
  http://arnoux.ch/thierry/metamath/mathml/cjth.html

 An alternative is a superscript *, but both notations suffer some ambiguity with other notations in math. (The overline is also used for closure and complement, and the postfix star is used for the Kleene star operation.) I'm fine with either one.

• For normal function value ( F ` X ), I display F(X). What shall I display for ( F " A ), the image of a set? I see one convention used in Wikipedia is F[A]. Ok to use it? Otherwise, I could use bold brackets to make the difference - but that difference is actually hard to see:
  http://arnoux.ch/thierry/metamath/mathml/dfco2a.html

The F[A] notation seems fine to me.

Mario

[Thierry Arnoux]

I've updated the preview with what it looks like with these changes:

    http://arnoux.ch/thierry/metamath/mathml/iundisj.html
    http://arnoux.ch/thierry/metamath/mathml/dfco2a.html

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

[David A. Wheeler]

On Mon, 24 Jul 2017 01:53:46 +0800, Thierry Arnoux <thierry...@gmx.net> wrote:
> I've updated the preview with what it looks like with these changes:
>
> http://arnoux.ch/thierry/metamath/mathml/iundisj.html

I get too much vertical empty space, and the sizes of some symbols don't seem
to work well with others. I've sent you an image so you can see the details.
That said, I think the overall direction looks nice & quite promising.
(I suspect the vertical height just requires a CSS tweak.)

I do ask that you strive to make the final generated display
unambiguous. In a few cases standard math notation is ambiguous.
Since the whole point here is to be rigorous, I think it'd be better
to tweak the notation as necessary to stay unambiguous.

--- David A. Wheeler

[Thierry Arnoux]

Hi David,

Yes, the spacing can be removed by tweaking CSS, here's my go at it:

http://arnoux.ch/thierry/metamath/mathml/uniioombllem4.html

I actually still prefer the version with more space (and regular line height), but I guess that's really a matter of personal preference!

As a matter of typesetting rules, there are two official ways to display math in a document: either inline/within text, or displayed as a separated line, e.g. a numbered equation. The first way (inline), is more compact and e.g. the under/over notation in summations become subscript/superscript, and fractions are written as a solidus (with a slash) / . (see for example the APS guideline, chapter E.2.). The second way (displayed) takes up more space above and below the equations. MathML/MathJax support both of those, and I initially chose to display the proof steps in the second way, as a block. The space and centering was added automatically by the tool as by standard.

I think it's clear that any math fragment added in the comment part (in between ` `) shall be displayed inline.

Then the question is whether we shall consider our proofs as "inline" too, or as "displayed", or if we define something in between. Indeed in the guidelines, it is stated that only the most important equations shall be displayed (cf. APS guideline chapter C.1.). In our proofs we actually may list hundred of them - but we number each of them.

As for your second remark, I definitively want to make the final display unambiguous. I shall e.g. keep the brackets in (-A)^B, since there is a discussion about it (e.g. in http://arnoux.ch/thierry/metamath/mathml/logtayl2.html). I currently remove brackets when there are already visual hints (below a square root sign, under/over a fraction bar, under/over a summation, within a F(X) function value, in singletons { X }, pairs, triplets, etc.), and where well-known order of precedence rules apply (that's actually only necessary in the case of multiplication over addition).

There are at least two points I need to work on:

• brackets around fractions : I keep them by default, but in most cases they can be removed.
  
• the form ( ( F ` X ) ^ Y ) is still displayed F(X)^Y which wrongly lets you think only X is put to the power of Y (as noted by Mario). I could either display F^Y(X) as a notation convention (like in sin^2), or keep brackets. The second is probably the better alternative.
  

_
Thierry

[David A. Wheeler]

On Mon, 24 Jul 2017 12:07:37 +0800, Thierry Arnoux <thierry...@gmx.net> wrote:
> Yes, the spacing can be removed by tweaking CSS, here's my go at it:
> http://arnoux.ch/thierry/metamath/mathml/uniioombllem4.html

I'm having trouble downloading that - is it still running?

> I actually still prefer the version with more space (and regular line
> height), but I guess that's really a matter of personal preference!

It's not just "preference". With all the excess vertical space
I can see less than half of the number of steps at a time.
That's awful when trying to follow a proof.

> Then the question is whether we shall consider our proofs as "inline"
> too, or as "displayed", or if we define something in between. Indeed in
> the guidelines, it is stated that only the most important equations
> shall be displayed (cf. APS guideline

> <http://forms.aps.org/author/styleguide.pdf> chapter C.1.). In our

> proofs we actually may list hundred of them - but we number each of them.

Proofs don't just show "the important equation", they show every step.
It would be good to be able to show a similar number of steps in the new
format as the current formats do, or the new format will have a serious
disadvantage compared to what we have now. So inline or "something in between"
is probably the better choice.

--- David A. Wheeler

[Norman Megill]

On Monday, July 24, 2017 at 9:36:08 AM UTC-4, David A. Wheeler wrote:

On Mon, 24 Jul 2017 12:07:37 +0800, Thierry Arnoux  wrote:
> Yes, the spacing can be removed by tweaking CSS, here's my go at it:
> http://arnoux.ch/thierry/metamath/mathml/uniioombllem4.html

I'm having trouble downloading that - is it still running?

> I actually still prefer the version with more space (and regular line
> height), but I guess that's really a matter of personal preference!

It's not just "preference".  With all the excess vertical space
I can see less than half of the number of steps at a time.
That's awful when trying to follow a proof.

I agree.  There may be a trade-off between aesthetics and usability, but I think most serious users would prefer to see as much as possible on the screen at one time.

Two other issues to think about:

1. Centering - Since the steps are centered, I often need to scroll horizontally to see them, which means I can't see the step number at the same time.  While centering is nice outside of the proof, I think the proof would be easier to follow if the steps were left-justified i.e. no extra spacing between the indentation level number and the start of the formula, like the current pages do.

2. Wrapping - The formulas don't wrap, so that the table width becomes the width of the longest proof step.  Combined with centering, this sometimes means horizontal scrolling is needed even for shorter lines, making the step numbers go off-screen. For long formulas, it means I can't see the whole formula at once.

On the existing pages, I put some effort into avoiding horizontal scroll bars even when I make the browser width very narrow.  This is convenient when I want to have several browser windows visible at once on the screen.

Norm

[Thierry Arnoux]

Hi David and Norm,

Alright, here is the page on another server:

http://metamath.tirix.org/mathml/uniioombllem4.html

This one has several experiments:

• line breaks/wraps for the math formulas (it seems to be done at nice places except for once)
  
• smaller margins around the formulas,
• lighter table cell borders but alternating row colors,
• highlighting of the antecedents (colors are too aggressive, this is just a test!)
  

I suppose this shall already improve readability, what's your opinion?

Next I'll indent the formulas left within proofs..

_
Thierry

[David A. Wheeler]

I tried this on Firefox on Android. The margins are still too big at the top and bottom of each cell. Perhaps more importantly, a lot of the symbols are assembly black rectangles, are you using web fonts? If not, you should, just like the current system does.

The load times are really large with Firefox on Android. I'm not sure if there is an easy way to optimize it, but that would be worth checking out. Perhaps you could see if an expression doesn't need MathML and generate it a different way in those cases?

--- David A.Wheeler

[Thierry Arnoux]

Hi David,

I'm using MathJax v2.7.1, which "fast preview" mode I have not been able
to deactivate yet. It tries to display the formula quickly in HTML
format
(http://docs.mathjax.org/en/latest/options/PreviewHTML.html#configure-previewhtml).
I have not tweaked the margins in that preview, they are still standard,
and it might not use Web Fonts, which would explain the black rectangles.

The final display is SVG. I've checked and found that each glyph is
actually drawn separately. Once MathML is displayed, I don't think there
can be such artifacts as black rectangles. So I assume you are viewing
the "fast preview". It might take some time until the SVG version MathML
is displayed, as pointed out by Mario.

Maybe I should switch to an alternative to MathJax, like KaTeX, which
claims to be much faster
(http://www.intmath.com/cg5/katex-mathjax-comparison.php), but does not
seem to support e.g. automatic line breaks.

I'd welcome it if you wish to contribute in any form!

_
Thierry

[David A. Wheeler]

The current MathML rendering is extremely slow. Maybe we can limit the use of MathML capabilities to only where they're actually needed, such as square root radicals. You don't need MathML for A e. B.

--- David A.Wheeler

[David A. Wheeler]

It would be worth at least checking on kaTeX. In this demo you mentioned:
http://www.intmath.com/cg5/katex-mathjax-comparison.php?processor=MathJax

It takes 65seconds to display in MathJax, and <1second in KaTeX, on Firefox on Android. Over a minute is a painfully long render time, and metamath proofs tend to have even more equations. KaTEX cannot do everything MathJax can, but it may be able to do enough.

There may also be ways to tweak MathJax invocations to be faster.

I think we need to find a way to render relatively quickly, including on mobile devices. There is no need to depend on MathML; Chrome dropped support long ago, for example, so it's not a standard actually supported by the key browsers. Everyone does support JacvaScript, so that is the key relevant standard.
--- David A.Wheeler

[Thierry Arnoux]

We sometimes have really huge pages (think mmdefinitions.html!), and I
don't want to change that, so I'll check out KaTeX.

Dave or others, if you have any other suggestions, don't hesitate!

Norm, I may do some adaptations to the program, so that it's more
flexible and loads the header/html snippets from the definition file.
You can still review what I've submitted, that core that will not change.

[David A. Wheeler]

I think prototyping some options, comparing them, and *then* selecting
them will be necessary. Basically, a mini-competition.

I think MathJax and KaTex are the main contenders.

MathJax is slow, but there are options that may dramatically improve its speed:
1. Pre-generate everything. That's what metamath does with everything else.
This, by itself, might turn MathJax from "too slow" to "works perfectly".
The final file sizes might be large, but they can be easily compressed and
blasted to the user without user-side processing. MathML is
notoriously wordy, so the pre-generated code might even be a similar or smaller
size than the current MathJax use.
2. Switch from MathML to something else. MathML is extremely wordy, slow, and
many browsers don't support it (e.g., Chrome doesn't support it, and that's about
half the users). MathML is probably at least part of the performance
problem, with no real gain. Instead, try out TeX and mark it using
<script type="math/tex">...</script>. Metamath already has a TeX generator,
and while it hasn't gotten a lot of use recently, building on it is plausible.
3. Generate something other than SVG. Is there a reason you're using SVG?
There are two other options, and SVG is not the default.
"Fast preview" is fine, but it has to be actually be fast. Waiting 10-15 minutes
for a page render is not a good thing.

A trial of KaTeX seems warranted. It's not as capable
as MathJax, but maybe that's okay. KaTeX easily supports
pre-generation. The most obvious challenge in KaTeX is that its
fractions can sometimes be cramped, but metamath proofs generally
don't involve the kind of multiple-level structures where that would be
a problem - so maybe it'll be fine.

--- David A. Wheeler

[David A. Wheeler]

> On Wed, 26 Jul 2017 23:52:31 +0800, Thierry Arnoux <thierry...@gmx.net> wrote:
> > We sometimes have really huge pages (think mmdefinitions.html!), and I
> > don't want to change that, so I'll check out KaTeX.
> > Dave or others, if you have any other suggestions, don't hesitate!

I've learned more information, which I'll share below.
I think we should prototype server-side MathJax; there are tools,
and some suggestions that it would eliminate the speed problem.

--- David A. Wheeler

The MathJax steering committee has formally declared what I
had separately observed: MathML is never going to be widely
adopted by browsers. For more information:
https://mathjax.github.io/papers/towards-v3/towards-mathjax-v3.html
http://pbelmans.ncag.info/blog/2015/12/21/on-towards-mathjax-3-0/

We *can* use MathML as intermediate format, but we shouldn't
feel constrained to do so, especially since both
MathJax and KaTeX can accept TeX format.

An obvious solution to MathJax's browser-side speed problems
is to do the rendering server-side, just like the rest of metamath's rendering.
It turns out there are tools to do just that. In particular, this library:
https://github.com/mathjax/MathJax-node
provides an API that "converts individual math expressions
(in any of MathJax's input formats) into HTML (with CSS), SVG or MathML code."
It might be easier to call from the command line, and there's
a tool for that too:
https://github.com/mathjax/mathjax-node-cli/

Here's a blog post of one person's use of this:
https://a3nm.net/blog/selfhost_mathjax.html

Some other pages:
https://github.com/mathjax/MathJax-docs/wiki/Mathjax-server-side

If it's all rendered server-side, then some other questions may become
less pressing (e.g., HTML-CSS vs. SVG generation,
MathML vs. TeX as input, etc.).

I note that arxiv.org uses MathJax, and generates math expressions
on the fly. Here's an example:
https://arxiv.org/abs/1401.3980

[David A. Wheeler]

On Wed, 26 Jul 2017 23:52:31 +0800, Thierry Arnoux <thierry...@gmx.net> wrote:

> We sometimes have really huge pages (think mmdefinitions.html!), and I
> don't want to change that, so I'll check out KaTeX.
>
> Dave or others, if you have any other suggestions, don't hesitate!

Can you send me the pages & supporting materials as a zip file?

I want to experiment with taking your existing files & pregenerating the HTML.

--- David A. Wheeler

[Thierry Arnoux]

Hi David,

KaTeX display is still work in progress, here is where I am:

• http://metamath.tirix.org/katex/uniioombllem4.html
• http://metamath.tirix.org/katex/cubic.html

There seems to be several display issues. There maybe ways to fix them, but right now the pre-rendering you propose might be the best compromise between rendering quality and display speed. I've put the project here, you'll find the .mmts translation files (there are now two of them), as well as the source C files:

http://metamath.tirix.org/Metamath.exe-170729.zip

You'll find the mathml pages in the previous directory (if you don't run mmmathml.js, you'll get the original mathml code):

• http://metamath.tirix.org/mathml/cubic.html

_
Thierry

[Thierry Arnoux]

Hi all,

I moved on with the MathJax offline rendering, using mathjax-node as described in the link provided by David.

Here is the result:

• http://metamath.tirix.org/mathml/areacirc.html (your browser does the rendering)
  
• http://metamath.tirix.org/mathml/areacirc_prerender.html (pre-rendered)
  

I think the gain is clear, the drawback being that the width of the pages is static, it does not adapt to the screen you are using to browsing with and obviously, that the time cost for rendering the pages is now server side, which multiplies the time required to generate the full set of a few tens of thousands of web pages.

This was manually generated - the next step would be to automatize the process, and recover the "no margin, left alignment" presentation.

If there is no objection, I will move on this path!

_
Thierry

[David A. Wheeler]

On September 27, 2017 9:48:54 PM EDT, Thierry Arnoux <thierry...@gmx.net> wrote:
>Hi all,
>
>I moved on with the MathJax offline rendering, using mathjax-node as
>described in the link provided by David.
>
>Here is the result:
>

> * http://metamath.tirix.org/mathml/areacirc.html (your browser does
> the rendering)
> <http://metamath.tirix.org/mathml/areacirc.html>
>* http://metamath.tirix.org/mathml/areacirc_prerender.html
>(pre-rendered)
> <http://metamath.tirix.org/mathml/areacirc_prerender.html>

>
>I think the gain is clear,

I agree. I do not even know how long the mathJax version takes to display, because after 5 minutes I gave up as being ridiculous. Even after 5 minutes it still was not displaying most of the fonts.

The second version is significantly slower than unicode, but is not hideously slow and does produce some nice results. Having actual square root radicals and such is nice.

> the drawback being that the width of the
>pages is static, it does not adapt to the screen you are using to
>browsing with

Would it be possible to pre-render just portions? When something needs to be displayed underneath a square root symbol, there needs to be some magic, but for a lot of symbols there is really nothing special about them. You could then render it just like Unicode does in many cases, and then render specially only the situations that need special rendering. That might also mean that it could be more flexible about moving things around.

I do not know if that is actually possible. But if it could be possible, that might make it work in a better way.

> and obviously, that the time cost for rendering the pages
>is now server side, which multiplies the time required to generate the
>full set of a few tens of thousands of web pages.

How much does it take per page?

>This was manually generated - the next step would be to automatize the
>process, and recover the "no margin, left alignment" presentation.
>
>If there is no objection, I will move on this path!

I think it looks very promising. This approach trades off slower rendering for a prettier rendering, but as long as it isn't too long, I suspect many people would be willing to spend a little extra time to get the prettier View.
If we can find ways to get closer to a best of all worlds, that would be even better.


--- David A.Wheeler

[Thierry Arnoux]

Hi David,

>> and obviously, that the time cost for rendering the pages
>> is now server side, which multiplies the time required to generate the
>> full set of a few tens of thousands of web pages.
> How much does it take per page?

It took 2.6s to generate the original HTML page, and then 20.6s to
pre-render it - that's for the complex ~ areacirc.
It took 1.3s to generate the original HTML page, and then 3.0s to
pre-render the proof to the intermediate ~ karatsuba.
It took 1.1s to generate the original HTML page, and then 1.7s to
pre-render the proof for the very basic ~ eqeq2i.

Assuming an average of 4.3s per page, it would still take half a day to
generate 10k pages!
Of course Metamath will not load several times its database, that part
shall be much quicker.

_
Thierry

[David A. Wheeler]

>Assuming an average of 4.3s per page, it would still take half a day to
>
>generate 10k pages!
>Of course Metamath will not load several times its database, that part
>shall be much quicker.

This is embarrassingly parallelizable though. Use 20 cpus, and it is 20x faster. I do not think that is a killer.

--- David A.Wheeler

[Thierry Arnoux]

Good!

I've now embedded the call to the external mathjax-node processing in
metamath.exe, so now the process is automated.
I'm using "popen/pclose" though, where pclose is waiting for the child
to terminate, so right now there is no parallelization at all.

I've regenerated a few of the pages:

http://metamath.tirix.org/mathml/cubic.html
http://metamath.tirix.org/mathml/areacirc.html
http://metamath.tirix.org/mathml/mmdefinitions.html

Can you check that you are fine with loading & displaying time,
margins/alignments?

_
Thierry

[David A. Wheeler]

On Mon, 2 Oct 2017 12:05:28 -0500, Thierry Arnoux <thierry...@gmx.net> wrote:
> Good!
>
> I've now embedded the call to the external mathjax-node processing in

> metamath.exe, so now the process is automatized.

> I'm using "popen/pclose" though, where pclose is waiting for the child
> to terminate, so right now there is no parallelization at all.

For testing I think that's fine. We know how to do things in parallel :-).

> I've regenerated a few of the pages:
>
> http://metamath.tirix.org/mathml/cubic.html
> http://metamath.tirix.org/mathml/areacirc.html
> http://metamath.tirix.org/mathml/mmdefinitions.html
>
> Can you check that you are fine with loading & displaying time,
> margins/alignments?

On Firefox + Windows 7, the first two look in the ballpark (if a little wide).
Around 3-4 sec time to load and display, which isn't ideal but works.
Some cleanup is needed, but the direction makes sense.
Being able to see the square root radicals over other expressions is very nice!
mmdefinitions seems overly wide, and has a number of problems, e.g.:
wcel 1684 No typesetting for: wff A e. B

Of course, mobile is more challenging.
I tried on Firefox on Android.
cubic.html first displays in 8sec, and mmdefinitions in 11sec.
That is a very long wait, and that's over Wifi (cell would be worse).
The margins are crazy; you can't read the text
if you zoom out enough to see a whole line. A narrow point:
Something is wrong with csb;
the underlined square brackets aren't getting generated correctly.

This is definitely progress, but there are still some problems.

I think you need to find a way to let this be generated
progressively; it currently appears to require the browser to load
the whole page, determine sizes for the whole page, and *then* finally render.
For the *vast* majority of expressions you don't need this at all.
Again, is there any way to specially typeset only a *subset* and wrap that
in less than a full screen?

--- David A. Wheeler

[Benoit]

That looks very nice.
It appears that the delimiters after vol and vol* are not extensible (I mean, the opening one for instance is "(" instead of the latex "\left(" ). Also, for the empty set, \varnothing looks better than \emptyset.

I really like the coloring of the proof step and the steps it uses when you hover over it. Maybe you could add a third color for the proof steps that use it.

--
Benoit

[Thierry Arnoux]

Thanks for the feedback Benoît!

> That looks very nice.
> It appears that the delimiters after vol and vol* are not extensible
> (I mean, the opening one for instance is "(" instead of the latex
> "\left(" ).

I think I found this online and proactively configured the fences for
function application as "not-stretchy" to distinguish them from the
"grouping" parenthesis. I'll just remove it so all parenthesis are going
to stretch.

> Also, for the empty set, \varnothing looks better than \emptyset.

Yes! I also believe so!
Unfortunately it seems that these are actually just variants of the same
glyph and MathML does not see the difference, so I cannot choose which
one to render. See this:
http://lists.w3.org/Archives/Public/www-math/2004Apr/0007.html
See also this interesting answer:
https://math.stackexchange.com/questions/184943/which-symbol-should-be-used-for-an-empty-set

I'll keep this like it is for now, but if I find time I'll try to change it.

> I really like the coloring of the proof step and the steps it uses
> when you hover over it. Maybe you could add a third color for the
> proof steps that use it.

That's a done thing now!
A new version is online with those changes.

[Thierry Arnoux]

One small hack later, the empty set symbol now looks just like on my
teacher's blackboard!

[Benoit]

That looks better.

I don't see any change for the coloring? What I meant is: also color the step(s) that use the set that is hovered over.

As for symbols:
- for the universal class, I would prefer the standard V used in mpeuni (\mathbb{V} often denotes a vector space), and similarly for _E and _I
- for functions, I would use \longrightarrow (since \rightarrow is used for implication), and similarly \longmapsto
- like David, I see problems for wceq and wcel
-several formulas (in mmdefinitions) are display on several lines for no apparent reasons: inferences with & and =>, but also df-oi, df-cnf or ax-ac2 for instance.

How do you decide on the symbol? Is it an automatic extraction from the htmldef or texdef of set.mm? I ask this because it would be best to keep them synchronized, in case some set.mm symbols change.

[Thierry Arnoux]

Hi Benoît,

Coloring is there for both dependents and antecedents - maybe you shall just actively reload the page (or simply reload http://metamath.tirix.org/hant.js) to get it?

I've done the changes for ` _V ` (you are right about its usage), for _E, _I and for the arrows. You may reload the pages to check if it's Ok for you now.

For wceq and wcel, in the mmdefinitions.html page, I need more time to understand what's going on. I may have to add rules especially for the mmdefinitions.html page, since actually equality and elementhood are correctly displayed everywhere else!

I'll try to understand what is wrong with line breaks. I guess this may have to do with the "N-ary times operator", ⨉, present in df-prds, which does not break correctly.

I've been trying to stick to the same symbols as in the GIF/Unicode version, however because I used MathML there is no immediate one-to-one correspondence.

For example, ` limCC ` is disaplayed:

• In MathML as: <msub><mo>lim</mo> <mi>&Copf;</mi></msub>
• In unicode (althtmldef) as: lim_&#8450;
• In LaTeX as : {\rm lim}_\mathbb{C}
  

Whereas &#8450; and &Copf; are actually entities for the same glyph. For example, recently I've stumbled upon ` .0. ` (a variable usually representing the zero element of a group), which is represented as a zero with dotted underline in Unicode - I don't know how to create a dotted underline in MathML; in LaTeX, ` .0. ` is simply represented as a zero.

BR,
_
Thierry

[Benoit]

Thanks, I can see the new feature now, and it looks good.

I understand the difficulty of translating from unicode to mathML... I just hope it will not be too hard to maintain if some changes are made in the $t comment of set.mm, for instance.

Benoit

[Thierry Arnoux]

I actually hope this will be made official and stored/updated alongside with set.mm, either as a separated file on the same github repository, or as part of the $t comments.
Right now I have to catch up with 1000+ symbols, but normally the incremental changes shall be manageable. They could either be done by the contributors, or I could help them if needed.

[Thierry Arnoux]

> - like David, I see problems for wceq and wcel
>

I think I understood what's going on with ~ wceq and ~ wcel - it's a bit
technical :
they are actually both defined inside a "patch to prevent connective
overloading", and as a result the A and B variable tokens used in these
definitions are "scoped" inside this patch, they are actually not the
same as the global ones (although they look exactly the same). My
schemes are defined outside of any scope, so I've been using the global
symbols only.

Right now I don't have a solution for this, I'll think more about how to
fix it - but hopefully the additional cost for handling this special
case shall not be higher than the benefit of having those 2 rules
displayed correctly in mmdefinitions.html...
_
Thierry

[David A. Wheeler]

Worst comes to worst, you could make an exception and simply use the Unicode result for those two cases. I imagine you could to find some reasonable rule to detect the pattern that causes the problem and then do it that way.
--- David A.Wheeler

[Thierry Arnoux]

The trick for ~ wceq and ~ wcel will probably be, for such tokens which
are defined in several scopes, to create duplicated rules for each of
the versions/scopes of the token. This could be done when the rules are
parsed.

I have another question, regarding the math embedded in comments. For
the sake of coherency, I would like to generate typesetting for them
with the same method as the formulas in the hypothesis and proof.
However several of them, even though built of valid set.mm tokens, are
actually not parseable, and as such, cannot be displayed using the same
method.
What do you think is best?
- that I don't use the "structured typesetting" for comments, but simply
always fallback to Unicode for them,
- that I insist on using the same typesetting method, which means
rewriting several of these "math embedded in comments" ,
- that I first try to use the "structured typesetting", but if I fail,
revert to unicode.

BR,
_
Thierry

[David A. Wheeler]

>What do you think is best?
>- that I don't use the "structured typesetting" for comments, but
>simply
>always fallback to Unicode for them,
>- that I insist on using the same typesetting method, which means
>rewriting several of these "math embedded in comments" ,
>- that I first try to use the "structured typesetting", but if I fail,
>revert to unicode.

This last option. There are a number comments that won't fully parse the way you want them to.


--- David A.Wheeler

[Thierry Arnoux]

Hi all,

Recently I've been catching up with this "structured typesetting" project, here is what I did :

• the pages are now entirely pre-rendered with MathJax + node.js, so loading time shall be fast enough (could you check for you?),
  
• the typesetting rules now cover all set.mm constructs and syntax (more than 1000 rules), even though several can still be improved,
  
• I've manually merged into the latest version of metamath.c the changes needed to generate the web pages. How could we better track version changes? I think Norm still wanted to wait before putting metamath.c in GitHub, so I have not created my own repo for this project fork yet. Or, even if this is experimental code, could it be included in the official metamath.c?
  
• I've added a functionality to quickly verify the integrity of the rules - this allows to detect if new syntax is not covered by the rules, and could be run as a travis script.
  
• I've generated the proofs for the whole set.mm - they are available here: http://metamath.tirix.org/index.html
• I've created a kind of front page explaining what this is about, at the same address: http://metamath.tirix.org/index.html

Of course there is still much to do, but it time to start tracking changes - I shall actually have started it before.

_
Thierry

On 17/07/2017 09:25, Mario Carneiro wrote:

In the logical arena, I don't think I can compromise on at least /\ left assoc, higher precedence than -> right assoc. These are essential for making prop calc sane and are universal conventions (among books that formalize logic to begin with). Remember, I'm not talking about programming conventions at all. (However, it's worth noting that if you have ever done type theory or Haskell / functional programming, you will be very familiar with -> as a right assoc operator.) Furthermore, there is no reason we can't make precedence information easily accessible, similar to the "syntax hints" in the current HTML.

I am fine with introducing mandatory parens whenever there is any significant disagreement about some precedence relation (as in the -u vs ^ case), but there needs to be an *actual* disagreement with some kind of reference, not some vague worry of confused users that haven't been taught any symbolic math. Let's face it: Metamath is really heavy on symbolic notation for math, and the reader *needs to learn it* to read it. We can make it easy for them to learn, but we should be aiming for something that an experienced mathematician with no Metamath training should be able to understand.

Mario

On Mon, Jul 17, 2017 at 1:24 AM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Mon, 17 Jul 2017 00:30:31 +0100, Mario Carneiro <di....@gmail.com> wrote:
> I don't buy this argument. Within mathematics, there is a well-established
> precedence relation for all the common arithmetic operators.

It's absolutely true that there's a well-established precedence relation.

But many people don't *correctly* understand them, so I think the use of
precedence should be greatly limited. Particularly if you want a larger readership.

David Hilbert remarked on August 8, 1900:
An old French mathematician said: ‘A mathematical theory is not to
be considered complete until you have made it so clear that you can
explain it to the first man whom you meet on the street.’
http://www.sciencedirect.com/science/article/pii/S0315086016300465

Hidden rules such as precedence rules can *inhibit* clear reading of an
expression's meaning.

> I don't think we are really disagreeing; I am referring to the algorithm
> structure, not the result, which may very well have a good deal of parens.

Fair enough, I'm focusing on the final result.

> x. / are left assoc (always paren / against itself)
> + - are left assoc

I think x. having higher precedence than + and - is the "most safe".
However, a nontrivial number of programmers do *not* know this rule,
and it gets *worse* the further you stray from this.

> -> is right assoc

Would this be automatically widely *understood*? I have my doubts.
It's safer to parenthesize.

> There are probably a few more I'm missing, but this should eliminate almost
> all parens in usual metamath deductions.

The goal shouldn't be to minimize parens, the goal should be to maximize clarity.

I suggest starting with parens in most cases, then *slowly* removing ones
when it's obvious removing them isn't interfering with understanding.
If there's doubt, parenthesize.

--- David A. Wheeler

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.

To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Giovanni Mascellani]

Hi,

Il 27/05/2018 17:54, Thierry Arnoux ha scritto:
> Recently I've been catching up with this "structured typesetting"
> project, here is what I did :

I find this very interesting and useful. As the author of another
program that works with set.mm, I am curious of how much difficult it is
to reuse the same rules in another project. I think that my mmpp might
eventually greatly benefit from showing Metamath formulae using your
structured typesetting. How are these rules specified?

Thanks, Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Thierry Arnoux]

Hi Giovanni,

The file with the rules can be found here:

http://metamath.tirix.org/set-mathml.mmts

Actually, if this is to be adopted more widely, it may be interesting to
add this file to set.mm's github repository, as it needs to be updated
whenever a new syntax is added to set.mm.
Most of the entries follow this simple model:

$s <pattern> $: <translation> $.

Where <pattern> is the pattern formula in set.mm, and <translation> is
the resulting string. In the translation, a variable name between
hashes, like #A#, shall be replaced by the translation of the variable A
in the pattern - obtained by a recursive call.

Lines starting with $i follow the same model, except that they are used
to specify the type of a variable, and restrict the patterns it will be
matched against. They are not to be further translated, even if a
variable appears in the pattern.

_
Thierry

[Glauco]

Nice job!

Would it be hard to also implement an "hide less important steps" feature, like what Mario's described in this post?

https://groups.google.com/forum/#!topic/metamath/Wm3VIfun_qk

To keep it simple, having the option to show only the n (let's say 5) statements with highest label numbers (in set.mm).

Glauco

[Giovanni Mascellani]

Hi Thierry,

Il 27/05/2018 19:43, Thierry Arnoux ha scritto:
> The file with the rules can be found here:
>
> http://metamath.tirix.org/set-mathml.mmts

That is wonderful, thank you! I will do some experiments with it as soon
as I have some spare time.

[Thierry Arnoux]

Thank you!

To be fair, I think yes, Mario's algorithm could be hard to implement.
I think the part about "fixing the proof" so that it still appears complete seems complex to me.
In algorithm B, for example, if the proof has been reduced, the same sylanc step may be used by several steps down the road, how would you replace it?
You would also need to maintain a list of what is a "less important" theorem.

To be simpler, I would maybe keep the full proof, just hiding/collapsing the steps deemed less important.

Your idea about keeping only the n statements with highest labels could be interesting.

To start with, I had a simple highlighting of antecedents/dependent steps in previous versions. I've actually lost it due to a mistake when manually merging the sources files.

I've reinstated it here in one file:
http://metamath.tirix.org/inttsk.html

That may already help a bit to read long proofs.
BR,
_
Thierry

[Mario Carneiro]

On Sun, May 27, 2018 at 9:56 PM, Thierry Arnoux <thierry...@gmx.net> wrote:

Thank you!

To be fair, I think yes, Mario's algorithm could be hard to implement.
I think the part about "fixing the proof" so that it still appears complete seems complex to me.
In algorithm B, for example, if the proof has been reduced, the same sylanc step may be used by several steps down the road, how would you replace it?

If we had the following situation, with later back-references to steps 4 and 5:

1::thm1       |- F1
2::thm2        |- F2
3::thm3         |- F3
4:3:thm4       |- F4
5:2,4:thm5    |- F5
6::thm6       |- F6

7:1,5,6:thm7 |- F7

8:4:idi      |- F4

9:5:idi      |- F5

then Algorithm A yields:

1::thm1       |- F1
2::thm2       |- F2
3::thm3        |- F3
4:3:thm4      |- F4
6::thm6       |- F6

7:1,2,4,6:thm7 |- F7

8:4:idi      |- F4

9:2,4:idi    |- F5

and Algorithm B yields:

1::thm1       |- F1
2::thm2        |- F2
3::thm3        |- F3
5:2,3:thm4    |- F5
6::thm6       |- F6

7:1,5,6:thm7 |- F7

4:3:thm4      |- F4
8:4:idi      |- F4

9:5:idi      |- F5

Note that the removal of step 4 as a replacement for step 5 only occurs when it is actually acting as a child of step 5; since step 4 is referenced twice here the second reference is retained, and after dag-ification you end up with step 4 relocating to just before step 8, which is now the first reference to it. The reference to step 5 appears as normal, since the step is still there.

You would also need to maintain a list of what is a "less important" theorem.

If it's based on axiom use, then this can be precomputed and kept in a list, and tested against each step.

Mario

To be simpler, I would maybe keep the full proof, just hiding/collapsing the steps deemed less important.

Your idea about keeping only the n statements with highest labels could be interesting.

To start with, I had a simple highlighting of antecedents/dependent steps in previous versions. I've actually lost it due to a mistake when manually merging the sources files.

I've reinstated it here in one file:
http://metamath.tirix.org/inttsk.html

That may already help a bit to read long proofs.
BR,
_
Thierry

On 28/05/2018 02:14, Glauco wrote:

Nice job!

Would it be hard to also implement an "hide less important steps" feature, like what Mario's described in this post?

https://groups.google.com/forum/#!topic/metamath/Wm3VIfun_qk

To keep it simple, having the option to show only the n (let's say 5) statements with highest label numbers (in set.mm).

Glauco

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.

To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.

[Glauco]

I would be really interested in reading proof pages with an expand/collapse option (and possibly a notion of "show only least trivial steps")  :-)

[Norman Megill]

An older expand/collapse proof-of-concept experiment can be found here:
http://us.metamath.org/other.html#displib
As it stands, it is somewhat confusing to use and needs work.

An issue for discussion is whether the proof should be expanded or collapsed when the page is entered.  I am in favor of showing the proof expanded by default, while providing one or more ways to collapse it for those wanting a higher-level view.  It is different from Windows Explorer, where you want to start with everything collapsed because your goal is to navigate to a single file.  I would find it annoying to have to click on dozens of sub-trees individually in order to see the whole proof, not knowing how big the proof really is or how much more I have to click, until it is fully expanded.

For most proofs I would probably use only the fully expanded proof, especially when the whole proof fits on the screen, which I think is the case for the majority of proofs.  Where I see a big advantage of collapsing is for long proofs where it is hard to match up, say, the outermost chain of equivalences because they are too far apart to appear on the screen at once.

Norm

[Thierry Arnoux]

So I've tried to prototype this proof collapsing on those pages, e.g.

    http://metamath.tirix.org/geoihalfsum.html

(it shall actually be on all pages of the site)

The page is first displayed with 12 steps shown (those with the highest label rank, as proposed by Glauco), plus the hypothesis and the theorem's formula. For relatively short proofs, almost everything shall be displayed.

When hovering the mouse over a step row, its antecedents and dependents steps are highlighted, as was already the case in earlier versions of the script.

I've added a '^' (expanded) or '>' (collapsed) marker at the beginning of the column (or a dot '·' if there is actually no antecedent step to expand/collapse).

The idea is that it works like a revered tree, with the leaves at the top and the root as the last line: when antecedents of a step are collapsed, this goes all the way up. If shown again, they are restored in their previous status.

I'm not completely satisfied with the result: as mentioned by Norm, one has to "click his way" through the proof to see its entirety. Tree implementations sometimes offer the possibility to "expand all", I think this shall be available here too.

BR,
_
Thierry

[Glauco]

I'm having some problems expanding line 164 in ftalem2: line 163 is not displayed properly (I'm using Chrome under Windows).

My feeling is that these pages are a good start toward an alternative presentation, with the goal to resemble the granularity of a "detailed pdf proof" as it could be found in a book: I was able to quickly focus on the most important steps of the Fundamental Theorem of Algebra (as Mario proved it).

http://metamath.tirix.org/ftalem2.html

[Thierry Arnoux]

That line shall now display correctly, but it seems that collapsing back a big number of steps take ages (ie. several seconds)

Maybe there is a need for some optimization.

_

Thierry

--

[Norman Megill]

Hi Thierry,

I like the default collapsing you chose, which seems very good for getting an overview of the proof.

If you are going to add a "expand all" function, a "default view" function might also be useful for re-establishing the default collapsing after the user goes exploring through various details of the proof then wants to see the proof overview again.  (Or, maybe just reloading the page would be sufficient.)

The mouseover highlighting of steps affected by and affecting a step is very nice.  Would it make sense to have it "stick" when the mouse moves off the proof (or off a specific column such as the Hyp column), so that the highlighting will persist when scrolling to a step off screen?

A possible wish-list item for discussion: add 4th and 5th highlight shades to indicate all steps that the current step depends on indirectly as well as all steps affected by the current step.  Or instead, perhaps use the current shades to indicate indirect dependence instead of just direct dependence?  I think indirect dependence is important for knowing that the current step didn't just pop out of the blue (esp. when its hypotheses are collapsed) but is a consequence of specific previous steps.

I understand the intent of alternating light mint green and lighter mint green in the full proof display - they make it easier to follow a line horizontally across the screen.  For a collapsed display, I'm not sure if they are helpful since they no longer necessarily alternate.  I found it slightly confusing at first to see so many different shades changing until I got used to it.  I'm not sure if alternating shades really make that much of a difference for our purpose.  They aren't used in ordinary text (that would be rather distracting), they are very helpful if not essential for tables with many columns and no cell borders, and proof displays are somewhere in between.  I decided against it for the existing web pages because I felt the table cell borders already guide the eye sufficiently.  In any case, you now have the line highlighted by a mouseover, so the purpose of alternating shades more or less disappears.

A small bug with the http://metamath.tirix.org/ftalem2.html display:  the N and S seem to be using the wrong font in the dIstinct variable list (and there is no S in the theorem).  Also, in the syntax hints, some symbols like -> and sum_ are red instead of black.

Overall, I think this display will be quite useful to people who already have some mathematical maturity i.e. are able to read and follow informal textbook proofs.  Basically they need hints about what is important in order to understand the proof, and the rest they can "fill in" mentally.  Your algorithm seems to have done a good job of choosing reasonable steps to provide these hints.  The display should also help satisfy people who think Metamath notation (linear strings of symbols) is cryptic.

On the other hand, I think there is still a need for the current direct translation of tokens into linear symbol strings, with no omission of parentheses, for people with little or no math background.  One of the features that makes Metamath stand out from all other proof languages is that a proof can  be followed in perfect detail by almost anyone, knowing only the mechanical substitution rule.  Some of that ability goes away once we add additional, possibly unstated rules for when parentheses are suppressed and when a series of symbols maps to a 2-dimensional display.

So for the long term future, I could see two displays, the mpeuni display and an mpethierry display, selectable just as mpeuni and mpegif are now.  I'm not sure if anyone still needs the mpegif display - does anyone think so? - which could be made obsolete.  Actually, this could be done right now by having the mpegif link changed to a link to your site, and conversely, while you fine-tune your display.

Any improvement in collapsing speed would be welcome.  I have received several complements over the years about how fast the Metamath pages load compared to many other sites.

BTW is any dynamic server-side functionality needed?  Right now, mirrors are trivial to set up regardless of web server, because all pages are static.

Norm

On Wednesday, May 30, 2018 at 10:07:25 PM UTC-4, Thierry Arnoux wrote:

That line shall now display correctly, but it seems that collapsing back a big number of steps take ages (ie. several seconds)

Maybe there is a need for some optimization.

_

Thierry

[David A. Wheeler]

> > Il giorno martedì 29 maggio 2018 20:30:02 UTC+2, Thierry Arnoux ha scritto:
> >>
> >> So I've tried to prototype this proof collapsing on those pages, e.g.
> >>
> >> http://metamath.tirix.org/geoihalfsum.html

...
> http://metamath.tirix.org/ftalem2.html

This is a really good-looking display! And unlike some of the previous
efforts at pretty displays, it seems to be relatively speedy.
On my laptop it's quite quick.
On an older smartphone it takes a few seconds to display, but I think
that the display time really isn't too bad. I like it!

The default collapsing selection is really nice for getting an overview,
and I think it's a good one to begin the display at.
That might be even speeding up display (if so, that's a good thing).
I think an "expand all" and "default collapse view" button is important,
but that should be relatively easy to add (the hard work's been done!).

> The mouseover highlighting of steps affected by and affecting a step is
> very nice.

Me too! That is really awesome. It seems to work on phones, too.

I will say that sometimes I had to do a bunch of clicks to do
expansions, esp. when there was a sequence of steps that had a single
predecessor. It's not clear how to improve that, esp. since I like being
able to control what's in view. Maybe slider at the top for
"minimum depth of steps to expand", default of 1? That doesn't need
to be right away, but I think it'd be worth thinking about.

> The display should also help satisfy people who
> think Metamath notation (linear strings of symbols) is cryptic.

Agreed. It *is* easier to read some constructs with a more
traditional presentation - all of us have been trained for many years
to read it.

> On the other hand, I think there is still a need for the current direct
> translation of tokens into linear symbol strings, with no omission of

> parentheses, for people with little or no math background. ...

> So for the long term future, I could see two displays, the mpeuni display
> and an mpethierry display, selectable just as mpeuni and mpegif are now.

I agree!!

> I'm not sure if anyone still needs the mpegif display - does anyone think
> so? - which could be made obsolete.

I think mpegif has served its purpose and can be declared obsolete.
Font faces look nicer, perform better, and have practically universal support.
There are a few subtleties setting them up, due to CORS security limits,
but the setup only has to be done once (and we've done it).

As you can see here:
https://caniuse.com/#feat=fontface
font faces are supported by Chrome, Firefox, Safari, IE (11), Edge,
UC Browser for Android, and even Samsung Internet.
The only browser that doesn't support font faces that's used by anyone is
Opera mini. But Opera mini omits many capabilities, and most of its users
will increasingly be iOS or Android users who could easily use a different
browser for these pages.

Awesome!

--- David A. Wheeler

[Glauco]

Il giorno giovedì 31 maggio 2018 18:22:40 UTC+2, Norman Megill ha scritto:

On the other hand, I think there is still a need for the current direct translation of tokens into linear symbol strings, with no omission of parentheses, for people with little or no math background.  One of the features that makes Metamath stand out from all other proof languages is that a proof can  be followed in perfect detail by almost anyone, knowing only the mechanical substitution rule.

I definitely agree that the current "full detail" 1to1 html translation should stay in place.

Thierry's pages are a really promising alternative for a condensed/dynamic presentation (that I'm sure will be fine tuned with new ideas in the future).

 

So for the long term future, I could see two displays, the mpeuni display and an mpethierry display, selectable just as mpeuni and mpegif are now.  I'm not sure if anyone still needs the mpegif display - does anyone think so?

I almost always use the mpegif version (mainly because Google returns those pages), and I use the ALT statements a lot. Would it be possible to move the ALT metainformation to mpeuni pages, also?

Glauco

 

[Giovanni Mascellani]

Hi,

Il 01/06/18 05:01, David A. Wheeler ha scritto:

> I think mpegif has served its purpose and can be declared obsolete.
> Font faces look nicer, perform better, and have practically universal
> support.

The only feature of mpegif I miss in mpeuni is the possibility to easily
see and copy the underlying Metamath code. Does anybody knows how to
recover that with mpeuni? Specifically, it seems that we (or, at least,
I) would like the possibility to select which text to copy when some
HTML span block is selected, in much the same way the alternative text
is copied when an image is selected. I am not an expert in HTML, but if
you think this would be useful I can ask on the relevant Q&A sites to
see if a reasonable solution can be cooked up. At that point I would
feel no need for mpegif anymore.

Bye, Giovanni.

[Norman Megill]

On Sunday, June 3, 2018 at 1:33:14 PM UTC-4, Giovanni Mascellani wrote:

Hi,

Il 01/06/18 05:01, David A. Wheeler ha scritto:
> I think mpegif has served its purpose and can be declared obsolete.
> Font faces look nicer, perform better, and have practically universal
> support.

The only feature of mpegif I miss in mpeuni is the possibility to easily
see and copy the underlying Metamath code. Does anybody knows how to
recover that with mpeuni? Specifically, it seems that we (or, at least,
I) would like the possibility to select which text to copy when some
HTML span block is selected, in much the same way the alternative text
is copied when an image is selected. I am not an expert in HTML, but if
you think this would be useful I can ask on the relevant Q&A sites to
see if a reasonable solution can be cooked up. At that point I would
feel no need for mpegif anymore.

This is a good point.

We can put tool tips that display on mouseover with e.g. "<span title="E.">&exist;</span> will display "E." on mouseover.  However, unlike with images, I don't know of any way to force the "E." and not the "&exist;" into the copy buffer.

I'll keep the mpegif directory up until a satisfactory solution is found.

Norm

[Giovanni Mascellani]

Hi,

Il 03/06/18 21:32, Norman Megill ha scritto:

> I'll keep the mpegif directory up until a satisfactory solution is found.

I wrote a question here:

https://stackoverflow.com/q/50671185/807307

Feel free to interact if you have something to add. If you have enough
reputation on StackOverflow, voting the question up can help to attract
attention over it. :-)

Let us see if some useful hint will arrive!

[David A. Wheeler]

Giovanni Mascellani:

> The only feature of mpegif I miss in mpeuni is the possibility to easily
> see and copy the underlying Metamath code. Does anybody knows how to
> recover that with mpeuni?

If you want the ability to "copy this step to the clipboard in Metamath format",
you could add a little button on each step to do that.
The button could be configured so that on click it would invoke a JavaScript function
that would put the corresponding text to the clipboard.
The "corresponding text" could be placed as hidden text on the page with its own selector.

IIRC there are some funny workarounds that you need to do with the clipboard,
but there's a "clipboard.js" library you can use:
https://clipboardjs.com/

Bonus points: You could make the buttons only visible if JavaScript is enabled
(start with them disabled, and then the JavaScript can enable it).
That will give you graceful degradation for users who disable JavaScript.

More bonus points: You could support multiple formats, e.g., TeX as well as Metamath.

--- David A. Wheeler

[Norman Megill]

As an experiment, I put a link to Thierry's "Structured version" next to the "GIF version" or "Unicode version" link on each web page e.g.

http://us2.metamath.org:88/mpeuni/ftalem2.html

so people can immediately compare Thierry's version during normal browsing.

Norm

On Thursday, May 31, 2018 at 12:22:40 PM UTC-4, Norman Megill wrote:

Hi Thierry,

I like the default collapsing you chose, which seems very good for getting an overview of the proof.

...

[Thierry Arnoux]

Hi all,

Copy to clipboard is relatively easy to implement, using the library mentioned by David. I've added that functionality, only to this page:

    http://metamath.tirix.org/ftalem2.html

When hovering the mouse over one proof step, after a short while, a tooltip shall be displayed with the Metamath source code for that step.
There shall also be an icon at the right of the line; clicking on that icon copies that Metamath source to the clipboard.

Other features are unchanged.

BR,
_
Thierry

--

[Dan Connolly]

This is really fantastic.

I really enjoyed the traditionally typeset formulas, but I eventually ran into one that was ambiguous for lack of ()s. Ah yes... step 8 of 2p2e4:

2 + 1 + 1 = 2 + 1 + 1

With this "look at and copy the original metamath source" feature, I get everything I could wish for all in one place.

Well, I guess I do have one more wish: a link to the whole proof in plain text; i.e. the response from the metamath program for "show me 2p2e4".

On Mon, Jun 4, 2018 at 12:46 PM, Thierry Arnoux <thierry...@gmx.net> wrote:

Hi all,

Copy to clipboard is relatively easy to implement, using the library mentioned by David. I've added that functionality, only to this page:

    http://metamath.tirix.org/ftalem2.html

When hovering the mouse over one proof step, after a short while, a tooltip shall be displayed with the Metamath source code for that step.
There shall also be an icon at the right of the line; clicking on that icon copies that Metamath source to the clipboard.

Other features are unchanged.

BR,
_
Thierry

On 04/06/2018 09:32, Norman Megill wrote:

As an experiment, I put a link to Thierry's "Structured version" next to the "GIF version" or "Unicode version" link on each web page e.g.

http://us2.metamath.org:88/mpeuni/ftalem2.html

so people can immediately compare Thierry's version during normal browsing.

Norm

On Thursday, May 31, 2018 at 12:22:40 PM UTC-4, Norman Megill wrote:

Hi Thierry,

I like the default collapsing you chose, which seems very good for getting an overview of the proof.
...

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.

To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.

To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

--

Dan Connolly

http://www.madmode.com/

[David A. Wheeler]

I think the remove parentheses action is too aggressive. Can't it be changed so that it removes parentheses only in certain cases? A few extra parentheses are not a problem.
--- David A.Wheeler

[Thierry Arnoux]

First, thank you very much for all the encouraging comments!

I'll try to catch up with questions/requests as much as possible:

On 05/06/2018 06:30, David A. Wheeler wrote:

I think the remove parentheses action is too aggressive. Can't it be changed so that it removes parentheses only in certain cases? A few extra parentheses are not a problem.

--- David A.Wheeler --

That's a very good point, and I think the previous discussion on parenthesis was not completely closed, but was rather pending some progress on my side with the page generation!

My original goal is to display expressions just like they would be displayed on a textbook, so that e.g. a quadratic form ax2+bx+c is rendered without parentheses, just as in a textbook. This of course leads to ambiguity. To solve this, we could either put back those parenthesis everywhere, or explicitly keep them only for steps where associativity theorems are applied, or for statements of associativity theorems, like ~addass*, which is what one would see in textbooks.

I would tend to prefer the second solution. What do you think?

On 01/06/2018 00:22, Norman Megill wrote:

A small bug with the http://metamath.tirix.org/ftalem2.html display:  the N and S seem to be using the wrong font in the dIstinct variable list (and there is no S in the theorem).  Also, in the syntax hints, some symbols like -> and sum_ are red instead of black.

That's a very interesting point, here is the explanation for that:
As for -> and sum_, they are tokens in Metamath, but have no meaning taken alone, unlike e.g. "cos" or "A". The same is true for e.g. "E!" or a standalone parenthesis "(". The structured typesetting only has rules for full valid expressions of type "wff", "class" or "set", which "sum_" is not. The same is valid for math in comments. E.g. in the comment of ~ftalem2, "F ( 0 )", and cannot be displayed correctly since this is not a valid set.mm expression. It would be if it was written ''( F ` O )". An example of a valid formula in comment would be ~nfsum.
For the case of comments, I've implemented a fallback to sequentially displaying the translation of the individual tokens.
For the display of individual tokens with no rules, I simply fallback to displaying their ASCII version in red. This was useful for debugging the display. A better fallback is necessary now, either adding rules for displaying these single expressions (but with what type? I'd probably add a dummy type for them), or by falling back to their MPEUNI display.

As for the reason why N and S are displayed in red, it's more complex so I will explain more in another post: let's keep the suspense!
Note that if you're curious about which tokens can be displayed standalone and which can't, you can check out the mmascii page.

On June 4, 2018 4:11:51 PM EDT, Dan Connolly <dc...@madmode.com> wrote:

Well, I guess I do have one more wish: a link to the whole proof in plain text; i.e. the response from the metamath program for "show me 2p2e4".

I'm not sure I understand what you mean:
Do you wish for a button to "expand all" steps of the proof, like David, which is probably what's next on my list, or do you mean you would like to get the result of the command "SHOW PROOF 2p2e4" in the Metamath program displayed or in a clipboard, which would be something like:

17     oveq1i.1=df-2    $a |- 2 = ( 1 + 1 )
18   eqtr4i.1=oveq2i  $p |- ( 2 + 2 ) = ( 2 + ( 1 + 1 ) )
32     3eqtri.1=df-4    $a |- 4 = ( 3 + 1 )
37       oveq1i.1=df-3    $a |- 3 = ( 2 + 1 )
38     3eqtri.2=oveq1i  $p |- ( 3 + 1 ) = ( ( 2 + 1 ) + 1 )
42       axi.1=2cn        $p |- 2 e. CC
43       axi.2=ax-1cn     $a |- 1 e. CC
44       axi.3=ax-1cn     $a |- 1 e. CC
45     3eqtri.3=addassi $p |- ( ( 2 + 1 ) + 1 ) = ( 2 + ( 1 + 1 ) )
46   eqtr4i.2=3eqtri  $p |- 4 = ( 2 + ( 1 + 1 ) )
47 2p2e4=eqtr4i     $p |- ( 2 + 2 ) = 4

On 01/06/2018 00:22, Norman Megill wrote:

Your algorithm seems to have done a good job of choosing reasonable steps to provide these hints.

Let me stress that while I've implemented it, the algorithm is originally nothing more than what Glauco suggested. I don't want to take undue credit for it!

Overall, like you, I do think there is a need to keep along the current direct translation of tokens into linear symbol strings as in MPEUNI. This display, although it is more accessible, transforms/hides a lot and the beauty of Metamath can only be seen in the "linear" displays.
_
Thierry

[David A. Wheeler]

>That's a very good point, and I think the previous discussion on
>parenthesis was not completely closed, but was rather pending some
>progress on my side with the page generation!

It is always safe to include parentheses. I suggest detecting a few patterns where it is clearly not a problem to remove parentheses, and then leave the rest alone. You can always add new patterns later. That would be a much safer course, since anything you didn't think of will be handled in a safe manner.

--- David A.Wheeler

[fl]

 

Would it be hard to also implement an "hide less important steps" feature, like what Mario's described in this post?

An informal proof is not simply a "hide subtrees" feature. Unessential

steps can be at the higher levels, and impotrant ones can be pushed into the depths of a subtree.

Take the time to examine a translation of an informal proof into a formal one to convince yourself.

Secondly the right device to navigate through a proof is not the mouse but the arrow keys.

--

FL

[Thierry Arnoux]

Actually the rules are implemented just like that:

• every rule, every variable has a type. The type of a rule is simply the first token of its pattern. The type of a variable is the token used in its declaration. A rule " $i class A $: ... $. " is interpreted as "A is of type class".
  
• the recursive display of formula makes use of these types. Take the display of  " |- ( ph -> ( A + B ) = C ) " as an example:
  
• It is of type |-, and first matches rule " |- ( ph -> ps ) ". When unifying these formulas, ps is matched with "( A + B ) = C".
  
• Then, ps is of type wff, so we are looking for a rule for matching "wff ( A + B ) = C". We find "wff A = B", where A and B are both of type "class".
  
• Recursively, we have to find a rule matching "class ( A + B )".
  
• this system of "types" is reused for differentiating between displays with- and without parenthesis.
  For the cases where parenthesis can be omitted (and only for those cases), instead of class variables A, B, C.. special variables O, P, Q are used. They have a special type, "class-o", which results in a display without parenthesis. Whenever we know parenthesis can be omitted, instead of using A, B, C, the variables O, P, Q are used in the rules. For example, since fractions are displayed as two separated rows, we are sure neither nominator nor denominator should get additional parenthesis. The rule for fraction will be " $s class ( O / P ) $: ... $. ". The same is true, for example, for exponents, which are on their own rows (but not for their radicals), for function values " F ` ( O ) ", since the "O" already has parenthesis around it, and so on.
• for the generic case, in the end, there are two rules which tell how to represent operations: The "class" version has parenthesis, while the "class-o" does not.
  

$( By default, put brackets on infix operator classes $)
$s class ( A F B ) $: <mfenced><mrow>#A# #F# #B#</mrow></mfenced> $.

$( By default, don't put brackets on O-classes $)
$s class-o ( A F B ) $: <mrow>#A# #F# #B#</mrow> $.

• for associativity of addition, there are specific rules, which remove the inner parenthesis especially, and only in these cases:
  

$( Associativity for addition $)
$s class ( ( A + B ) + C ) $: <mfenced><mrow>#A# <mo>+</mo> #B# <mo>+</mo> #C# </mrow></mfenced> $.
$s class ( A + ( B + C ) ) $: <mfenced><mrow>#A# <mo>+</mo> #B# <mo>+</mo> #C# </mrow></mfenced> $.

$( Associativity for addition, non-fenced expressions $)
$s class-o ( ( A + B ) + C ) $: <mrow>#A# <mo>+</mo> #B# <mo>+</mo> #C# </mrow> $.
$s class-o ( A + ( B + C ) ) $: <mrow>#A# <mo>+</mo> #B# <mo>+</mo> #C# </mrow> $.

        Would we choose to add a restriction, only these rules would not apply to ~addass* theorems.

Is that what you were thinking about?
_
Thierry

[Thierry Arnoux]

On 01/06/2018 00:22, Norman Megill wrote:

> If you are going to add a "expand all" function, a "default view"
> function might also be useful for re-establishing the default
> collapsing after the user goes exploring through various details of
> the proof then wants to see the proof overview again.  (Or, maybe just
> reloading the page would be sufficient.)

FYI, there is now a toggle at the top right of proof tables. Clicking it
will toggle between expand all steps, and returning to the starting display.
_
Thierry

[David A. Wheeler]

>         Would we choose to add a restriction, only these rules would
>not apply to ~addass* theorems.
>
>Is that what you were thinking about?

That was not exactly what I had in mind, but that might work. Another heuristic that might work, and would be more general, would be to notice if the only thing that moved position from a previous step were parentheses, and in that case do not remove them.


--- David A.Wheeler

[fl]

I just want to emphasize the fact that the  right device to explore a proof is the arrow keys not the mouse.

Comfort and speed matter.

-- 

FL

[fl]

An older expand/collapse proof-of-concept experiment can be found here:
http://us.metamath.org/other.html#displib

One interesting point here is that the formula is also displayed before substitutions are made.

-- 

FL

[Norman Megill]

Your comment provides no information and is not helpful.  What do you expect the arrow keys to do that they don't do now?

If you want an old-fashioned pure keyboard experience, you can use the w3m browser (only works with mpegif though).

There is a Firefox add-on called "My Keyboard Navigator" that lets you browse using only the keyboard.  I haven't tried it, though.  Perhaps you can try it and report back your experience.

Norm

[David A. Wheeler]

I few minor comments looking at <http://metamath.tirix.org/funimaex.html>:

* Hypotheses and assertions should also have a "Metamath copy" button.

* There's a bug when copying step 2 (involving function application). It produces:
|- ( ( Fun A /\ B e. _V ) -> ( A
which has unbalanced parens and thus is obviously not right :-).

But don't let my critiques discourage you. I think this is very promising.

--- David A. Wheeler

[Thierry Arnoux]

On 07/06/2018 03:26, David A. Wheeler wrote:

> * There's a bug when copying step 2 (involving function application). It produces:
> |- ( ( Fun A /\ B e. _V ) -> ( A
> which has unbalanced parens and thus is obviously not right :-).

Yes! Obviously I omitted to convert the "<", ">", and "&" symbols to the
respective corresponding HTML entities.
Such issues will occur if they appear in the ASCII version of the formula.
I'll try to fix it soon!

[fl]

Your comment provides no information and is not helpful. 

You repeat yourself.

 

What do you expect the arrow keys to do that they don't do now?

Simple. Use the arrow keys to move from one step to the other or open a step. It will be smoother.

You need an interface that is useful. With that kind of interface you will have to open or close 

hundreds of steps while exploring the proof. Don't use the mouse, use the keyboard. 

-- 

FL