[isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS

Makarius makarius at sketis.net
Mon Jul 16 11:34:25 CEST 2012


On Sun, 15 Jul 2012, Alexander Krauss wrote:

> Jasmin Christian Blanchette wrote:
>> What is an official component? Among the Nitpick/Sledgehammer/SMT
>> components, "vampire-1.0" and "yices-1.0.28" are not to be
>> redistributed (due to their license) and have never been part of an
>> official Isabelle release. (Sascha and I do use them for evaluations,
>> though.)
>
> As I said, "official" does not imply "redistributable". Rather, it means 
> that the packages may participate in the integration with isatest/mira 
> (the setup of the two tools will converge in this respect).

So "official" could be defined as "mentioned in some version of 
Admin/components from the latest Isabelle tip back 1-2 years into the 
past".

Thus these components will be available for tools or users to use them in 
bisection, for examples.


 	Makarius




More information about the isabelle-dev mailing list