Le 05/01/2020 à 15:57, Mario Carneiro a écrit :
On Sun, Jan 5, 2020 at 5:23 AM Olivier Binda <[email protected]
<mailto:[email protected]>> 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
<http://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 <[email protected]
<mailto:[email protected]>> 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 [email protected]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSuzjPVLeCGK03D5CQ3O10tUyu%2BLm%3DE3o4GiiqEV6ZsZrg%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CAFXXJSuzjPVLeCGK03D5CQ3O10tUyu%2BLm%3DE3o4GiiqEV6ZsZrg%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/c72f5e8e-e545-dc7e-d02c-3b56dfbc15d8%40gmail.com.
