[isabelle-dev] NEWS

Makarius makarius at sketis.net
Wed Jan 4 22:30:50 CET 2012


On Wed, 4 Jan 2012, Florian Haftmann wrote:

>> BTW "Nitpick_Examples" should have been failing all over the place. If 
>> they haven't, this indicates that neither of your two setups (macbroy2 
>> and local machine) have Kodkod enabled.

> Is there any reference to these details on some documentation (README, 
> manual, …)?  A grep for Kodkod over the sources did not look very 
> promising.

A good starting point is the semi-official Admin/contributed_components 
file, which seems to be also used officially for Mira tests.  It documents 
potentially relevant external components for tests.  The versions given 
there are not necessarily the latest ones, but the simplest ones to 
install from the last official release bundle (directory contrib/).

Eg. version edd50ec8d471 of the file still refers to 
contrib/scala-2.8.1.final from Isabelle2011-1, although the "latest" 
snapshots already uses scala-2.8.2.final, while the next release will 
potentially move forward to scala 2.9.x -- just the usual entertainment.


More specific information about isatest settings is in 
Admin/isatest/settings/, but that is much less comprehensive.  I can't say 
myself on the spot if every add-on is really tested.  How about the many 
variations on Predicate_Compile, code generator etc?


 	Makarius


More information about the isabelle-dev mailing list