On Sun, 26 May 2013, Hendrik Tews wrote:
Hi,
the Proof General releases do always contain a symlink
ProofGeneral --> ProofGeneral-X.Y, which, ahem, is a bit in the
way when creating debian packages.
What is the reason for having this symlink in the tar archive?
As far as I can tell it is merely historic -- just like Debian packaging
is historic. It was once motivated by certain implicit conglomeration of
packages contributing to Isabelle in particular. So some interface
startup script would find an accidental "ProofGeneral" if that happened to
be in the right spot.
We do that quite differently these days, with explicit identification of
any add-on component involved, with unique name-version. Thus we avoid
"package hell" of the past (and the present in many traditional OS
distributions).
See also
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013/README_REPOSITORY
and
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013/Admin/components/README
This is inspired by the multi-platform "artifact" stores that are
ubiquitious these days, but without the huge bloat around it.
So Isabelle defines its own multi-platform "distribution" for logic-based
tools. Most of our users like that -- they don't even know that it is
there, since it just works. Traditional packagers don't like it at all,
but that is a different story.
Makarius
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
