Re: [isabelle] Clone detection for Isabelle theories

On 07/13/2016 04:16 PM, Lars Hupel wrote:

> I'd like to announce the availability of a technology preview of code
> clone detection for Isabelle theories.


As far as I understood from the paper,
you are parsing source code with libisabelle,
which in turn requires a full Isabelle installation.
(Then - is parsing safe? Or is there danger of
code injection?)

I'd hope there is something like Language.Isabelle,
(just AST data type and parser - no semantics). cf.

very hypothetically - is there a formal Isabelle(Isar) grammar
from which AST representation and parser/printer (in Haskell)
could be generated (mostly) automatically?

Best regards, J. Waldmann.

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