Re: [isabelle] Clone detection for Isabelle theories

Hi Johannes,

> 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?)

no, it is unsafe; yes, there is danger of code injection. Loading
Isabelle theories with libisabelle is equivalent to loading them into

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

To quote the paper:

"Isabelle/Isar is the surface syntax for Isabelle theories. Because it
is user-extensible, it is impossible to parse statically."

Due to the presence of arbitrarily complicated parse translations (inner
syntax) and syntax parsers (outer syntax) written in ML the syntactic
analysis of Isar is equivalent to the halting problem. In that sense
Isar is very much like Perl.


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