Email Gateway (Aug 23 2022 at 08:50): Email Gateway (Aug 23 2022 at 08:50):From: Manuel Eberl <eberlm@in.tum.de>
Dear AFP users,
AFP abstracts may now contain LaTeX formulae (both inline and display).
Rendering is done with MathJax and should work smoothly and consistently
in any remotely recent browser.
Formulae can simply be embedded using $…$ or and most basic LaTeX
maths commands are supported.
An example can be found in the example submission:
https://www.isa-afp.org/entries/Example-Submission.html
For more information on this, see the submission guidelines:
https://www.isa-afp.org/submitting.html
Should there be any issues, please let me know.
Enjoy!
Manuel
Email Gateway (Aug 23 2022 at 09:06):From: Makarius <makarius@sketis.net>
That is certainly an improvement.
At some point the standard Isabelle document output for HTML needs to be
improved analogously, but the underlying web technologies are still unclear to me.
Instead of old-fashioned MathJax, I've seen more and more activity around
KaTeX in recent years, but these guys are very modest in there version
numbering: https://github.com/KaTeX/KaTeX/releases
Here is some further comparison:
https://www.intmath.com/cg5/katex-mathjax-comparison.php
Makarius
Email Gateway (Aug 23 2022 at 09:06):From: Manuel Eberl <eberlm@in.tum.de>
On 09/05/2020 11:29, Makarius wrote:
At some point the standard Isabelle document output for HTML needs to be
improved analogously, but the underlying web technologies are still unclear to me.
Absolutely. I personally find those PDF documents that we produce at the
moment completely useless. They are not very readable and the arbitrary
restriction to A4 PDFs introduces arbitrary and nonpredictable line
breaks that make this even worse.
Ideally, I think, we would have heavily hyperlinked HTML where you can
click on stuff to get to the definition (like in Isabelle/jEdit), hover
to see information like types (like in Isabelle/jEdit), and have maths
rendered more nicely using LaTeX.
I also have been wondering for a while whether we should have something
like an optional "handwavy output mode", where things are printed in
more casual notation (e.g. integrals are just printed as integrals) with
no regard for ambiguities or lost detail – just to give the user a
better impression of what the "real" content of the statement is. This
might also make big goals more readable.
But setting this sort of thing up properly is going to be a lot of work,
and we would first need more sophisticated output options in
Isabelle/jEdit (which is probably also a lot of work).
Instead of old-fashioned MathJax, I've seen more and more activity around
KaTeX in recent years, but these guys are very modest in there version
numbering: https://github.com/KaTeX/KaTeX/releases
I don't really see what the big advantage of KaTeX is. Yes, it is
perhaps slightly faster, but not enough to make a big difference, in my
impression. Perhaps it becomes more pronounced if you really have a huge
number of formulae (as would be the case for HTML export). I also got
the impression that KaTeX is still somewhat experimental and does not
support everything that MathJax does.
Switching MathJax for KaTeX or whatever in the AFP should be fairly easy
if we should decide to do so in the future.
My personal opinion is that all these JavaScript-based solutions are
suboptimal because 1. they rely on JavaScript and 2. it takes a while
for the formulae to be rendered. A much better option would be
delivering them as MathML directly (which the AFP sitegen could produce
from the LaTeX statically), but unfortunately, very few browsers support
MathML well. So I fear MathJax etc. is the best solution for now.
Manuel
Email Gateway (Aug 23 2022 at 09:06):From: Makarius <makarius@sketis.net>
MathML is one of these technologies that "are continuously coming" and never
arrive. I still remember it from approx. 1992:
https://www.w3.org/Amaya/MathExamples.html
I wonder if there is a framework for mathematical documents that is a bit more
high-level, that we don't have to it again from basic principles.
Recently, someone pointed at https://dlmf.nist.gov/LaTeXML but it looks fairly
old-school at first sight.
In contrast, the really fancy things appear to be mostly based on JavaScript
frameworks.
Makarius
Email Gateway (Aug 23 2022 at 09:06):From: Manuel Eberl <eberlm@in.tum.de>
My impression was that it's already there. Firefox supports it extremely
well (that's why MathJax outputs MathML for Firefox). Safari's support
on the other hand is still not great, last I heard.
The other two big players, Google and Microsoft, decided not to support
it at all. Presumably such small companies simply do not have the
resources for such an endeavour.
As always, the best standards are useless if the dominant players
(Google especially) are against them.
(MathML is of course extremely verbose and can hardly be considered an
input format. But that's not really an issue, given that you can compile
to it – which is what MathJax already does. I just think it should
happen statically and not on the client every time you load the web page.)
Manuel
Email Gateway (Aug 23 2022 at 09:06):From: Makarius <makarius@sketis.net>
I am myself an old-fashioned Firefox user, although we see a gradual
monopolization towards Chromium.
Even MicroSoft Edge is following that:
https://support.microsoft.com/en-us/help/4501095/download-the-new-microsoft-edge-based-on-chromium
VSCode already has Chromium at the bottom.
The java-cef project promises to embed Chromium into a regular Java GUI
environment: https://github.com/chromiumembedded/java-cef
So there might be an indication, that everything could converge to the
Chromium rendering platform rather soon. But as usual, it requires careful
research of the technology / sociology / ideology.
Makarius
Email Gateway (Aug 23 2022 at 09:07):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
El 9/5/20 a las 06:44, Manuel Eberl escribió:
On 09/05/2020 11:29, Makarius wrote:
At some point the standard Isabelle document output for HTML needs to be
improved analogously, but the underlying web technologies are still unclear to me.
Absolutely. I personally find those PDF documents that we produce at the
moment completely useless. They are not very readable and the arbitrary
restriction to A4 PDFs introduces arbitrary and nonpredictable line
breaks that make this even worse.Ideally, I think, we would have heavily hyperlinked HTML where you can
click on stuff to get to the definition (like in Isabelle/jEdit), hover
to see information like types (like in Isabelle/jEdit), and have maths
rendered more nicely using LaTeX.
Indeed. I link the source code of my projects in a very primitive way
(by modifying the produced HTMLs, for example in here
<https://cs.famaf.unc.edu.ar/~pedro/forcing/Forcing/html/Forcing_Notions.html>).
This also alleviates the "pink screen" phenomenon (that you can't
Crtl-click on a definition of sources of the current running logic).I also have been wondering for a while whether we should have something
like an optional "handwavy output mode", where things are printed in
more casual notation (e.g. integrals are just printed as integrals) with
no regard for ambiguities or lost detail – just to give the user a
better impression of what the "real" content of the statement is. This
might also make big goals more readable.Another nice feature would be (un)folding sections. If you are writing a
sensible proof document (especially math), it would be desirable to be
presented with an "eagle's eye" view of proofs, understandable/palatable
by specialists, and with the possibility of diving into details by
unfolding. Actually, I do not know if Isabelle documenting capabilities
allow to select what depth of an argument is to be shown.
Last updated: Apr 24 2024 at 08:20 UTC