[isabelle] Clone detection for Isabelle theories
I'd like to announce the availability of a technology preview of code
clone detection for Isabelle theories.
This is the result of a Master's Thesis carried out by Dominik Vinan
under my supervision, with the help of Benjamin Hummel. Benjamin's
company is the vendor of ConQAT, an open-source software quality
assurance toolkit, for which the student has implemented an Isabelle
The purpose of code clone detection is simple: to find duplicated
specification or proof fragments in Isabelle theories.
I will present the tool and its accompanying paper at the Isabelle
Workshop in Nancy, but it is already possible to download and use it:
The bundle should contain all instructions for feeding theories into
ConQAT. It should work on macOS and Linux (no guarantees for Windows).
The result is an HTML report of detected clones which can be viewed in
If you try it out, please report any problems (or that you didn't have
problems) to me via mail so that the student and me can iron out bugs
This archive was generated by a fusion of
Pipermail (Mailman edition) and