[isabelle-dev] Standard component setup (Re: NEWS)
krauss at in.tum.de
Thu Jan 5 09:36:19 CET 2012
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
> 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.
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?)
More information about the isabelle-dev