On Sun, 26 May 2013, Hendrik Tews wrote:


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.


ProofGeneral-devel mailing list

Reply via email to