Re: [isabelle] New AFP Feature: LaTeX formulae in abstracts

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:

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.