smm in the browser

[Stefan O'Rear]

I've implemented a subset of the Metamath web site by way of downloading a .mm
file and processing it on the client side.

Code: https://github.com/sorear/smm-webui
[The README there should be fairly up to date, just beware that it requires
downloading ~100MB of dependencies and I have no idea if it works on Windows]

Prebuilt version: https://smm.divshot.io
[Is there a better choice for this? github pages does not support custom
routes so I went looking for an alternative, and there are surprisingly few
players in this space it seems.]

Features: Most of them should be fairly discoverable. Two that aren't:

1. Layout of the theorem list switches significantly at 768 CSS pixels width.
The breakpoint may not be optimal.

2. Click on a subexpression to reveal grouping.

Non-Features (things it doesn't do yet):

1. Comment markup parsing

2. Meaningful proof display

Things which surely need work:

1. The bottom copy is something I just made up, and is speaking for people I
don't actually have authority to speak for. Wording tweaks accepted.

2. The ?go= / ?node= thing sucks, but it was the simplest thing that I knew how
to make work. I've been thinking of ways to do better, no firm ideas yet.

3. I need to figure out how to do automated testing for this; it's worked quite
well for the smm core but is not used in smm-webui yet.

It _seems_ to work in Chrome 43, Safari 6, Firefox 38, Firefox 39, and IE 10,
although there are a couple styling issues in the last oen (there's a
superfluous margin on the top of the page and alignment is broken in the inline
outline nav).

Some other thoughts:

1. Since it downloads a .mm file and then works with that, the bandwidth
behavior is significantly different from a metamath mirror: ~250kb of code,
then 9.2 MB of set.mm (with transparent gzip compression), then nothing
thereafter. If you want to run a mirror and not rely on free CDNs that could
decide to quit at any time, the bandwidth usage will probably be higher for
brief visitors and lower for long visits...

2. Especially if they switch math mode halfway through, because there's only
one version of the database.

3. Working from .mm files means we can provide editing options later. Details
TBD.

4. I've started down the path of extending .mm file syntax for this. See:
https://github.com/sorear/smm-webui/blob/master/public/assets/set-config.mm

--

Questions? Comments? Thoughts?

-sorear

[David A. Wheeler]

This is pretty cool. Another thing it needs is a way to show JUST the table of contents, where you can click to see more. Set.mm is pretty big.
--- David A.Wheeler

[Stefan O'Rear]

On Sun, Jul 05, 2015 at 06:01:27PM -0400, David A. Wheeler wrote:
> This is pretty cool. Another thing it needs is a way to show JUST the table of contents, where you can click to see more. Set.mm is pretty big.

How would that differ from https://smm.divshot.io/mpe/toc ?

(You have 3 choices from the top middle menu: the full list starting from page
1, the 2-level TOC, and the 3-level TOC).

-sorear

[David A. Wheeler]

On at least Firefox on Android, even the table of contents option shows a lot of detailed text. For example section 1 includes the text defining logic. That is useful text, but not what I would expect to see when showing just a table of contents.


--- David A.Wheeler

[Stefan O'Rear]

On Sun, Jul 05, 2015 at 07:21:12PM -0400, David A. Wheeler wrote:
> On July 5, 2015 6:56:25 PM EDT, Stefan O'Rear <stef...@cox.net> wrote:
> >On Sun, Jul 05, 2015 at 06:01:27PM -0400, David A. Wheeler wrote:
> >> This is pretty cool. Another thing it needs is a way to show JUST
> >the table of contents, where you can click to see more. Set.mm is
> >pretty big.
>

> On at least Firefox on Android, even the table of contents option shows a lot of detailed text. For example section 1 includes the text defining logic. That is useful text, but not what I would expect to see when showing just a table of contents.

Ah. It's intended to show just the first 200 characters of the "prologue"
field, which I thought would provide useful context about what you're looking
for, but I can remove it if it does more harm than good. (Presumably the
unabbreviated copy would still appear in the main listing.)

You mention Android - how's the performance like? On my dev machine, loading
the set.mm database takes 1-3 seconds (assuming the file itself is already in
cache).

(I haven't tried to optimize this at all for SpiderMonkey yet. I'm a little
surprised at how fast it already is on desktop Firefox.)

-sorear

[David A. Wheeler]

On Sun, 5 Jul 2015 16:41:27 -0700, Stefan O'Rear <stef...@cox.net> wrote:
> On Sun, Jul 05, 2015 at 07:21:12PM -0400, David A. Wheeler wrote:
> > On July 5, 2015 6:56:25 PM EDT, Stefan O'Rear <stef...@cox.net> wrote:
> > >On Sun, Jul 05, 2015 at 06:01:27PM -0400, David A. Wheeler wrote:
> > >> This is pretty cool. Another thing it needs is a way to show JUST
> > >the table of contents, where you can click to see more. Set.mm is
> > >pretty big.
> >
> > On at least Firefox on Android, even the table of contents option shows a lot of detailed text. For example section 1 includes the text defining logic. That is useful text, but not what I would expect to see when showing just a table of contents.
>
> Ah. It's intended to show just the first 200 characters of the "prologue"
> field, which I thought would provide useful context about what you're looking
> for, but I can remove it if it does more harm than good. (Presumably the
> unabbreviated copy would still appear in the main listing.)

I think it's better without the context, because the TOC itself is long.

Especially on a phone... there's no way to see the bigger picture.

> You mention Android - how's the performance like? On my dev machine, loading
> the set.mm database takes 1-3 seconds (assuming the file itself is already in cache).

It won't set speed records, but it's usable!



--- David A. Wheeler

[Stefan O'Rear]

On Sun, Jul 05, 2015 at 07:55:00PM -0400, David A. Wheeler wrote:

> On Sun, 5 Jul 2015 16:41:27 -0700, Stefan O'Rear <stef...@cox.net> wrote:
> > Ah. It's intended to show just the first 200 characters of the "prologue"
> > field, which I thought would provide useful context about what you're looking
> > for, but I can remove it if it does more harm than good. (Presumably the
> > unabbreviated copy would still appear in the main listing.)
>

> I think it's better without the context, because the TOC itself is long.
>
> Especially on a phone... there's no way to see the bigger picture.

OK, I got rid of it. Also changed the way the centering is done for the inline
children links to hopefully work on IE.

-sorear

[David A. Wheeler]

When using Firefox on Android, the initial load takes about 30 seconds... given the statement that it was loading, I was not surprised. After that, it seems to work fairly smoothly. I cannot seem to select the gif display, which is unfortunate because Firefox on Android cannot display important symbols like the turnstile.


--- David A.Wheeler

[Stefan O'Rear]

On Sun, Jul 05, 2015 at 08:18:12PM -0400, David A. Wheeler wrote:
> When using Firefox on Android, the initial load takes about 30 seconds...

> given the statement that it was loading, I was not surprised.

Ideally there would be more details there (to distinguish the "downloading"
from "parsing" steps, and provide progress for the former).

> After that, it seems to work fairly smoothly. I cannot seem to select the
> gif display, which is unfortunate because Firefox on Android cannot display
> important symbols like the turnstile.

Now that's interesting. What happens when you try, does the link not take at
all or does it take but you get a bunch of broken/missing images?

Do the source/LaTeX modes work?

Does http://localhost:4200/mpe/list?go=opth work? (For some reason, the
ordered pair brackets <. >. are rendered as GIFs even in Unicode mode, which
might be diagnostically useful.)

BTW, my long term plan is to make a .woff font with the Computer Modern symbols
we use along with the Metamath-specific symbol variants (e.g. -1-1-onto->) and
then use that everywhere...

-sorear

[Mario Carneiro]

On Sun, Jul 5, 2015 at 5:58 AM, Stefan O'Rear <stef...@cox.net> wrote:

I've implemented a subset of the Metamath web site by way of downloading a .mm
file and processing it on the client side.

This is fantastic. For a mockup it looks very slick - I'm happy there is a web 2.0 developer on the team, although every time I check back there is a new technology with a snappy name being used :)

 

Prebuilt version: https://smm.divshot.io
[Is there a better choice for this?  github pages does not support custom
routes so I went looking for an alternative, and there are surprisingly few
players in this space it seems.]

The obvious choice for this is metamath.org, since I think Norm has complete control over the backend.

 

2. Click on a subexpression to reveal grouping.

I would modify this so that double-, triple-, quadruple-clicking successively highlights larger subterms up the tree. (I am familiar with this behavior from Mathematica. Eclipse has a similar feature using Ctrl-Alt-Up, I believe.)

 

2. The ?go= / ?node= thing sucks, but it was the simplest thing that I knew how
to make work.  I've been thinking of ways to do better, no firm ideas yet.

I don't see what the problem is with this. It seems fine - in fact I'm surprised you managed more than https://smm.divshot.io/?data=stuff for all the pages (all working off the same base page).

4. I've started down the path of extending .mm file syntax for this.  See:
https://github.com/sorear/smm-webui/blob/master/public/assets/set-config.mm

Could you explain the intended purpose of these tags? Note that {"set", "wff", "class"} is discoverable: these are the type codes of variables ($f). The complement is {"|-"} which is also discoverable as the type codes of $p statements. I'm not sure what you need {"wff", "|-"} for but {"wff"} is discoverable as the type code of the root node of a grammar parse on any $p statement.

Mario

[Mario Carneiro]

You could also replace "$p statement" here with "$a axiom with $e hypotheses" if you don't like scanning proofs to determine structure. You can also use this to distinguish syntax axioms from logical axioms: the logical axioms start with {"|-"} and the syntax axioms start with {"set", "wff", "class"}, once you have used any of the above methods to determine these sets.

Mario

[Stefan O'Rear]

On Sun, Jul 05, 2015 at 08:51:04PM -0400, Mario Carneiro wrote:
> On Sun, Jul 5, 2015 at 5:58 AM, Stefan O'Rear <stef...@cox.net> wrote:
>
> > I've implemented a subset of the Metamath web site by way of downloading a
> > .mm
> > file and processing it on the client side.
> >
>
> This is fantastic. For a mockup it looks very slick - I'm happy there is a
> web 2.0 developer on the team, although every time I check back there is a
> new technology with a snappy name being used :)

Heh. Much of this is new to me as well / a learning opportunity.

> > Prebuilt version: https://smm.divshot.io
> > [Is there a better choice for this? github pages does not support custom
> > routes so I went looking for an alternative, and there are surprisingly few
> > players in this space it seems.]
> >
>
> The obvious choice for this is metamath.org, since I think Norm has
> complete control over the backend.

> 2. Click on a subexpression to reveal grouping.
> >
>
> I would modify this so that double-, triple-, quadruple-clicking
> successively highlights larger subterms up the tree. (I am familiar with
> this behavior from Mathematica. Eclipse has a similar feature using
> Ctrl-Alt-Up, I believe.)

I like that and it does that now. There's a bit of an inconvenient interaction
with the browser native triple-click-to-highlight-paragraph behavior though.

> > 2. The ?go= / ?node= thing sucks, but it was the simplest thing that I
> > knew how
> > to make work. I've been thinking of ways to do better, no firm ideas yet.
> >
>
> I don't see what the problem is with this. It seems fine - in fact I'm
> surprised you managed more than https://smm.divshot.io/?data=stuff for all
> the pages (all working off the same base page).

It's more the interaction between ?go/?node/?page that are the problem;
currently there are a few ways to get to a ?page=5&node=asdf, whereupon the
page=5 is ignored (the specific node takes precedence), whereas we should have
one URL for each state.

What I originally wanted was to not have visible pages (instead, do that thing
where it presents a very tall scrolling field and loads whatever is in the
viewport), and then use #anchors for positioning, e.g.
#sec-add-the-axiom-of-union, #thm-opth. But I didn't see an obvious way to do
it. (It probably can be done, but should it?)

> 4. I've started down the path of extending .mm file syntax for this. See:
> > https://github.com/sorear/smm-webui/blob/master/public/assets/set-config.mm
> >
>
> Could you explain the intended purpose of these tags? Note that {"set",
> "wff", "class"} is discoverable: these are the type codes of variables
> ($f). The complement is {"|-"} which is also discoverable as the type codes
> of $p statements. I'm not sure what you need {"wff", "|-"} for but {"wff"}
> is discoverable as the type code of the root node of a grammar parse on any
> $p statement.

In principle, it's all discoverable. My reasoning for making it explicit was
that if somebody messes up and adds a $f |- statement, I want that statement to
be flagged as an error, rather than causing an incorrect guess and then
flagging many unrelated statements as errors, which could be much harder to
track down.

-sorear

[David A. Wheeler]

Fof "math display" I can select Unicode, latex, or ascii. Ascii is quite usable. In Unicode, many things look good but important symbols like the turnstyle turn into big black rectangles.

Oddly enough, I simply cannot select gifs at all. I press my finger on that option but nothing seems to happen.. it is not getting selected. It is small and hard to hit with a finger, but I think I am getting it.


--- David A.Wheeler

[David A. Wheeler]

> Do the source/LaTeX modes work?

LaTeX mode works in the sense that I can see the latex codes, but frankly ascii is easier to work with. Ascii works fine.

> Does http://localhost:4200/mpe/list?go=opth work? (For some reason, the
ordered pair brackets <. >. are rendered as GIFs even in Unicode mode, which
might be diagnostically useful.)

I presume you mean this url...
https://smm.divshot.io/mpe/list?go=opth

Yes, the ordered pair brackets are rendered as gifs even though it is in Unicode mode and I cannot enable a gif mode. Weird. Though hopeful, that means that somehow it must be possible to do this. Now if only someone could figure out how to do that on purpose. :-).

--- David A.Wheeler

[David A. Wheeler]

You might also want to use an application cache. Then you can use this completely offline, without any network connection once it has been initially downloaded simply by viewing it. More information is here:

https://developer.mozilla.org/en-US/docs/Web/HTML/Using_the_application_cache
--- David A.Wheeler

[Stefan O'Rear]

On Sun, Jul 05, 2015 at 11:17:22PM -0400, David A. Wheeler wrote:
> You might also want to use an application cache. Then you can use this completely offline, without any network connection once it has been initially downloaded simply by viewing it. More information is here:
>
> https://developer.mozilla.org/en-US/docs/Web/HTML/Using_the_application_cache

A nice idea, but it seems to interact poorly with the infinite set of URLs
generated by smm. I don't suppose Firefox for Android is going to support
service workers any time soon?

-sorear

[Stefan O'Rear]

On Sun, Jul 05, 2015 at 11:00:41PM -0400, David A. Wheeler wrote:
> Fof "math display" I can select Unicode, latex, or ascii. Ascii is quite usable. In Unicode, many things look good but important symbols like the turnstyle turn into big black rectangles.
>
> Oddly enough, I simply cannot select gifs at all. I press my finger on that option but nothing seems to happen.. it is not getting selected. It is small and hard to hit with a finger, but I think I am getting it.

Unfortunately I can't seem to reproduce the unselectability in Firefox for Mac,
and I don't have an Android device. Unsure how to proceed.

-sorear

[David A. Wheeler]

Perhaps give it a little more text. It is possible that it's just difficult to hit with only a few letters.
--- David A.Wheeler

[Mario Carneiro]

Since I'm an android developer by day, I happen to have a lot of devices on hand. I tested on a hdpi 10-inch tablet and an mdpi 4-inch and xxhdpi 5-inch phone display. It would be nice if there were a visible indication that the button has been pressed; currently the menu opens with the old option selected, and after I press the button it freezes for .5 to 1.5 seconds (with the old option still selected) and then clears the menu and shows the new setting. But I was unable to replicate David's issue - the GIF seemed to be selectable as easily as the other options.

--
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.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at http://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Mario Carneiro]

For LaTeX display, this would be a perfect opportunity to try MathJax on the output. LaTeX output has not been used for years, and I can tell there are thousands of errors in output (just looking at the text version I noticed that "|- A = B" turns into "\vdashA = B" which definitely isn't going to render). It would be nice to flush these out with an easy to use render test.

Mario

[Stefan O'Rear]

On Mon, Jul 06, 2015 at 12:51:11AM -0400, Mario Carneiro wrote:
> For LaTeX display, this would be a perfect opportunity to try MathJax on
> the output. LaTeX output has not been used for years, and I can tell there
> are thousands of errors in output (just looking at the text version I
> noticed that "|- A = B" turns into "\vdashA = B" which definitely isn't
> going to render). It would be nice to flush these out with an easy to use
> render test.

Not quite the same thing, but one of the ideas I've been kicking around is -
since we have parse trees for everything - a highly context sensitive, somewhat
ambiguous "Conventional" output mode. E.g. if you see "( ... / ... )", turn
that into "\frac{...}{...}" and then pass the output into MathJax.

-sorear

[Mario Carneiro]

A nice idea, but making math "look good" is a highly non-trivial problem, and for the specific example you've given I would still stick with the slash. ((A/B)/(C/D))/((E/F)/(G/H)) looks a lot better than the alternative with a horizontal fraction bar. For me the biggest "offender" in this vein is the exponential, but again it is easy to exploit this to get something much more unreadable than a straight line of text. Not to say it's a bad idea, but it is a hard problem and would take a long time to look more like "standard math".

One thing which I haven't suggested yet for web output because it's basically impossible with web 1.0 is nicer line breaks. This would go a long way toward making long expressions more readable. For a start, it might help to break between hypotheses in preference to within a hypothesis in the theorem list view. The goal would be something like my favorite mmj2 output style, AlignVarDepth99. Here is an example of AlignVarDepth2 (which differs from depth 99 only in adding some extra forced breaks where there would normally be optional breaks dependent on the line length, which is useful for this example of the effect of extreme line breaking):

|- ( R e. *Ring <->
     ( R e. Ring /\
       A. x e.
          ( Base ` R )
          A. y e.
             ( Base ` R )
             ( ( ( *r ` R ) ` x ) e.
               ( Base ` R ) /\
               ( ( ( *r ` R ) `
                   ( x ( +g ` R ) y ) ) =
                 ( ( ( *r ` R ) ` x )
                   ( +g ` R )
                   ( ( *r ` R ) ` y ) ) /\
                 ( ( *r ` R ) `
                   ( x ( .r ` R ) y ) ) =
                 ( ( ( *r ` R ) ` y )
                   ( .r ` R )
                   ( ( *r ` R ) ` x ) ) /\
                 ( ( *r ` R ) `
                   ( ( *r ` R ) ` x ) ) =
                 x ) ) ) )

Without looking at the code, I would explain the alignment as follows: Each node in the tree can be either expanded or inline. An inline node has inline children, so expansion starts at the root and works its way down (depending on the amount of line breaking that needs to be done). Each node has substitutions in the form "C1 V1 C2 V2... V(n-1) Cn" where Ci is a (possibly empty) sequence of constants and Vi is a variable which has been substituted with a subtree. The alignment for an expanded node is then:

C1 V1 C2

   V2 C3...

   V(n-1) Cn

where the Vi are aligned with each other, each on a new line. This could be done with tables in a JS-free solution, but the challenge is to decide dynamically which nodes should be expanded in order to fit on screen (the mmj2 algorithm uses a fixed character limit and breaks greedily until it gets under the limit, which works well as long as you are using a monospace font).

Mario

[David A. Wheeler]

> A nice idea, but making math "look good" is a highly non-trivial problem, and for the specific example you've given I would still stick with the slash. ((A/B)/(C/D))/((E/F)/(G/H)) looks a lot better than the alternative with a horizontal fraction bar.

The specific example can be solved by only using vertical space for slashes in specific cases. But that also proves the point that making math look really good is a highly nontrivial problem. There is a long list of other things I would work on first.


--- David A.Wheeler

[Norman Megill]

On Sunday, July 5, 2015 at 8:51:04 PM UTC-4, Mario Carneiro wrote::
>
>
> On Sun, Jul 5, 2015 at 5:58 AM, Stefan O'Rear <stef...@cox.net
> <mailto:stef...@cox.net>> wrote:
>
>     I've implemented a subset of the Metamath web site by way of
>     downloading a .mm
>     file and processing it on the client side.
>
>
> This is fantastic. For a mockup it looks very slick - I'm happy there is
> a web 2.0 developer on the team, although every time I check back there
> is a new technology with a snappy name being used :)
>
>     Prebuilt version: https://smm.divshot.io
>     [Is there a better choice for this?  github pages does not support
>     custom
>     routes so I went looking for an alternative, and there are
>     surprisingly few
>     players in this space it seems.]
>
>

> The obvious choice for this is metamath.org <http://metamath.org>, since

> I think Norm has complete control over the backend.

Only us2, at my home, is under my complete control.  I can provide
access if you want to experiment.  Since they block port 80, I can't
point it to us.metamath.org.

I have no control over the mirrors, so only static pages are guaranteed
to work.

Norm

[Stefan O'Rear]

On Sun, Jul 05, 2015 at 02:58:36AM -0700, Stefan O'Rear wrote:
> 1. The bottom copy is something I just made up, and is speaking for people I
> don't actually have authority to speak for. Wording tweaks accepted.

I'm surprised nobody has had any feedback on this. Really, is everyone OK with
my describing NF as a "heterodox [set] theory", or the Metamath community as an
"international team of volunteers"? And those four databases were chosen more
for having public CORS-enabled URLs than any other reason; what would folks
like to see?

Unrelated: I left out another important non-discoverable feature. smm-webui
assigns the current database to the "MMDB" global variable to provide an easy
way to experiment with the smm API in the Javascript console.

-sorear

[Mario Carneiro]

On Wed, Jul 8, 2015 at 12:52 AM, Stefan O'Rear <stef...@cox.net> wrote:

On Sun, Jul 05, 2015 at 02:58:36AM -0700, Stefan O'Rear wrote:
> 1. The bottom copy is something I just made up, and is speaking for people I
> don't actually have authority to speak for.  Wording tweaks accepted.

I'm surprised nobody has had any feedback on this.  Really, is everyone OK with
my describing NF as a "heterodox [set] theory", or the Metamath community as an
"international team of volunteers"?  And those four databases were chosen more
for having public CORS-enabled URLs than any other reason; what would folks
like to see?

I think it sounds really cool to call us an "international team of volunteers", and it's not incorrect (although to my ears it makes the team sound larger than it really is - not that I'm complaining). And I think that 'heterodox' is an apt description for the ontological status of NF set theory. I'm glad you chose those databases as well; I know several people wanted to see the IL and HOL databases on the web so you managed to beat the "official release" in this regard.

 

Unrelated: I left out another important non-discoverable feature.  smm-webui
assigns the current database to the "MMDB" global variable to provide an easy
way to experiment with the smm API in the Javascript console.

Very convenient. In fact, depending on how things go you might even be able to use the JS console as a cheap and easy user script / editor interaction.

Mario

[ocatmetamath]

<<The goal would be something like my favorite mmj2 output style, AlignVarDepth99. Here is an example of AlignVarDepth2 (which differs from depth 99 only in adding some extra forced breaks where there would normally be optional breaks dependent on the line length, which is useful for this example of the effect of extreme line breaking):>>

This is an interesting point. And after so many years, I finally got some feedback on 

the TMFF scheme design :-)

This project is also quite interesting. Is it still active? 

[Thierry Arnoux]

Not sure what you refer to by “the project”.

If it is about making math “look good”, this was my purpose in the “structured typesetting”, see e.g.

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

_

Thierry

[ocatmetamath]

Wow! That is really beautiful.

You were unable to make grothprim comprehensible, I see:

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

(smile)

Are you keeping that website current? Do you need funding

to host it in the cloud? I am really impressed. 

Next step 3d, virtual reality? Augmented reality in IOS

or Android?

* * *

[Thierry Arnoux]

Wow! That is really beautiful.

Thank you! Though it’s really only beautiful thanks to MathJax, I only did the translator.

You were unable to make grothprim comprehensible, I see:

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

(smile)

Yes, correct line breaking is something MathJax does not seem to do well, and I’m just using it. 

In this example I think the issue is that the formula to be rendered is very unbalanced, with a very short left hand and very long right hand, and MathJax does not further line-break it.

I’m afraid that to get something better, one would have to change MathJax itself, which I have not ventured into.

“Structured” display is only really interesting for formulas that mathematics render in 2D, like sums, integrals, fractions, etc.

Are you keeping that website current? Do you need funding

to host it in the cloud? I am really impressed. 

I have still not automated the generation, that would be the next thing to do (together with better documenting how it works and how to replicate it). A short script pulling the latest set.mm from GitHub and launching the generation shall do. The syntax dictionary, set-mathml.mmts, is already under GitHub and can be kept updated as new symbols are added.

Page generation is done by a modified Metamath.exe (I still have to post the changes on e.g. GitHub), and it absolutely not threaded, so generating the HTML pages takes several days to complete. That’s not a problem per se, I could simply trigger an automatic generation e.g. every week.

I’m using my own hosting for that, so it’s a personally funded project! If anyone is interested in mirroring the pages, this is easy because the pages are static, however they also are one or two orders of magnitude bigger than their MPEUNI Unicode counterparts. I think the total size was more than 1Gb (I’ll confirm the figure later).

Next step 3d, virtual reality? Augmented reality in IOS

or Android?

You decide! 

There are already enough pending trivial tasks at hand before that, though (like scripting/documenting/archiving as listed above)...

Other threads are discussing formalizing geometry. Maybe one interesting topic would be to define how we can embed illustrative figures for geometric proofs. (I suppose embedding SVG would be a reasonable choice)

Then, would it e.g. be possible to automatically generate a figure to illustrate a given statement in geometry?...

[Thierry Arnoux]

>  I think the total size was more than 1Gb (I’ll confirm the figure later).

I have a bad memory. The actual total size of the "Structured" HTML
files is 8.3Gb.

[ocatmetamath]

<<Other threads are discussing formalizing geometry. Maybe one interesting topic would be to define how we can embed illustrative figures for geometric proofs. (I suppose embedding SVG would be a reasonable choice)

Then, would it e.g. be possible to automatically generate a figure to illustrate a given statement in geometry?...

>>

Right, keep focused on the main line: proving things. Supporting that

with grants or crowdfunding is conceivable. Presupposing an agenda,

obvious needs to fulfill that, and clear ways to distribute the funds :-)

I think perhaps it is time to rethink these separate Ivory Towers of Metamath.

Think like Bezos: everything is a service (call) in the cloud. Build up the

infrastructure to perform real-time, dynamic, adaptive I/O functions (parse,

render, verify, unify...translate, etc.) Some functions like 3D rendering could

be (also) done at the client level, but the server would have full IQ and

data. 

I don't see how there would be "Metamath funding" without a common 

computing environment, and these days there is "cloud", private and public.

So it seems clear which direction to go for progress. IMO. (Perhaps

Google would provide cloud time as a donation to the cause. Ask Raph.)