[isabelle-dev] Admin/contributed_components

Alexander Krauss krauss at in.tum.de
Fri Jan 7 14:33:15 CET 2011


Makarius wrote:
> Can someone explain the exact meaning of Admin/contributed_components
> (cf. 573f557ed716 krauss, 3214c39777ab boehmes).
> 
> It looks like I will have to understand it for the release, but my 
> current collection of contrib components already deviates from that list.

The idea was to formalize to some extent the external components that 
are recommended/needed for working with a particular repository 
revision. Currently, the mira testing framework relies on this 
information to assemble a testable version from a bare-bones repository. 
  This is a bit less fragile and more faithful to the actual 
dependencies than just using some arbitrary 'current' version of the 
respective components.

Operationally, the testing tool first symlinks $ISABELLE_HOME/contrib to 
a configurable directory (/home/isabelle/contrib_devel in our central 
setup), and then links the subset of components that are actually 
present into $ISABELLE_HOME/etc/components.

The file can also be used by developers to make an informed guess on
how to get, e.g., sledgehammer to work when running repository versions.

I would expect that at a release, the content of this file in the tagged 
revision should coincide with what is actually shipped with Isabelle. 
The current content may not be completely adequate (e.g. 
scala-2.8.0-RC5), since I just made a guess based on what was in the 
last release.

Alex



More information about the isabelle-dev mailing list