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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
