Metamath online editor (yet another UI discussion thread)

[Mario Carneiro]

Hi All,

This is inspired by the George Hotz thread to some extent but also my own work on MM0 and such. What would be a good user experience for writing metamath theorems in a web application? For example, MM0 currently works via a language server (written in Haskell, with a new LSP server written in Rust on the way) connected to the VSCode editor, and this could be pretty easily ported to a web application using Monaco and emscripten, if I haven't misunderstood the state of the art here. But would that meet peoples' needs? I don't know whether there is a similar push-button way to get the mmj2 java application on the web, but again, it needs a UI rethink even assuming that works.

Looking at this from a green-field perspective, what should a web interface for metamath look like? Related work:

* The metamath web pages are completely non-interactive, although they set the standard for proof visualization. I think things could be improved here if the page was rendered by JS, rather than shipping a bunch of giant html tags.

* The "structured version" looks great but the frequent mathjax causes some significant performance problems. I am doubtful that this can be kept up in an interactive setting, so we would have to use more ascii.

* If I recall correctly, Stefan O'Rear made a prototype web app that could load and display theorems from set.mm, but I don't think this project made it very far and in particular it was not interactive (allowing to write proofs, check individually, run tactics, save the results, etc).

Modern web browsers are definitely up to the task of running a metamath verifier in JS, but I don't know a really successful user interface that we could apply here. Some observations:

* Opening set.mm in a text area is not an option. It's just too big to be displayed. More likely, the information has to be condensed into a proof listing and a per-proof editor "worksheet" view similar to mmj2. Are people happy with this approach?

* Downloading set.mm directly (with caching) on page load and saving to the browser cache is possible, so the user experience could be just as "live" as the lean web editor (https://leanprover-community.github.io/lean-web-editor/).

* WebAssembly is a pretty good option for doing metamath processing without the overhead of JS, and I expect you can do full set.mm verification on the same order as metamath.exe with the right setup.

Ultimately, I usually don't go for web apps because they are almost never the best tool for the job, once you've got serious about the task at hand, but for the newbie experience they are a big plus, and metamath's fast check time would translate to a pretty solid user experience, at least in principle.

Mario

[vvs]

This is inspired by the George Hotz thread to some extent but also my own work on MM0 and such. What would be a good user experience for writing metamath theorems in a web application? For example, MM0 currently works via a language server (written in Haskell, with a new LSP server written in Rust on the way) connected to the VSCode editor, and this could be pretty easily ported to a web application using Monaco and emscripten, if I haven't misunderstood the state of the art here. But would that meet peoples' needs?

The most obvious advantage would be portability from a user's point of view. But does it really holds? As far as I know VSCode used native libraries and presently supports only 64-bit CPU. For that reason I was forced to use Emacs mode for Lean which I won't regret by the way.

Modern web browsers are definitely up to the task of running a metamath verifier in JS, but I don't know a really successful user interface that we could apply here.

Again, there were attempts to use web sockets to interface with a local language server here: https://observablehq.com/@bryangingechen/lean-websocketd

Certainly Lean is slow in JS, but how much better Metamath will look in browser remains yet to be seen.

* WebAssembly is a pretty good option for doing metamath processing without the overhead of JS, and I expect you can do full set.mm verification on the same order as metamath.exe with the right setup.

That looks like an interesting idea if there is a good tools support.

Ultimately, I usually don't go for web apps because they are almost never the best tool for the job, once you've got serious about the task at hand, but for the newbie experience they are a big plus, and metamath's fast check time would translate to a pretty solid user experience, at least in principle.

I will agree here. Besides, having a web editor available creates a more "mature" impression. Why Lean (with origin from just 2013) has it while Metamath has not? Though, I know that there are much more active community (and experienced developers) around Lean. Probably not least because having a parsed language is more appealing to programmers? And having a web UI enables someone to create a web tutorial at some point.

Also, some people would say that JS itself is not a pretty language and is oriented towards web designers and not professional software developers. But I'm pretty sure that nobody would beat that click and forget experience when it comes to people who are curious about logic and proofs but not CS per se.

[Thierry Arnoux]

On 04/01/2020 18:28, Mario Carneiro wrote:

* If I recall correctly, Stefan O'Rear made a prototype web app that could load and display theorems from set.mm, but I don't think this project made it very far and in particular it was not interactive (allowing to write proofs, check individually, run tactics, save the results, etc).

Here is a link to Stefan's Web test. It would be interesting if someone tried it out. I assume it would be a very good starting point for a possible JS assistant.

https://github.com/sorear/smm/tree/master/webtest

From the README, it seems it provides commands available to the javascript console, so it certainly provides a good back-end. What would need to be filled-in is a front-end (displaying formulas, etc.)

In order to load an assistant, it should not be required to load the full set.mm, including comments and proofs. Definitions and statements would be enough, and whatever that input file is, it shall be cached so that next time the user loads it, a local copy is used.

[Jim Kingdon]

On 1/4/20 9:28 AM, Mario Carneiro wrote:

> Ultimately, I usually don't go for web apps because they are almost
> never the best tool for the job, once you've got serious about the
> task at hand, but for the newbie experience they are a big plus, and
> metamath's fast check time would translate to a pretty solid user
> experience, at least in principle.

I think your instinct is sound in terms of being skeptical about the
value of building a whole IDE inside a web browser. Not impossible, just
not clearly a win over making sure that Visual Studio Code (and anything
else using a language server, like NeoVIM) works well. And a lot of work
to even get to the point of "is this something I or others would want to
use?"

There is a potential integration with editors/IDEs in terms of "I hit
save, and my web browser reloads a proof view - generally similar to
SHOW STATEMENT/ALT_HTML - with my changes. That's inspired by how tools
like webpack work for writing web apps (for example, those using React).
Perhaps the biggest obstacle which springs to mind is how well the tools
handle partly written proofs or proofs with errors.

There's another potential use case for tutorials/learning. There
definitely have been "code in a web form" tools over the years, and I
think some of them have even seen some success in terms of getting
people started without a lot of startup effort. This, however, is
something I don't know as much about (for example, are these things
generally seen as successes or were they kind of fads which faded out?).
And we should consider other ways of reducing startup effort - packaging
our tools for debian, and/or other systems like homebrew, springs to mind.

[Jon P]

I've thought a bit about a web editor and I really like the idea. It makes distribution of the tool effortless. Here's a few things. 

Firstly for me I think the most enduring challenge of metamath is finding theorems in the database to use them in proofs. I had a go at making a search engine but that didn't go so well. I like how Milpgame is laid out with all the theorems down the left hand side. I think in my imaginary ideal tool that would be something which was central, easy ways to search the database with common theorems in a palette maybe and even suggested theorems to use next if that is possible. 

Secondly I had a look at making a frontend and came across Quill, you can see how in maybe 10 lines you can add a text editor to a webpage so I think the frontend would be relatively easy. 

Thirdly I recently came across literate programming for the first time. I think it's a really interesting idea and immediately made me think of metamath. If it were possible to write proofs in natural language and then have macros replace the natural language with mm steps I think that could be a really powerful way of bridging the gap between beginners and experienced users. It's also interesting how it only uses substitutions which is very in line with how metamath works. It might also really help with constructing a proof, that's generally how I try to do things, to write down the ideas first and then fill in the details after.

I even had some crazy thought about trying to auto generate natural language explanations of proofs from existing proofs, however that was probably just a flight of fancy. 

Jon

[Mario Carneiro]

On Sat, Jan 4, 2020 at 1:36 PM vvs <vvs...@gmail.com> wrote:

This is inspired by the George Hotz thread to some extent but also my own work on MM0 and such. What would be a good user experience for writing metamath theorems in a web application? For example, MM0 currently works via a language server (written in Haskell, with a new LSP server written in Rust on the way) connected to the VSCode editor, and this could be pretty easily ported to a web application using Monaco and emscripten, if I haven't misunderstood the state of the art here. But would that meet peoples' needs?

The most obvious advantage would be portability from a user's point of view. But does it really holds? As far as I know VSCode used native libraries and presently supports only 64-bit CPU. For that reason I was forced to use Emacs mode for Lean which I won't regret by the way.

I haven't heard of any issue like this, although admittedly I haven't touched a 32-bit machine in a long time. VSCode is an electron application, which means that it is pretty portable, and it runs on all major platforms. But the web isn't one of those, and Monaco (https://github.com/microsoft/monaco-editor) is the "web version" of VSCode (it uses the same back end code IIRC but the actual interface is a bit different and not nearly as feature-rich). Really, anything that is LSP compatible would work just as well, but I have learned my lesson from mmj2 never to attempt to write a text editor because it will eat your life. (And now I'm curious if Raph Levien concurs :) )

Modern web browsers are definitely up to the task of running a metamath verifier in JS, but I don't know a really successful user interface that we could apply here.

Again, there were attempts to use web sockets to interface with a local language server here: https://observablehq.com/@bryangingechen/lean-websocketd

Certainly Lean is slow in JS, but how much better Metamath will look in browser remains yet to be seen.

The main reason lean is slow in JS is because it was not really designed to run like that. It's a giant C++ app that was just run through emscripten, and I have doubts about the number of layers involved to make things happen. I am confident that a text editor + metamath web app would be bottlenecked on the text editor, not the metamath (which is pure compute and so translates well to wasm).

Ultimately, I usually don't go for web apps because they are almost never the best tool for the job, once you've got serious about the task at hand, but for the newbie experience they are a big plus, and metamath's fast check time would translate to a pretty solid user experience, at least in principle.

I will agree here. Besides, having a web editor available creates a more "mature" impression. Why Lean (with origin from just 2013) has it while Metamath has not?

Microsoft funding...

 

Though, I know that there are much more active community (and experienced developers) around Lean. Probably not least because having a parsed language is more appealing to programmers? And having a web UI enables someone to create a web tutorial at some point.

Also, some people would say that JS itself is not a pretty language and is oriented towards web designers and not professional software developers. But I'm pretty sure that nobody would beat that click and forget experience when it comes to people who are curious about logic and proofs but not CS per se.

I agree, although JS has improved a lot in recent years it's not really a language I would choose to program in. But wasm has opened the field a lot here for writing programs in your language of choice, as well as the bevy of JS-transpilable languages, so JS isn't your only option on the web anymore, practically speaking.

On Sat, Jan 4, 2020 at 1:36 PM Thierry Arnoux <thierry...@gmx.net> wrote:

On 04/01/2020 18:28, Mario Carneiro wrote:

* If I recall correctly, Stefan O'Rear made a prototype web app that could load and display theorems from set.mm, but I don't think this project made it very far and in particular it was not interactive (allowing to write proofs, check individually, run tactics, save the results, etc).

Here is a link to Stefan's Web test. It would be interesting if someone tried it out. I assume it would be a very good starting point for a possible JS assistant.

https://github.com/sorear/smm/tree/master/webtest

Ah, thanks I couldn't find the link.

From the README, it seems it provides commands available to the javascript console, so it certainly provides a good back-end. What would need to be filled-in is a front-end (displaying formulas, etc.)

In order to load an assistant, it should not be required to load the full set.mm, including comments and proofs. Definitions and statements would be enough, and whatever that input file is, it shall be cached so that next time the user loads it, a local copy is used.

I thought about serving pre-parsed metamath files in e.g. JSON, but metamath is already pretty easy to parse, so there might not even be that much to gain through transforming the data. I know that SMM3 was able to verify faster than download time (although I don't think it was designed to work on streaming input), so conceivably this can be done with close to zero overhead. (Also, I think 30 MB or whatever we're up to now is something like the size of the average web page by now so I think we won't be noticed. :P )

On Sat, Jan 4, 2020 at 1:50 PM Jim Kingdon <kin...@panix.com> wrote:

On 1/4/20 9:28 AM, Mario Carneiro wrote:

> Ultimately, I usually don't go for web apps because they are almost
> never the best tool for the job, once you've got serious about the
> task at hand, but for the newbie experience they are a big plus, and
> metamath's fast check time would translate to a pretty solid user
> experience, at least in principle.

I think your instinct is sound in terms of being skeptical about the
value of building a whole IDE inside a web browser. Not impossible, just
not clearly a win over making sure that Visual Studio Code (and anything
else using a language server, like NeoVIM) works well. And a lot of work
to even get to the point of "is this something I or others would want to
use?"

Right, this is the main draw of "try it online" web apps: they lower the barrier to entry. Probably set.mm isn't even necessary for this purpose, since here you are mostly doing toy examples and a reduced or axioms-only set.mm would be an easy way to provide a decent standard library without much else.

There is a potential integration with editors/IDEs in terms of "I hit
save, and my web browser reloads a proof view - generally similar to
SHOW STATEMENT/ALT_HTML - with my changes. That's inspired by how tools
like webpack work for writing web apps (for example, those using React).
Perhaps the biggest obstacle which springs to mind is how well the tools
handle partly written proofs or proofs with errors.

I still don't really understand what the GMFF option in mmj2 does (or what GMFF stands for), but I recall it doing something similar to this; it would render your current worksheet in a web browser with the gif images and you could write and they would live-update.

On Sat, Jan 4, 2020 at 2:31 PM Jon P <drjonp...@gmail.com> wrote:

I've thought a bit about a web editor and I really like the idea. It makes distribution of the tool effortless. Here's a few things. 

Firstly for me I think the most enduring challenge of metamath is finding theorems in the database to use them in proofs. I had a go at making a search engine but that didn't go so well. I like how Milpgame is laid out with all the theorems down the left hand side. I think in my imaginary ideal tool that would be something which was central, easy ways to search the database with common theorems in a palette maybe and even suggested theorems to use next if that is possible. 

Common theorems in a palette is an interesting idea. In particular, I wonder if theorems sorted by number of uses (say, the top 20 theorems) would make a useful "propositional logic toolbox" for doing all the in between work. Of course that's only half of the work, the other half is finding relevant theorems for your goal, and I have always used metamath.exe's "search" command for this. It's a very simple mechanism, essentially text search with a tiny bit of regex, but it's enough to find all theorems about a particular constant or an algebraic manipulation theorem.

Secondly I had a look at making a frontend and came across Quill, you can see how in maybe 10 lines you can add a text editor to a webpage so I think the frontend would be relatively easy. 

I think that text editors is one area that is very well trodden by the larger programming community, so I have little doubt that there is something suitable (and likely many things), so I'm not giving it that much thought. The main question is if you can get the desired interaction mode to work with the library.

Thirdly I recently came across literate programming for the first time. I think it's a really interesting idea and immediately made me think of metamath. If it were possible to write proofs in natural language and then have macros replace the natural language with mm steps I think that could be a really powerful way of bridging the gap between beginners and experienced users. It's also interesting how it only uses substitutions which is very in line with how metamath works. It might also really help with constructing a proof, that's generally how I try to do things, to write down the ideas first and then fill in the details after.

Patrick Massot has done something similar with lean: https://www.math.u-psud.fr/~pmassot/lean/ . (Click on the lines of proof to see the tactic line that corresponds to it, with buttons on each side to show how the state changes.)

 

I even had some crazy thought about trying to auto generate natural language explanations of proofs from existing proofs, however that was probably just a flight of fancy. 

It's not completely crazy: I am reminded of the Ganesalingam / Gowers prover (https://arxiv.org/abs/1309.4501), which produces plausible natural language proofs for statements about metric spaces. However, this prover is finding its own proofs, so it's not quite the same as processing existing proofs, which can use a much broader range of theorems, each having a complex "gloss" in terms of a deduction style argument.

Mario

[vvs]

I even had some crazy thought about trying to auto generate natural language explanations of proofs from existing proofs, however that was probably just a flight of fancy.

And you are certainly not alone:

https://formalabstracts.github.io/

https://en.wikipedia.org/wiki/Mizar_system

[Thierry Arnoux]

On 04/01/2020 20:58, Mario Carneiro wrote:

> I still don't really understand what the GMFF option in mmj2 does (or
> what GMFF stands for), but I recall it doing something similar to
> this; it would render your current worksheet in a web browser with the
> gif images and you could write and they would live-update.

Yes, according to MMJ2:

https://github.com/digama0/mmj2/blob/master/CHGLOG.TXT#L360

    ------------------------------------------------------------
    3. New! GMFF (Graphics Mode Formula Formatting) Enhancement.
------------------------------------------------------------

       What is great about this feature is that it helps users see
       right away what the Metamath ASCII formulas look like when
       rendered in html (or Latex, etc.) Simply press Ctrl-1 (One) on
       the Proof Assistant GUI screen to generate export file(s) via
       GMFF -- use Alt-Tab to switch back and forth between the Proof
       Assistant GUI and your browser window.

[OlivierBinda]

Le 04/01/2020 à 21:00, vvs a écrit :

I even had some crazy thought about trying to auto generate natural language explanations of proofs from existing proofs, however that was probably just a flight of fancy.

Ok. Now I know. I am crazy.

And you are certainly not alone:

https://formalabstracts.github.io/

https://en.wikipedia.org/wiki/Mizar_system

Give me another 2/3 weeks and I'll demonstrate with Mephistolus preview 3 (I skipped preview 2 a week ago to make my case more convincing) that I am also a good candidate to join the fun club of lunatics who want to make computer generate human proofs (with some human interaction). :)

Also, I believe that there is a lot of talk in this thread about making metamath/mm0 interface with some editor (emacs, vs studio, some language). IMO, this is a misconception to say that it is a thread about putting an UI on metamath

I am not sure that this is the right way to go, unless you want to convert the process of writing maths into the art of writing software, with features designed for software development but somehow adapted to maths.

What about writing a standalone App DEDICATED to maths ?


see you in 2/3 weeks for less talk and more video :)

Best regards,
Olivier

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b767ab62-4a42-4a6a-8289-214339bf3507%40googlegroups.com.

[Olivier Binda]

Le samedi 4 janvier 2020 18:28:18 UTC+1, Mario Carneiro a écrit :

Looking at this from a green-field perspective, what should a web interface for metamath look like? 

I am also really really interested by the answer to this question.
Because I am trying to build one. 
My prototype will have to be refactored/improved because, I am 100% sure that I won't get it right on my first try.

But If I had, at least partial answers to this question, my first try would be much much better/closer to what is needed

 

* The metamath web pages are completely non-interactive, although they set the standard for proof visualization. I think things could be improved here if the page was rendered by JS, rather than shipping a bunch of giant html tags.

* The "structured version" looks great but the frequent mathjax causes some significant performance problems. I am doubtful that this can be kept up in an interactive setting, so we would have to use more ascii.

* If I recall correctly, Stefan O'Rear made a prototype web app that could load and display theorems from set.mm, but I don't think this project made it very far and in particular it was not interactive (allowing to write proofs, check individually, run tactics, save the results, etc).

MathJax renders math beautifully and it is possible to make it interactive, as I will demonstrate soon.

 

Modern web browsers are definitely up to the task of running a metamath verifier in JS, but I don't know a really successful user interface that we could apply here. Some observations:

MathJax is the only thing on earth NOW that enables interactive and beautifully rendered maths on a computer.
So, javascript (or typescript, or whatever is used to make MathJax work) is not an option. You have to somehow use javascript to build a decent math ui.

(even if you port MathJax to another language, you'll still need the dom and javascript...or you would need to rewrite the dom in your target language, good luck with that, 

or painfully port MathJax to another subsystem that the dom)

On a side note, having to work with javascript opens a lot of opportunities :

antlr/lucene/elastic search do have javascript ports

So you could write a complete standalone Methamath with UI application in javascript, 
or in a language that is able to speak with a WebView (like java, kotlin, c++...)

 

* Opening set.mm in a text area is not an option. It's just too big to be displayed. More likely, the information has to be condensed into a proof listing and a per-proof editor "worksheet" view similar to mmj2. Are people happy with this approach?

* Downloading set.mm directly (with caching) on page load and saving to the browser cache is possible, so the user experience could be just as "live" as the lean web editor (https://leanprover-community.github.io/lean-web-editor/).

* WebAssembly is a pretty good option for doing metamath processing without the overhead of JS, and I expect you can do full set.mm verification on the same order as metamath.exe with the right setup.

Ultimately, I usually don't go for web apps because they are almost never the best tool for the job, once you've got serious about the task at hand, but for the newbie experience they are a big plus, and metamath's fast check time would translate to a pretty solid user experience, at least in principle.

The UI requirement for a UI for metamath are somewhat low performance-wise: we do not need 60 fps at resolution 4K ^^
 
Javascript will do beautifully

Mario

[vvs]

I am not sure that this is the right way to go, unless you want to convert the process of writing maths into the art of writing software, with features designed for software development but somehow adapted to maths.

What about writing a standalone App DEDICATED to maths ?

If you think about it for a minute then you should realize that it's just an old argument about GUI vs. CLI. Of course many people will prefer to design some figure visually. And some powerful extensions can only be written using programming languages. I think we need both. It is just happens that creating a good visual UI is much harder than programming languages. Also, I don't think that many CS students take an art lessons.

[OlivierBinda]

Le 05/01/2020 à 13:24, vvs a écrit :

I am not sure that this is the right way to go, unless you want to convert the process of writing maths into the art of writing software, with features designed for software development but somehow adapted to maths.

What about writing a standalone App DEDICATED to maths ?

If you think about it for a minute then you should realize that it's just an old argument about GUI vs. CLI. Of course many people will prefer to design some figure visually. And some powerful extensions can only be written using programming languages. I think we need both.

Sure. The GUI app I am writing will be free (without adds, with respect of user privacy, no bs like selling stuff to companies)... and open source after a reasonnable length of time (or after I die...)

At one point, people will want a CLI app/library, to build stuff on it, which I'll try to provide too but with a caveat :
There will be a price, say like 1€, for each user (Once, not the developer, mind you, the final user) to use it (forever, without adds, on many devices, ...)

That way, people could also build commercial app, if they want with prices as they want
(say, if they charge users 100€ for it, I would like to get 1€ out of it)

This would be this way because, on the gui app, I would be able to offer users
interesting stuff (but not necessary) that they could buy if they want
but I would not be able to do that on a cli/library app

It is just happens that creating a good visual UI is much harder than programming languages.

Yeah. I already feel the pain. :/

Developping an ui on a webview is a lot less frustrating than developping an ui on android.
But it is still painfull, with weird stuff happening on things you have no control on...

And I have not even touched the artistic/metric part of it yet... :/

Also, I don't think that many CS students take an art lessons.

Yes. This also one of my many shortcomings (I suck at taking artistic decisions, though I still try my best).
This is one of the reason why I'll need help.

I'll be in your care. Pretty please, everyone :)

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c293fe23-76f6-4457-8291-7c6f53260c29%40googlegroups.com.

[fl]

Thirdly I recently came across literate programming for the first time. I think it's a really interesting idea and immediately made me think of metamath. If it were possible to write proofs in natural language and then have macros replace the natural language with mm steps I think that could be a really powerful way of bridging the gap between beginners and experienced users. 

Honestly if you think that you will be able to use a system of formal logic withouth spending a decent amount of time on it, without learning logic and set theory 

and without breaking your head, stop right now.

Literate programming is not about replacing computer languages by natural languages. It is about reversing the relative importance of comments and code.

Comments become more important than code. It's about writing an essay and then adding code. This way the problem is better understood and the code 

is of better quality. 

-- 

FL

[Mario Carneiro]

On Sun, Jan 5, 2020 at 5:23 AM Olivier Binda <olus....@gmail.com> wrote:

Le samedi 4 janvier 2020 18:28:18 UTC+1, Mario Carneiro a écrit :

Looking at this from a green-field perspective, what should a web interface for metamath look like? 

I am also really really interested by the answer to this question.
Because I am trying to build one. 
My prototype will have to be refactored/improved because, I am 100% sure that I won't get it right on my first try.

But If I had, at least partial answers to this question, my first try would be much much better/closer to what is needed.

 Actually, from what I understand, I think Mephistolus is attempting to address a slightly different problem than what I'm talking about. You are interested in a (visual?) front end for metamath that is geared to the teaching of mathematics itself (correct me if I am wrong), while I am talking about how to provide an interface for people writing metamath "code". Abstraction of the underlying representation helps a little bit in both cases, but hiding the textual representation away completely would not be a good idea if the point is to teach a newbie what metamath is, since then the skills don't transfer.

* The metamath web pages are completely non-interactive, although they set the standard for proof visualization. I think things could be improved here if the page was rendered by JS, rather than shipping a bunch of giant html tags.

* The "structured version" looks great but the frequent mathjax causes some significant performance problems. I am doubtful that this can be kept up in an interactive setting, so we would have to use more ascii.

* If I recall correctly, Stefan O'Rear made a prototype web app that could load and display theorems from set.mm, but I don't think this project made it very far and in particular it was not interactive (allowing to write proofs, check individually, run tactics, save the results, etc).

MathJax renders math beautifully and it is possible to make it interactive, as I will demonstrate soon.

I'm sure it can. My main concern with use of mathjax is one of scale; mathjax rendering an average size metamath proof takes several seconds, which is over budget for an interactive editor. There are probably tricks you can play to improve this, but I see a difficult road here.

Modern web browsers are definitely up to the task of running a metamath verifier in JS, but I don't know a really successful user interface that we could apply here. Some observations:

MathJax is the only thing on earth NOW that enable interactive and beautifully rendered maths on a computer.

So, javascript (or typescript, or whatever is used to make MathJax work) is not an option. You have to somehow use javascript to build a decent math ui.

This sentence makes no sense. MathJax is implemented in javascript, so of course you could do the same thing mathjax does with javascript.

But again this shows our differing goals. For teaching math, sure, mathjax away, but for teaching metamath you probably want to introduce people to the ascii symbols that are used to represent expressions, because that's what appears in metamath files, and in all likelihood they will be typing these symbols when searching and writing proofs.

(even if you port MathJax to another language, you'll still need the dom and javascript...or you would need to rewrite the dom in your target language, good luck with that, 

or painfully port MathJax to another subsystem that the dom)

WASM covers this. You can write the core program in any language that compiles to wasm and use JS hooks for interaction with the web browser. Of course the program needs to be aware that it is running in a browser to some extent so it throws up the right interface.

 

So you could write a complete standalone Methamath with UI application in javascript, 

or in a language that is able to speak with a WebView (like java, kotloin, c++...)

Right, that's the plan.

The UI requirement for a UI for metamath are somewhat low performance-wise: we do not need 60 fps at resolution 4K ^^

 
Javascript will do beautifully

Ha, you would be surprised how slow some frameworks can be.

On Sun, Jan 5, 2020 at 7:24 AM vvs <vvs...@gmail.com> wrote:

I am not sure that this is the right way to go, unless you want to convert the process of writing maths into the art of writing software, with features designed for software development but somehow adapted to maths.

What about writing a standalone App DEDICATED to maths ?

If you think about it for a minute then you should realize that it's just an old argument about GUI vs. CLI. Of course many people will prefer to design some figure visually. And some powerful extensions can only be written using programming languages. I think we need both. It is just happens that creating a good visual UI is much harder than programming languages. Also, I don't think that many CS students take an art lessons.

I don't think I have *ever* seen a practical visual programming language. They never graduate past the "toy" stage. (That said, an in-browser verifier will probably be a "toy", so perhaps it's not a bad match.) But for the purpose of acclimating newbies to the ecosystem, you want it to resemble the "real thing", so that skills transfer. So maybe it should be an mmj2 clone?

Mario

 

[OlivierBinda]

Le 05/01/2020 à 15:57, Mario Carneiro a écrit :

On Sun, Jan 5, 2020 at 5:23 AM Olivier Binda <olus....@gmail.com> wrote:

Le samedi 4 janvier 2020 18:28:18 UTC+1, Mario Carneiro a écrit :

Looking at this from a green-field perspective, what should a web interface for metamath look like? 

I am also really really interested by the answer to this question.
Because I am trying to build one. 
My prototype will have to be refactored/improved because, I am 100% sure that I won't get it right on my first try.

But If I had, at least partial answers to this question, my first try would be much much better/closer to what is needed.

 Actually, from what I understand, I think Mephistolus is attempting to address a slightly different problem than what I'm talking about. You are interested in a (visual?) front end for metamath that is geared to the teaching of mathematics itself (correct me if I am wrong),

You are right about that. On my end, this is all about math (and not metamath/mm0) :

proof checking, reading, writing/authoring, researching, using, teaching, exporting to TeX/pdf/html/mp4/english/french/Japanese/chinese.

Ideally, I would like to abstract away the Metamath/Mm0 layer to make it as computer-representation agnostic as possible

while I am talking about how to provide an interface for people writing metamath "code".

I'm lost there. :)

Abstraction of the underlying representation helps a little bit in both cases, but hiding the textual representation away completely would not be a good idea

displaying the textual representation can be an option for power users

if the point is to teach a newbie what metamath is, since then the skills don't transfer.

* The metamath web pages are completely non-interactive, although they set the standard for proof visualization. I think things could be improved here if the page was rendered by JS, rather than shipping a bunch of giant html tags.

* The "structured version" looks great but the frequent mathjax causes some significant performance problems. I am doubtful that this can be kept up in an interactive setting, so we would have to use more ascii.

* If I recall correctly, Stefan O'Rear made a prototype web app that could load and display theorems from set.mm, but I don't think this project made it very far and in particular it was not interactive (allowing to write proofs, check individually, run tactics, save the results, etc).

MathJax renders math beautifully and it is possible to make it interactive, as I will demonstrate soon.

I'm sure it can. My main concern with use of mathjax is one of scale; mathjax rendering an average size metamath proof takes several seconds,

sure, but is it really problematic ?
I mean, MathJax is for the  human eyes, I don't know any human that needs to look at ALL the equations of a proof at the exact same moment to understand it.

Why can't you do it sequentially (with concurrency, for speeding up the process), like with paging or with drag to refresh scrolling  ?

What if we keep ascii for computers and svg/mathml for humans ?

which is over budget for an interactive editor. There are probably tricks you can play to improve this, but I see a difficult road here.

Modern web browsers are definitely up to the task of running a metamath verifier in JS, but I don't know a really successful user interface that we could apply here. Some observations:

MathJax is the only thing on earth NOW that enable interactive and beautifully rendered maths on a computer.
So, javascript (or typescript, or whatever is used to make MathJax work) is not an option. You have to somehow use javascript to build a decent math ui.

This sentence makes no sense. MathJax is implemented in javascript, so of course you could do the same thing mathjax does with javascript.

Except that MathJax renders to mathml or svg or html with css. So you need something that is able to display svg/html/css or mathml to display it.

Either you use a WebView or the native widgets of your platform (say android/ios/windows) or you have to develop something that can take the output of MathJax to render it (and having developed a widget in C++ that accepted parts of Html1 + CSS1 for the nintendo ds, I know how horrible this is)

So, the safest road is to use a WebView (that is C++ webkit or chromium adapted (with bridges) to use with your language of choice). And then, it makes sense to use javascript (or webasm for the computing heavy jobs...but I read somewhere that webasm was on par with javascript for dom related tasks)

But again this shows our differing goals. For teaching math, sure, mathjax away, but for teaching metamath you probably want to introduce people to the ascii symbols that are used to represent expressions,

Sure. It is what I started doing first (in preview 1), but as my long term goal is normal people, for preview 2, I switched from metamath to real math (which is harder).

If you only care for metamath/mm0/formal logic layer. It is much easier to implement an app.
you mostly only need a Text and a List widget. Really easy stuff.

But as there is a market for 100 people in the world for that,  I won't spend 3+ years of development to achieve that :)

because that's what appears in metamath files, and in all likelihood they will be typing these symbols when searching and writing proofs.

(even if you port MathJax to another language, you'll still need the dom and javascript...or you would need to rewrite the dom in your target language, good luck with that, 

or painfully port MathJax to another subsystem that the dom)

WASM covers this. You can write the core program in any language that compiles to wasm

yes

and use JS hooks for interaction with the web browser.

yes

Of course the program needs to be aware that it is running in a browser to some extent so it throws up the right interface.

yes :)

 

So you could write a complete standalone Methamath with UI application in javascript, 
or in a language that is able to speak with a WebView (like java, kotloin, c++...)

Right, that's the plan.

The UI requirement for a UI for metamath are somewhat low performance-wise: we do not need 60 fps at resolution 4K ^^

 
Javascript will do beautifully

Ha, you would be surprised how slow some frameworks can be.

Yeah. :)
And then, there are the tablet/phone platform with arm and slow processors, and flash for ram...

For sure, we have to keep an eye on performance...
Because nobody wants to use a slugish authoring tool.

On Sun, Jan 5, 2020 at 7:24 AM vvs <vvs...@gmail.com> wrote:

I am not sure that this is the right way to go, unless you want to convert the process of writing maths into the art of writing software, with features designed for software development but somehow adapted to maths.

What about writing a standalone App DEDICATED to maths ?

If you think about it for a minute then you should realize that it's just an old argument about GUI vs. CLI. Of course many people will prefer to design some figure visually. And some powerful extensions can only be written using programming languages. I think we need both. It is just happens that creating a good visual UI is much harder than programming languages. Also, I don't think that many CS students take an art lessons.

I don't think I have *ever* seen a practical visual programming language. They never graduate past the "toy" stage.

I would concur there. But I want to reproduce the math experience on a blackboard/paper.
And there has been 2000 years of development that turned this visual programming language into a killer tool.

I mean, to write a big complexe proof with mmj2, you have to do it on paper first and then you slowly convert it into a mm proof  until you hear the "DONG" that says it is finished ^^

spoiler :
in 3 weeks, I hope to be able to prove
|- ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) ) = ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) ) )

in about 20 visual moves involving like about 50 clicks and a few typed chars (I'll copy and paste the longer stuff ^^).
Without preparation on the paper, quicker than I can write it on paper.

(That said, an in-browser verifier will probably be a "toy", so perhaps it's not a bad match.)

The Jvm app does the proof check outside the browser so it is quite fast.
I'll see about the browser platform when I get there, but using wasm sounds to me like a really good advice for the computationaly intensive stuff

But for the purpose of acclimating newbies to the ecosystem, you want it to resemble the "real thing", so that skills transfer. So maybe it should be an mmj2 clone?

It cannot. Mephistolus and mmj2 work in too different ways.

mmj2 doesn't function like humans, which makes the preparation on paper part necessary.
You have to know where you want to go/end up with mmj2. This is impossible to use if you haven't been trained in maths

With Mephistolus, you just walk from what you have in the direction you want
and then, you see where you ended up. This make it usable by teenagers who do not understand maths (you'll see :p )

Also, you wisely said that implementing a text editor is a soul eating job.
I won't do that ^^

Olivier

ps : about CLI :
an authoring tool on CLI is not that good of an idea. But I see the point of a tool on CLI that transforms a proof and exports it to 50+ different human languages (like translating research papers...) or to Youtube/pdf/TeX
ot to a universal proof exchange format

Mario

 

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuzjPVLeCGK03D5CQ3O10tUyu%2BLm%3DE3o4GiiqEV6ZsZrg%40mail.gmail.com.

[vvs]

I don't think I have *ever* seen a practical visual programming language. They never graduate past the "toy" stage. (That said, an in-browser verifier will probably be a "toy", so perhaps it's not a bad match.) But for the purpose of acclimating newbies to the ecosystem, you want it to resemble the "real thing", so that skills transfer. So maybe it should be an mmj2 clone?

As I don't know what "practical" really means I couldn't argue with that. But I think that asserting that any productive use of computers (or Metamath) requires to explicitly learn a programming language is overly definitive. Where is the border between our different abilities to use intelligence? I know some people who are very serious about https://en.wikipedia.org/wiki/Unified_Modeling_Language. Though, I'm not necessarily share their views, but they exist nevertheless. And while my mother won't tell the difference between JavaScript and plain English, still she can use computers to solve her problems. Of course that's only possible because she actually used some languages and theories behind the scene, but the fact is that she doesn't have a clue how it really works.

Let's just say that personally I'd like to acquire abstract learning skills including many programming languages and mathematics, but that is not necessary for many practical tasks.

[David A. Wheeler]

On Sat, 4 Jan 2020 14:58:41 -0500, Mario Carneiro <di....@gmail.com> wrote:
> I thought about serving pre-parsed metamath files in e.g. JSON, but
> metamath is already pretty easy to parse, so there might not even be that
> much to gain through transforming the data.

Metamath format is extremely easy to parse, I suspect it would be simplest
just to use it as-is.

> Right, this is the main draw of "try it online" web apps: they lower the
> barrier to entry. Probably set.mm isn't even necessary for this purpose,
> since here you are mostly doing toy examples and a reduced or axioms-only
> set.mm would be an easy way to provide a decent standard library without
> much else.

That said, I think it *would* be awesome to have a useful
"zero install" tool for creating Metamath proofs.
It can be a pain to install tools; if users can skip that step entirely
that's one less barrier to entry. There are now many ways to
store nontrivial amounts of data from client-side JavaScript.

Please allow me to make a few comments about UI.
The big draw of *me* to mmj2 is that mmj2 lets people do
proofs going backwards, proofs going forwards, and even
speculative "in the middle" proofs of fragments or facts that
might be useful later. Some tools force you to go backwards,
and I find that to be a straightjacket.

The big negative of mmj2 is that it doesn't support much in
the way of tactics. Yes, it has a little automation built in, but
it doesn't have a system where users can easily define tactics
that build on other tactics that can then be invoked from the UI.
I'm not sure how to integrate that into a text editor like
interface, but it seems to be it'd be possible.
E.g., some sort of escape like a leading "!" that switches modes.

--- David A. Wheeler

[vvs]

I'm not sure how to integrate that into a text editor like
interface, but it seems to be it'd be possible.
E.g., some sort of escape like a leading "!" that switches modes.

Look how Jape did it: https://github.com/RBornat/jape/tree/master/dev/doc/manuals/roll_your_own

Though, it might be overly complex. The UI in Jape is friendly but the language is not. I wouldn't try to write my own tactic in it.

[Olivier Binda]

Just to correct something (I am often mistaken, please correct me when I am) :
Javascript/Webview may be bypassed with some a big amount of work, just not so herculean)...

Rendering math correctly and interacting with it is the main reason why I am stucking with a WebView/Javascript.

After a bit more of thoughts, making that happen on something other than a WebView is possible but would require : 
1) drawing on a canva/FrameBuffer
2) porting one input processor (the TeX input processor?) and the svg output processor/Jax of MathJax to another language (C ?)
3) writing a simple rectangular widget that is able to display the subset of svg that the output processor of MathJax use (mostly paths apparently) and to tally the bounding box of those paths/elements

Doing that would be a HUGE benefit, resource and performance wise (the more demanding part would be 2)
As well as allow everyone, everywhere to display/use maths

Sounds like a very interesting project to me....

Sadly I do not have enough time to do that, now. :)
Because that is the kind of fun and hard project that I just love indulging in ^^
Well, who knows, maybee in 3 years... :)


Also. An authoring tool for maths that write proofs in metamaths/mm0 somewhat make it into an authoring tool for metamath/mm0 too...
(but an imperfect one, as metamathiciens are concerned with the length of proofs and I do not yet see how Mephistolus could help with that. 
Mephistolus could complement with mmj2 though to allow metamathematicians to do what mmj2 cannot and the opposite)

Best regards,
Olivier