[isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS

[Alexander Krauss]

Alexander Krauss wrote:
> * Integrity of this directory is ensured by a cron job which compares
> the output of "sha1sum /home/isabelle/components/*" with a file in
> the Admin section of the Isabelle repository. So we can easily detect
> accidents (and revert them, possibly with the help of the standard
> backups).

See now 387ed2f30918 for the script and initial state.

To add a new component/version:
- copy the tarball to /home/isabelle/components
- in some clone of the repository, run
     Admin/component_repository/checksum -u
- check the result with "hg diff" (the checksum of the new file should 
be added to the diff)
- commit and push the result

Jasmin Christian Blanchette wrote:
> What is an official component? Among the Nitpick/Sledgehammer/SMT
> components, "vampire-1.0" and "yices-1.0.28" are not to be
> redistributed (due to their license) and have never been part of an
> official Isabelle release. (Sascha and I do use them for evaluations,
> though.)

As I said, "official" does not imply "redistributable". Rather, it means 
that the packages may participate in the integration with isatest/mira 
(the setup of the two tools will converge in this respect).

I now added vampire and yices as well (while keeping them private to TUM 
as before), reflecting the previous situation in mira.

> For the others, please use
>
>      cvc3-2.4.1 (from http://www21.in.tum.de/~blanchet/cvc3-2.4.1.tar.gz)
>      e-1.5
>      kodkodi-1.2.16
>      spass-3.8ds
>      z3-4.0 (from http://www21.in.tum.de/~blanchet/z3-4.0.tar.gz)

Ok. I updated the versions in Admin/components accordingly (429fab105d99).

Now the following tarballs are still missing:
* scala-2.9.2
* ProofGeneral-4.1
* jdk-6u31

Alex