Email Gateway (Aug 22 2022 at 13:49): Email Gateway (Aug 22 2022 at 13:49):From: Joachim Breitner <breitner@kit.edu>
Dear list,
we just had the final presentation this year’s installment of the
Isabelle course¹ in Karlsruhe. In their final reports, the students
gave feedback, and some of the feedback pertains the general Isabelle
ecosystem, which I’d like to share with your.
Some would have loved to have more tool support for style and
analysis, i.e. some form of linter, and better ways to query the
“call graph” of the lemmas.
Such tooling is of course tricky with Isabelle, partly because of
the “To parse Isabelle you need to run Isabelle” problem.
Some suggested that it would be nice to have the documentation
available as a website, and not just PDFs. Websites have the
advantage that they are searchable by Google & co, easily linkable,
and generally more accessible than the somewhat rigid PDF format.
I think this is a worthwhile suggestion and one that might be
doable, at least if the TeX code producing the PDF documentation is
structured well enough to be fed to one of the TeX-to-HTML-
conversion tools.
By the way: We had one group that solved the final task (for a given
while language with time-counting big-step-semantics,
prove determinism, implement constant folding and propagation (without
fixed-point iteration for WHILE), prove that to be totally semantics
preserving, time-improving, idempotent and type-preserving) in only 260
lines of code, compared to 500 in the example solution and ~1200 in the
typical solution. Very impressive!
Greetings,
Joachim
¹ http://pp.ipd.kit.edu/lehre/SS2016/tba/
signature.asc
Email Gateway (Aug 22 2022 at 13:50):From: Tobias Nipkow <nipkow@in.tum.de>
On 20/07/2016 11:00, Joachim Breitner wrote:
Dear list,
we just had the final presentation this year’s installment of the
Isabelle course¹ in Karlsruhe. In their final reports, the students
gave feedback, and some of the feedback pertains the general Isabelle
ecosystem, which I’d like to share with your.
- Some would have loved to have more tool support for style and
analysis, i.e. some form of linter, and better ways to query the
“call graph” of the lemmas.
At the end of a project the "unused_thms" command can be helpful to identify junk.
Tobias
Such tooling is of course tricky with Isabelle, partly because of
the “To parse Isabelle you need to run Isabelle” problem.
- Some suggested that it would be nice to have the documentation
available as a website, and not just PDFs. Websites have the
advantage that they are searchable by Google & co, easily linkable,
and generally more accessible than the somewhat rigid PDF format.I think this is a worthwhile suggestion and one that might be
doable, at least if the TeX code producing the PDF documentation is
structured well enough to be fed to one of the TeX-to-HTML-
conversion tools.By the way: We had one group that solved the final task (for a given
while language with time-counting big-step-semantics,
prove determinism, implement constant folding and propagation (without
fixed-point iteration for WHILE), prove that to be totally semantics
preserving, time-improving, idempotent and type-preserving) in only 260
lines of code, compared to 500 in the example solution and ~1200 in the
typical solution. Very impressive!Greetings,
Joachim
Email Gateway (Aug 22 2022 at 13:50):From: Lars Hupel <hupel@in.tum.de>
Hi,
yes, I also think that'd be great to have. Quite a while ago I tried the
various tools floating around the web but none of them worked well. (Not
sure whether the situation has changed.) I got the impression that it
might be better to produce HTML directly (given that we already have
"browser_info" files).
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:52):From: Makarius <makarius@sketis.net>
We are trying to move towards high-quality HTML presentation for about
10 years. The idea is to use the document structure of Isabelle + PIDE
markup directly, instead of LaTeX-to-HTML conversion.
With markup commands like 'chapter', 'section', 'text', and markdown
inside the text body + antiquotations there is very little left for
actual LaTeX. Maybe some advanced TeX math typesetting in rare
situations, where formal text typesetting of Isabelle is not sufficient.
At some point there might be a @{math} antiquotation for $...$, which
could be translated to HTML by MathJax.
Actually doing that reform of HTML document preparation will take an
unspecified time as usual: it might happen tomorrow in or 10 more years.
In the mean time, authors of Isabelle documentation can update their
sources to Isabelle markdown + antiquotations as much as possible. There
is still relatively much raw LaTeX in manuals that are not in my
responsibility.
Makarius
signature.asc
Email Gateway (Aug 22 2022 at 13:55):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
The Nitpick and Sledgehammer manuals are of course particular offenders in this area. The Sledgehammer manual is pretty short and should be relatively easy to port. It's on my list, but feel free to bug me again if it doesn't get done in a timely enough fashion.
As for Nitpick, the goal is to replace it with Nunchaku, so it might we better to leave the manual as is and wait until the tool is obsoleted. (Nunchaku will soon be integrated in the development Isabelle, in time for the next release, but it may take 1-2 more release cycles before Nitpick is effectively subsumed.)
As for the Nunchaku manual, I will write it in the modern style.
Jasmin
Last updated: Apr 23 2024 at 16:19 UTC