Email Gateway (Aug 18 2022 at 16:19): Email Gateway (Aug 18 2022 at 16:19):From: Till Mossakowski <till@informatik.uni-bremen.de>
It is no problem to let Isabelle depend on sun-java6-jdk, this should
solve the jedit problem.
Best, Till
Email Gateway (Aug 18 2022 at 16:19):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
not really: sun-java6-jdk is not Free Software by Debian’s standards and
is shipped outside of Debian, in a special “non-free” repository. If
jedit (or a theoretical isabelle package) would depend on sun-java6-jdk,
then it would also be in non-free, even though it is free software.
A proper fix would be to find out what does not work with OpenJDK and
why, and fix it. But this is getting off-topic here.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:20):From: Till Mossakowski <till@informatik.uni-bremen.de>
Hi,
I think that these arguments are not ruling out an Ubuntu packaging of
Isabelle, and packaging has several advantages, like installation e.g.
within the Ubuntu Software center, and easier deinstallation.
Since we need Ubuntu packages for Isabelle for packaging the
Heterogeneous Tool Set (that interfaces with Isabelle), we will
continue to build them in Bremen (unless someone else provides them),
and are grateful for any hints (like the jedit/Java problem).
All the best,
Till
Email Gateway (Aug 18 2022 at 16:20):From: Lionel Elie Mamane <lmamane-isabelle.users.ml@conuropsis.org>
Not quite. The Ubuntu/Debian package uses:
automatically: the first it finds in the list:
OpenJDK Java6 JRE
Cacao JRE
Sun/Oracle Java6 JRE
(as long as they are installed in a way recognised by the
java-wrappers mechanism, for example through the Ubuntu/Debian
packages).
through manual override: any one (even not in this list, even one
not installed through packages) manually specified through one of
the JAVA_FLAVOR / JAVA_HOME / JAVA_BIN environment variables. See
man page java-wrappers in section 7 for details.
True, if you install the "jedit" package on a system that has neither
OpenJDK6 JRE, nor Sun Java6 JRE, it will by default install
OpenJDK6 JRE. But if you install (or select for installation) Sun Java6
JRE first, then installing jedit will not install OpenJDK6 JRE.
Besides, I'm curious what doesn't work with jEdit using OpenJDK. I
installed it, with all default options (so OpenJDK Java6 JRE):
I installed the "accents" plugin, tried some strings it was
supposed to substitute, it did substitute them.
I installed the "FTP" plugin, works with SFTP protocol (open file,
change, save).
The Python Shell plugin evaluates "print 2+2" to displaying "4" in
the Console.
Email Gateway (Aug 18 2022 at 16:20):From: Makarius <makarius@sketis.net>
After actually using it for 10min or so, you should notice many annoying
details on OpenJDK. E.g. with certain fonts (such as IsabelleText) at
certain sizes you get erratic lines painted right into the main TextArea.
Moreover the metrics of many GUI elements are just strange. Moreover the
portable Nimbus look and feel from Sun is missing, which is really
required to avoid ugly "Java-style" look and feel. Moreover antialiasing
of the caret and thin lines is very bad. Moreover ...
Just last week some further issues were mentioned on the jedit-dev mailing
list again, and some main developers confirmed that they don't support it.
I did investigate this further some months ago. OpenJDK lacks many
fundamental things, such as a proper Graphics2D implementation. Maybe
when (or if) OpenJDK 7 comes it it will be usable.
Makarius
Email Gateway (Aug 18 2022 at 16:20):From: Makarius <makarius@sketis.net>
That is a lot of complication introduced by the packaging. So what is the
point of it?
Isabelle does not need "installation" nor "uninstallation". You just run
it, or delete it if you are unsatisfied.
Makarius
Email Gateway (Aug 18 2022 at 16:20):From: Ian Lynagh <igloo@earth.li>
On Sun, Nov 28, 2010 at 02:39:23PM +0100, Makarius wrote:
That is a lot of complication introduced by the packaging.
I don't follow you.
So what is the point of it?
It's a lot easier to "apt-get install isabelle" than it is to find
where to download it, download it, work out how to install it (even if
that does turn out to be "just untar it"), add it to my path, etc
I can be sure that packaged software is actually going to work on my
machine, e.g. it won't fail because my glibc is far too old or far too
new. Similarly, I won't have to spend time working out what
dependencies I need to install.
You may say that the first of these represents a small amount of effort
in the grand scheme of things, and that if you put in the little effort
then you find that the second isn't a problem - and you would be right
on both counts - but I spent a year using coq before I even downloaded
Isabelle because of this.
Some other factors:
If something is in Debian then I can be pretty sure it really is Open
Source software
Packaged software is more likely to "fit in" with the rest of the
system, e.g. docs where I expect them
Packaged software is more likely to be "well-behaved"
Packaged software often does things better than upstream - most
commonly where two pieces of software can integrate
Isabelle does not need "installation"
Yes it does. "wget ...; tar -jxf ..." is installation just as much as
"apt-get install ..." is.
Thanks
Ian
Email Gateway (Aug 18 2022 at 16:21):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
may I amend this point with something relevant especially to Isabelle:
Isabelle is an research tool and consequently will appear in university
courses (this is where I learned about it). For that it has to be
installed on computer pool computers, and the admins of these pools will
be very happy to just add the name of a package to a configuration file
than having to write scripts that download tarballs, extracts them etc.
The current installation effort is small if you plan to be a heavy user
of Isabelle that will spend hours and hours proving stuff. But it is
high if you are an admin who has to maintain lots of machines and
packages, or just a curious user who would like to have a quick look on
the software.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:21):From: Makarius <makarius@sketis.net>
On Sun, 28 Nov 2010, Ian Lynagh wrote:
- It's a lot easier to "apt-get install isabelle" than it is to find
where to download it, download it, work out how to install it (even if
that does turn out to be "just untar it"), add it to my path, etc
So which version of Isabelle is the "isabelle" package? You do need to be
able to use several Isabelle versions at the same time in parallel.
Personally I also find the apt-get business very strange and hard to use.
It is always like looking many years back in the history of computing.
Synaptic is a bit better, but hardly 100% success.
- I can be sure that packaged software is actually going to work on my
machine
This is simply not the case. Many Debian packages are broken, like the
jEdit one I mentioned. Once I wanted to give Axiom a quick try, and its
Debian/Ubuntu package was really bad, so I did a quick compile from
sources again at it just worked out of the box.
- Packaged software is more likely to "fit in" with the rest of the
system, e.g. docs where I expect them
You mean READMEs in .gz format?
Isabelle expects its documentation in a certain place, but not where
Debian has it.
- Packaged software often does things better than upstream - most
commonly where two pieces of software can integrate
Do I have to mention the OpenSSH debacle?
Makarius
Email Gateway (Aug 18 2022 at 16:21):From: Makarius <makarius@sketis.net>
In fact, our tar.gz bundles are exactly made for this situation, where you
have the typical mixture of several different architectures and operating
system versions sharing one file space. The platform identifiers within
the Isabelle directory structure make this very convenient.
Here the distribution-specific packaging would get in the way, unless you
assume a Debian only universe.
Makarius
Email Gateway (Aug 18 2022 at 16:21):From: Ian Lynagh <igloo@earth.li>
On Sun, Nov 28, 2010 at 05:04:53PM +0100, Makarius wrote:
On Sun, 28 Nov 2010, Ian Lynagh wrote:
- It's a lot easier to "apt-get install isabelle" than it is to find
where to download it, download it, work out how to install it (even if
that does turn out to be "just untar it"), add it to my path, etcSo which version of Isabelle is the "isabelle" package?
One that works.
You do need to be able to use several Isabelle versions at the same
time in parallel.
Oh no I don't.
Now a power user's needs might not be served by the version in their
distro. They might need to use a recent development version, for
example. But new users have much simpler needs.
In fact, I started using coq trunk several months before downloading
Isabelle too, having started using the packaged version and then finding
I wanted some recent new features and bug fixes.
Something else I should have mentioned: I am reluctant to start writing
proofs with Isabelle that I ultimately want to share, because I know
that the people I want to share them with are much less likely to be
bother if the barrier to getting started is higher than "apt-get install
isabelle; isabelle myProof".
- I can be sure that packaged software is actually going to work on my
machineThis is simply not the case.
s/sure/more confident/
Many Debian packages are broken, like the
jEdit one I mentioned. Once I wanted to give Axiom a quick try, and its
Debian/Ubuntu package was really bad, so I did a quick compile from
sources again at it just worked out of the box.
I've never tried either of those, but broadly speaking my machine is the
same as the package maintainers, and it presumably works for the
maintainer, so it's likely to work for me.
I'm far more likely to have problems with a binary compiled on some
version of RedHat, when I try to use it on some version of Debian.
Or trying to compile some software on Linux when the maintainer uses
Solaris.
- Packaged software is more likely to "fit in" with the rest of the
system, e.g. docs where I expect themIsabelle expects its documentation in a certain place, but not where
Debian has it.
Then an Isabelle package might move the docs to where they should be on
Debian systems, and update Isabelle accordingly. Perhaps adding a
configure flag so the location is configurable.
Or alternatively, it might put a symlink from one place to the other.
Or it might be as simple as a README (in the normal place) explaining
how to find the documentation. It depends what fits the package best.
Thanks
Ian
Email Gateway (Aug 18 2022 at 16:21):From: Makarius <makarius@sketis.net>
On Sun, 28 Nov 2010, Ian Lynagh wrote:
I've never tried either of those, but broadly speaking my machine is the
same as the package maintainers, and it presumably works for the
maintainer, so it's likely to work for me.
The whole confusion seems to be based on a general disagreement of what
"works" actually means.
Or it might be as simple as a README (in the normal place) explaining
how to find the documentation. It depends what fits the package best.
Again these extra complications due to packaging. Hopeless.
Makarius
Email Gateway (Aug 18 2022 at 16:22):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
I think it would be just as difficult to construct packages that could
be relied upon to work on your machine as it is to get Isabelle working
on your machine under the present situation.
Your theory files have to be correct for (say) Isabelle 2007 (Isabelle
2005 and Isabelle 2008 are significantly different). For Isabelle 2005
you have to run PolyML 4.1.4, not PolyML 5.x - subsequent versions of
Isabelle work with certain versions of PolyML only. And although I have
Isabelle 2005 working with my theory files with PolyML 4.1.4 on (I
think) five machines,
it won't work on some other machines (possibly because of the machine
architecture).
On this latter point - can anyone help ? I'm wondering if the problem
is that I'm now trying to get it (ie, Isabelle 2005 on PolyML 4.1.4)
working on a different machine which is a 64-bit machine - does this
require a different version of PolyML 4.1.4 ? Is there such a version
available ?
Thanks for any help,
Jeremy
Email Gateway (Aug 18 2022 at 16:22):From: Makarius <makarius@sketis.net>
Did you see this explanation how to revive really old Isabelle versions
with current SML/NJ?
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-November/msg00013.html
Makarius
Email Gateway (Aug 18 2022 at 16:32):From: "Edward Z. Yang" <ezyang@MIT.EDU>
Hello all,
I was hoping to install Isabelle on my machine but winced when I saw the
following instructions:
tar -C /usr/local -xzf Isabelle2009-2_bundle_x86-linux.tar.gz
And I was wondering if Isabelle had been packaged up for any of the major
distros with the collaboration of the Isabelle authors (since "Pre-packaged
versions of Isabelle, Poly/ML, and Proof General floating through the Net as
deb, rpm, port etc. are often outdated and rarely work as advertised.")
Packaged software confers a number of notable benefits (uninstallability,
ease of installation, upgrade facilities).
Thanks,
Edward
Email Gateway (Aug 18 2022 at 16:32):From: Christian Maeder <Christian.Maeder@dfki.de>
Hi,
for our hets project we've packaged Isabelle for Ubuntu
(without the collaboration of the Isabelle authors, though).
http://www.dfki.de/sks/hets
https://launchpad.net/~hets/+archive/hets
You should be able to get it via:
sudo apt-add-repository ppa:hets/hets
sudo apt-get update
sudo apt-get install isabelle
HTH Christian
Email Gateway (Aug 18 2022 at 16:32):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
there has been an attempt to integrate Isabelle into Debian:
http://bugs.debian.org/494491
and at the bottom¹, an explanation why this has failed is given:
„to make a long story short: the Isabelle developers strongly prefer to
have only one official Isabelle distribution and, thus, do not
encourage Isabelle distribution by others. Moreover, they prefer to
provide the whole "Isabelle suite" (i.e., Isabelle and all surrounding
tools (Poly/ML, Proof General, Scala, e, spass, jedit, etc) as one
integrated bundle. Of course, this "bundling requirement" makes is
hard (if not impossible) to integrate properly into Debian.“
If this is wrong or has been changed, I would could imagine to try to
package Isabelle myself, but not without the good will of the Isabelle
developers.
Greetings,
Joachim
¹ http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=494491#44
signature.asc
Email Gateway (Aug 18 2022 at 16:32):From: Makarius <makarius@sketis.net>
On Wed, 24 Nov 2010, Edward Z. Yang wrote:
I was hoping to install Isabelle on my machine but winced when I saw the
following instructions:tar -C /usr/local -xzf Isabelle2009-2_bundle_x86-linux.tar.gz
The /usr/local is indeed a bit old-fashioned here, but the instructions
also say that this is just an example. There is in fact no "installation"
of Isabelle. You just put it anywhere an run it. This trend will
continue further in the coming years, as more and more ad-on components
are required. It will also become increasingly difficult for third
parties to do correct packaging.
And I was wondering if Isabelle had been packaged up for any of the
major distros with the collaboration of the Isabelle authors (since
"Pre-packaged versions of Isabelle, Poly/ML, and Proof General floating
through the Net as deb, rpm, port etc. are often outdated and rarely
work as advertised.") Packaged software confers a number of notable
benefits (uninstallability, ease of installation, upgrade facilities).
Packaging was one of my hobbies many years ago. Around 2000 I made an rpm
of Isabelle for SuSE (probably also for Redhat). This did not solve any
problems, so the game was discontinued.
If you look at Mac OS X, the self-contained .app bundling works much
better than package management, even though you need a bit more disk
space. The recent trend of "portable" applications for Windows (for USB
sticks etc.) go in the same direction.
No "installation" means no problems of "uninstallation".
Makarius
Email Gateway (Aug 18 2022 at 16:32):From: Makarius <makarius@sketis.net>
It is still right and has changed only slightly in the sense that the
trend towards fully integrated bundling will become even stronger. With
our more recent move towards full dependency on JVM 1.6, for example, it
has become practically impossible to rely on existing Java packaging.
Just take plain jEdit (without Isabelle): the Ubuntu/Debian package uses
OpenJDK on that platform and then fails to deliver an application that
actually works, because jEdit requires JDK/JRE from Sun/Oracle.
This is why I always download jEdit from www.jedit.org directly and use it
with Java from http://www.java.com/en/download/index.jsp, although I know
that this is heretical.
Makarius
Email Gateway (Aug 18 2022 at 16:33):From: "Edward Z. Yang" <ezyang@MIT.EDU>
Thanks for all of your responses. I did notice that the packaged binaries
seemed a bit large, and if Isabelle is shipping with all of its dependencies,
that explains it, and also explains why there's no packaging.
As several people pointed out, Isabelle can be run directly from the downloaded
tarball. That will work quite well for my purposes.
Cheers,
Edward
Last updated: Apr 25 2024 at 20:15 UTC