Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] MathJax


view this post on Zulip Email Gateway (Aug 18 2022 at 17:56):

From: Gerwin Klein <gerwin.klein@nicta.com.au>
They look pretty good! The first solution I've seen that isn't somehow hugely clunky.

Cheers,
Gerwin

view this post on Zulip Email Gateway (Aug 18 2022 at 17:57):

From: Steven Obua <steven.obua@googlemail.com>
Yes, this look extremely impressive!

view this post on Zulip Email Gateway (Aug 18 2022 at 18:00):

From: Jason Dagit <dagitj@gmail.com>
I've had pretty decent success using Hevia to convert Isabelle's latex
to HTML. I just had to define the right class files. I should dig
that stuff out again and share it with people here. I bet there would
be some interest. My goal was to make a website like the real-world
haskell book website that converted literate isabelle to a webpage
where people could leave paragraph level comments. I had a working
prototype but it was a little rough around the edges still (no css for
example).

Jason

view this post on Zulip Email Gateway (Aug 18 2022 at 18:00):

From: Slawomir Kolodynski <skokodyn@yahoo.com>
I replaced jsMath with MathJax recently on the the isarmathlib.org site (a web presentation of IsarMathLib). It looks better and renders much faster than jsMath. MathJax is also simpler to use - there is no need to install anything on the server. Just a couple of lines in the head and of course LaTeX markup on the page.

Slawomir Kolodynski

http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

view this post on Zulip Email Gateway (Aug 18 2022 at 18:01):

From: Makarius <makarius@sketis.net>
It would be certainly worth sharing it. Right now our Google Summer of
Code student Peter is working on direct HTML generation from the Isabelle
sources, also re-using some ideas from Hevea.

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 18:01):

From: Jason Dagit <dagitj@gmail.com>
Interesting. I hadn't heard that you have a summer of code student or
about this project. Were announcements sent somewhere and I just
missed it? I'd love to put details up on the isabelle subreddit
(increase visibility for people who don't read the list).

Thanks,
Jason

view this post on Zulip Email Gateway (Aug 18 2022 at 18:01):

From: Makarius <makarius@sketis.net>
There was a very brief (implicit) announcement on isabelle-dev:

http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg01470.html

The connection of documents within the Prover IDE and XHTML/CSS generation
is based on the observation that the latter appears to be the only format
that can be reasonably well renderen on the JVM/Swing platform with full
hyperlinks etc.

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 18:07):

From: Sascha Boehme <boehmes@in.tum.de>
Hi,

There is some new technology to integrate math (formulas) into
webpages:

http://www.mathjax.org/

It requires only HTML/CSS/Javascript on the client-side and thus runs
in all modern browsers without fancy plugins.

This may be a technology to build upon when setting up an
Internet-based interface to Isabelle.

Cheers,
Sascha


Last updated: Mar 28 2024 at 20:16 UTC