Re: [isabelle] Report from our Isabelle course

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.


    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!


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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