Email Gateway (Aug 19 2022 at 12:02): Email Gateway (Aug 19 2022 at 12:02):From: René Neumann <rene.neumann@in.tum.de>
I'd like to disagree here. While Gentoo supports slotting (i.e. multiple
versions installed at once), only a few packages are slotted, and also
the slots might be too wide for certain uses (e.g. jdks are slotted by
5,6,7,... and not by minor version). Furthermore, depending on the
package, consumers might not work with multiple versions of a dependency
installed (cf slotting boost).
The same holds for configurations: A too restricted dependency (most
notable: needing to have a feature disabled) will quickly result in trouble.
So while Gentoo supports all those thing in theory, it would probably
not work out in practice.
Email Gateway (Aug 19 2022 at 12:04):From: Makarius <makarius@sketis.net>
These observations are consistent with my earlier guesses about the
culture and mindset of Gentoo packaging, or similar packaging communities.
Paradoxically, the "open-source bazaar" becomes centralized by the one big
arrangement of packages of a particular community (although there might be
ways to have alternative repositories, but this is again more complication
than necessary).
I see a fundamental conceptual problem here of operating system
distributions versus (against) application programs.
Moreover, I must confess that I am not very attached to a particular Linux
distribution nor its current brand, and tend to change the system
partiation quite often, while certain add-on applications remain happily
on /home. (This is out of necessity since no Linux version is really
stable these days.)
Interestingly, the Coq guys are presently discussing similar packaging
questions on the Coq-club thread "Package managing", e.g. see
https://sympa.inria.fr/sympa/arc/coq-club/2013-10/msg00096.html -- the
idea seems to be to delegate to OCaml package management (and thus become
subject to a particular INRIA-centric programming language world).
For Isabelle2013 and Isabelle2013-1-RC1 this privatized package management
is done in the weakest-possible sense: Isabelle "components" are bundled
with the one big application that you get from the Isabelle website.
There are no variants nor dependencies just one piece to be shipped, which
happens to be composed from a selection of parts according to the
specification in etc/components.
This tends to require a bit more disk space than necessary, but even just
one HOL image is already quite substantial compared to basic things like
Poly/ML or ATPs for Sledgehammer. Of course, JDK dwarfs everything else
and is as usual a problem on its own.
Using Isabelle professionally over some time, several GBs of disk space
can be easily filled with further heap images for the Isabelle
distribution, AFP, or other projects. This outperforms even JDK, despite
recent attempts of Oracle to inflate it again.
Makarius
Email Gateway (Aug 19 2022 at 12:23):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-10-09 15:29 Makarius:
On Wed, 9 Oct 2013, Christoph LANGE wrote:
Wouldn't it be easier to provide a *.desktop file instead? (See
https://wiki.archlinux.org/index.php/Desktop_Entries for documentation.)
I think these are widely understood across Linux desktop environments.I was trying that recently, but the freedesktop.org standardization
committee does not support the idea of relative paths in .desktop
specifications. See also
http://lists.freedesktop.org/archives/xdg/2011-June/011992.html
Oh, I see, I didn't know; thanks for pointing out.
Are you actually using Arch Linux yourself, or is the above URL just an
accident?
Neither. I'm using Gentoo Linux, but Arch Linux has an excellent online
documentation, and therefore that Arch wiki entry was the first good
reference I found on the *.desktop format.
I am just trying to tick major Linux fractions as "tested",
although for Arch everybody needs to start from scratch anyway in the
selection of packages so it is hard to test anything once and for all.
What do you mean? I thought that Isabelle, given its very specific Java
and jEdit dependencies, does not integrate well with package managers
anyway (i.e. maintainers can't easily provide an Isabelle package, which
would depend on some version of the distribution's Java and jEdit
packages), and that therefore the recommended way is to unzip the
all-in-one download, which brings its own dependencies. Which is what I
do (even though, in principle, I'd like the "package" approach better) –
and I haven't had any problems on Gentoo so far.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:23):From: Makarius <makarius@sketis.net>
OK, so I make a mental "tick" for Gentoo.
Note that the Isabelle "dependencies" are not very specific, we are just
trying to get things as stable as possible for end-users.
There is a fundamental flaw in the model of classic package management: 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.
At the start of the Isabelle/PIDE and Isabelle/jEdit project I was much
more naive about that, and was still supporting the idea that the user
provides some JDK via his base system, but no JDK is equaivalent to any
other one, not even of the very same version number. The same for other
contributing components, although to a lesser degree.
Historically, Proof General never got rock solid for everyone, because it
was impossible to bundle a particular version of Emacs -- both for
technical and social reasons. Isabelle/jEdit makes the critical cut at a
different boundary, and by bundling exactly one JDK the dimensions of the
problem space are much reduced.
Makarius
Email Gateway (Aug 19 2022 at 12:23):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-10-09 16:07 Makarius:
There is a fundamental flaw in the model of classic package management:
Good that you added "classic", …
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.
At the start of the Isabelle/PIDE and Isabelle/jEdit project I was much
more naive about that, and was still supporting the idea that the user
provides some JDK via his base system, but no JDK is equaivalent to
any other one, not even of the very same version number.
I acknowledge that this is a problem, and it probably can't be fixed, as
the Oracle JDK is non-free.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:23):From: Makarius <makarius@sketis.net>
On Wed, 9 Oct 2013, Christoph LANGE wrote:
2013-10-09 16:07 Makarius:
There is a fundamental flaw in the model of classic package management:
Good that you added "classic", …
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? 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.
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.
Since someone claimed something else recently on some Heise forum, I've
studied once again the license text: they mainly exclude changes to the
official directory layout, which already explains why packagers don't like
it. Oracle then also changed something recently that stops Linux
distributors, probably due to bad experiences in the past.
If Oracle really becomes evil at some point, we will have to sit down to
make our own shrink-wrapped compilation of OpenJDK.
Makarius
Email Gateway (Aug 19 2022 at 12:23):From: Makarius <makarius@sketis.net>
Wait, that was too fast. We still have this open issue to sort out:
https://bitbucket.org/isabelle_project/isabelle-release/issue/18/word-completion-by-keyboard-shortcut-ctrl
Makarius
Email Gateway (Aug 19 2022 at 12:24):From: Christoph LANGE <math.semantic.web@gmail.com>
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:
http://devmanual.gentoo.org/general-concepts/dependencies/ (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:
https://devmanual.gentoo.org/general-concepts/slotting/index.html
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.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:24):From: Makarius <makarius@sketis.net>
On Wed, 9 Oct 2013, Christoph LANGE wrote:
Please see:
for depending on specific version:
http://devmanual.gentoo.org/general-concepts/dependencies/ (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:
https://devmanual.gentoo.org/general-concepts/slotting/index.html
Thanks, I will study this further, just to know what is the current
approach in that camp.
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.
There are several problems coming together here, and the "open" model is
no solution either. Why does the open Linux Mint mess with its window
manager in a way that even its own version of OpenJDK does not work
properly? Searching the web for such incidents reveals tracker items that
are several years old and still open. (At least the openess of the
tracker helps to guess which workarounds can be applied on our side.)
Anyway, we should work out the Gentoo problem with C-B for explicit
completion in Isabelle/jEdit.
I have already learned something about Fedora 18/19 by getting to the
bottom of a completely different keyboard problem. For Gentoo it will be
more difficult, since I can't make my own installation of it in finite
time.
Makarius
Email Gateway (Aug 19 2022 at 12:24):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-10-09 17:00 Makarius:
Anyway, we should work out the Gentoo problem with C-B for explicit
completion in Isabelle/jEdit.
As I have just realised this may be a different problem than what I had
thought:
https://bitbucket.org/isabelle_project/isabelle-release/issue/18/word-completion-by-keyboard-shortcut-ctrl#comment-6401431
For Gentoo it will
be more difficult, since I can't make my own installation of it in
finite time.
Anyway, I'll be happy to test anything on Gentoo for you, maybe even
other users' problems, given precise instructions.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:24):From: Makarius <makarius@sketis.net>
OK, so we close the issue once more on the mailing list.
Note that Isabelle/jEdit tries to find a middle ground in providing
sensible defaults for theory editing and preserving original jEdit
behaviour.
For the completion I have added the "isabelle.complete" action and made it
the default for the C-B keyboard shortcut that was formerly
"complete-word". The corresponding menu item actually refers to the old
action. If you were actually using "complete-word" for its own merits,
you can invent new keyboard mappings to avoid the conflict.
The explicit mode of "isabelle.complete" does have some virtues that were
not there in Isabelle2013. It requires some practice to figure out its
dynamics (and options). It is essentially a computer game, but so far
with little documentation.
Makarius
Last updated: Apr 27 2024 at 04:17 UTC