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 Â http://pp.ipd.kit.edu/lehre/SS2016/tba/
Description: S/MIME Cryptographic Signature