Re: [isabelle] *.desktop entries and Arch packages [Re: Isabelle2013-1-RC2 available for testing]

2013-10-09 16:33 Makarius:
> On Wed, 9 Oct 2013, Christoph LANGE wrote:
>> 2013-10-09 16:07 Makarius:
>>> it makes equivalence classes of components of the same base name:
>>> "java", "jedit", "polyml" etc. and does not support precise dependencies
>>> on particular versions, or depencies on particular configurations of
>>> certain software components, or multiple such configurations at the same
>>> time without interfering.
>> … because Gentoo and some other distributions support all of these.
> I am not sure about this.  It depends both on technical side-conditions
> and the mindset of packagers.
> Can I have many versions of the same application at the same time?

Sure – trust an experienced Gentoo user writing this email.

Please see:

* for depending on specific version: (section
"Version Dependencies")

* for depending on a specific configuration of a package: same page
(section "Built with USE Dependencies") – the package depended on needs
to have the given configuration feature prepared as a "USE flag", but
that's the case with most widely used packages.

* for multiple versions of a package at the same time:

> Both
> for Isabelle and Coq, real users do this routinely, but the packagers
> don't support it.  Even just getting a recent version of some
> application is a problem, without subscribing to some continous-update
> model of the operating system.

Being _recent_ is a problem.  In the Gentoo practice it depends a lot on
the individual packages and their maintainers.  Most packages in the
core package repository are fairly recent, recent versions of some
others are only available from third-party package repositories (which
one can, however, access easily), and some packages are not available at
all in a recent version.

>> I acknowledge that this is a problem, and it probably can't be fixed,
>> as the Oracle JDK is non-free.
> This is another old argument, and the side-conditions have changed
> several times, sometimes this way sometimes that way.  I still don't
> quite understand why Oracle JDK is called non-free.

Maybe I did injustice to Oracle, but as you said that "no JDK is
equaivalent to any other one, not even of the very same version number"
I thought that's probably a typical symptom of a software package with,
let's say, a non-open communication model.



Christoph Lange, School of Computer Science, University of Birmingham, Skype duke4701

→ Mathematics in Computer Science Special Issue on “Enabling Domain
  Experts to use Formalised Reasoning”; submission until 31 October.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.