[isabelle-dev] Standard component setup (Re: NEWS)

[Alexander Krauss]

On 01/04/2012 10:30 PM, Makarius wrote:
>> 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.

The idea behind Admin/contributed_components is to list the 
"recommended" versions that people should use unless they know better 
for some reason.

I added the hints about components to the HOWTO on the Wiki, which is 
becoming somewhat complete now.

https://isabelle.in.tum.de/isanotes/index.php/Working_with_the_repository_version_of_Isabelle

However, there is one open question:

- There is no stardard way of actually getting hold of the components. 
The HOWTO recommends reusing the ones from the last release, which is 
usually a good idea. However, some components do not come with the 
release (vampire, yices, jedit_build). Should we simply have a directory 
at TUM which is served via http and where developers can get components? 
Maybe simply serve /home/isabelle/contrib_devel for that (For 
jedit_build this should be unproblematic, but I am not sure about the 
licensing situation for the other stuff.)

> 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.

It seems that sledgehammer is not tested, since no ATPs are initialized. 
Maybe one should use the same strategy as in Mira: Symlink 
$ISABELLE_HOME/contrib to /home/isabelle/contrib_devel and activate all 
components from Admin/contributed_components that are actually found.

> How about the
> many variations on Predicate_Compile, code generator etc?

Good question. What are the further packages required here? (I heard 
some talking about Prolog a while ago, but how serious was it?)

Alex