Email Gateway (Aug 17 2022 at 14:46): Email Gateway (Aug 17 2022 at 14:46):From: C Y <smustudent1@yahoo.com>
Has anyone tried building Isabelle with the new 4.2.0 release of
polyml? I was able to build with the binary provided on the Isabelle
website but using 4.2.0 doesn't seem to work at all - do I need some
support libs in polyml?
Sorry for such an elementary question - I'm looking at putting together
an ebuild for gentoo linux and matters would be somewhat simplified if
4.2.0 worked, since the license on that release is LGPL.
Cheers,
Cliff Yapp
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
Email Gateway (Aug 17 2022 at 14:46):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
The 2005 release of Isabelle doesn't type-check with the 4.2 release of
PolyML as some library things changed. However PolyML4.1.4 is the same
as 4.2 with some small changes for backward compatibility. The CVS
version of Isabelle builds fine with PolyML 4.2
best,
lucas
C Y wrote:
Email Gateway (Aug 17 2022 at 14:46):From: Makarius <makarius@sketis.net>
Note that the Isabelle website offers a build with 4.1.4, which is an
internal downgraded version of 4.2.0. See the included README of the
polyml package for further details. Please ignore the other 4.1.4 version
on the source forge site of PolyML.
You can spend quite some time playing around with all these variants. We
have found that it is most convenient for users just to download plain
tar.gz files for Isabelle + PolyML + ProofGeneral, without system package
managers getting in the way.
Makarius
Email Gateway (Aug 17 2022 at 14:46):From: Makarius <makarius@sketis.net>
This sounds a bit strange to me -- users cannot be controlled like this.
Even more, all of this is free software, so people out there are free to
do what they want (ideally help other people to simplify their life).
Anyway, I suppose it is possible to produce Gentoo packages in the spirit
of the original Isabelle ones, while minimizing the potential for
surprise. (I've once seen a BSD port of Isabelle where everything was torn
to bits and pieces -- doc into /usr/share/doc, src into /usr/src etc. --
just to have a point to package things in the first place.)
By default, Isabelle expects everything at the same directory level as
itself (e.g. /opt/Isabelle2005, /opt/polyml, /opt/ProofGeneral), or within
its own contrib (e.g. /opt/Isabelle2005/contrib/polyml,
/opt/Isabelle2005/contrib/ProofGeneral etc.).
ProofGeneral can also go into some central /usr/lib/emacs place, but then
users are forced to that version -- emacs will ignore private ones! PolyML
setup has various traps and pitfalls, too, but I cannot recall all of them
on the spot.
Also note that some users have several Isabelle/PolyML/ProofGeneral
versions at the same time.
Makarius
Email Gateway (Aug 17 2022 at 14:46):From: Makarius <makarius@sketis.net>
On Sat, 24 Jun 2006, C Y wrote:
where everything was torn to bits and pieces -- doc
into /usr/share/doc, src into /usr/src etc. --
While I do not say that such reorganizations are never done arbitrarily,
there is normally a global operating system level organization policy
acting to dictate such locations.
Not quite so. If you look at the Linux File System Standard, for example,
it leaves the freedom for vendors to put everything in one place, such as
/opt/my-application or /usr/local/my-application. Then there is little
need to do extra packaging, of course.
In contrast Isabelle does expect certain things in certain positions
relative to its main directory (doc, src, lib, etc). The idea is that an
Isabelle installation is a single integral unit, not a collection of files
floating through the global file system.
Also note that some users have several Isabelle/PolyML/ProofGeneral
versions at the same time.Obviously, in a case such as that the packaging mechanisms are seldom
the best way to go.
So why bother at all? Why make simple things complicated anyway? With the
present tar.gz collection even non-root users can install as many Isabelle
versions in any place they wish.
Makarius
Email Gateway (Aug 17 2022 at 14:46):From: Martin Ellis <m.a.ellis@ncl.ac.uk>
On Saturday 24 June 2006 21:21, Makarius wrote:
ProofGeneral can also go into some central /usr/lib/emacs place, but then
users are forced to that version -- emacs will ignore private ones! PolyML
setup has various traps and pitfalls, too, but I cannot recall all of them
on the spot.
I think there's also an issue if the user decides to rebuild an Isabelle logic
with their own patches. If I understood/recall correctly, Isabelle favours
the heaps in the installation directory over the ones in the user's
~/isabelle directory.
For example, if there's a Pure logic build in both the install directory and
the user's home directory, then I think HOL will be built using the Pure in
the install directory as a basis.
Personally, Isabelle is about the only piece of software I don't like the idea
of trusting to a package manager anyway, but I can see how providing binary
packages might help people get started with Isabelle faster. However, it'd
probably only save < 1 hour of finding and following the installation
instructions. If the ebuild compiles from source, I suspect it'd take
somewhat longer than that to install.
Also note that some users have several Isabelle/PolyML/ProofGeneral
versions at the same time.
Not to mention emacs. :o)
Martin
Email Gateway (Aug 17 2022 at 14:46):From: C Y <smustudent1@yahoo.com>
--- Makarius <makarius@sketis.net> wrote:
On Thu, 22 Jun 2006, C Y wrote:
Has anyone tried building Isabelle with the new 4.2.0 release of
polyml? I was able to build with the binary provided on the
Isabelle website but using 4.2.0 doesn't seem to work at all -
do I need some support libs in polyml?Note that the Isabelle website offers a build with 4.1.4, which
is an internal downgraded version of 4.2.0. See the included
README of the polyml package for further details. Please ignore the
other 4.1.4 version on the source forge site of PolyML.
Ah! OK, that makes sense.
You can spend quite some time playing around with all these
variants. We have found that it is most convenient for users
just to download plain tar.gz files for Isabelle + PolyML +
ProofGeneral, without system package managers getting in the way.
The main reason I was asking is I was hoping to provide ebuild files
for Gentoo Linux. Gentoo is a bit uncommon in that the entire
distribution and all end user applications are normally built from
source. Traditionally Gentoo usually does its best to stay out of the
way of software authors, insofar as this is consistent with maintaining
a sane environment.
Would there be objection to creating ebuild files for Isabelle, if the
ebuild instructed the person installing the software that they should
not contact the Isabelle team with support issues related to the ebuild
install?
Cheers,
CY
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
Email Gateway (Aug 17 2022 at 14:46):From: C Y <smustudent1@yahoo.com>
--- Makarius <makarius@sketis.net> wrote:
On Sat, 24 Jun 2006, C Y wrote:
Would there be objection to creating ebuild files for Isabelle,
if the ebuild instructed the person installing the software that
they should not contact the Isabelle team with support issues
related to the ebuild install?This sounds a bit strange to me -- users cannot be controlled like
this. Even more, all of this is free software, so people out there
are free to do what they want (ideally help other people to
simplify their life).
I didn't mean to suggest controlling the users. This is done in (for
example) the e17 ebuild to inform the end users that the gentoo ebuilds
are not a supported method of installing the software and advising them
that the core development team may not wish to respond to bug reports
generated from the ebuild installed software. Of course, the user may
decide to raise a given issue anyway.
Of course, free software allows the freedom for many things. It is
usually a matter of courtesy to the original developers to consult with
them and respect their wishes in cases such as this. Unilateral action
seldom builds community spirit ;-).
Anyway, I suppose it is possible to produce Gentoo packages in the
spirit of the original Isabelle ones, while minimizing the
potential for surprise. (I've once seen a BSD port of Isabelle
where everything was torn to bits and pieces -- doc
into /usr/share/doc, src into /usr/src etc. --
just to have a point to package things in the first place.)
This was more probably done in order to allow Isabelle users to locate
documentation, src, and other components in the same top level
structured used by the vast majority of other software on the system.
While I do not say that such reorganizations are never done
arbitrarily, there is normally a global operating system level
organization policy acting to dictate such locations.
Possibly symlinking between standard OS level locations and standard
Isabelle locations would allow both to function, but that's just an
idea.
By default, Isabelle expects everything at the same directory level
as itself (e.g. /opt/Isabelle2005, /opt/polyml, /opt/ProofGeneral),
or within its own contrib (e.g. /opt/Isabelle2005/contrib/polyml,
/opt/Isabelle2005/contrib/ProofGeneral etc.).
OK, that explains its behavior when I installed it. It does pose a
difficult problem for packaging.
ProofGeneral can also go into some central /usr/lib/emacs place, but
then users are forced to that version -- emacs will ignore private
ones! PolyML setup has various traps and pitfalls, too, but I cannot
recall all of them on the spot.
proofgeneral is actually already available in the Gentoo ebuild system,
and polyml is installable in its 4.2.0 form (the ebuild has not yet
been made mainstream.) Hmm - it's a bit of a surprise that you can't
specify a specific location for the proofgeneral package. I'll have to
check into that.
Also note that some users have several Isabelle/PolyML/ProofGeneral
versions at the same time.
Obviously, in a case such as that the packaging mechanisms are seldom
the best way to go. It is actually possible to do this in Gentoo using
a slot mechanism, but I doubt it is worth that trouble. I was merely
hoping to make the "most current" Isabelle available for automatic
install (and more important, file tracking by the emerge system.) For
those doing serious development, package managers are usually a poor
fit. Perhaps for software like Isabelle there is little distinction
between user and developer? In any case, Isabelle's expectation of
having all activity at the same root level location does make packaging
problematic. Just out of curosity, what motivated that design
decision? Is the core Isabelle system itself changed by the
manipulations performed? (Sorry about my ignorance in such matters.
It's looking like this is a much more difficult problem than I had
anticipated, so I'll have to do some research first.)
Cheers,
CY
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
Email Gateway (Aug 17 2022 at 14:46):From: C Y <smustudent1@yahoo.com>
--- Martin Ellis <m.a.ellis@ncl.ac.uk> wrote:
On Saturday 24 June 2006 21:21, Makarius wrote:
ProofGeneral can also go into some central /usr/lib/emacs place,
but then users are forced to that version -- emacs will ignore
private ones! PolyML setup has various traps and pitfalls, too,
but I cannot recall all of them on the spot.I think there's also an issue if the user decides to rebuild an
Isabelle logic with their own patches. If I understood/recall
correctly, Isabelle favours the heaps in the installation directory
over the ones in the user's ~/isabelle directory.
Erm. Is this configurable?
For example, if there's a Pure logic build in both the install
directory and the user's home directory, then I think HOL will be
built using the Pure in the install directory as a basis.
Yes, that could pose a problem.
Personally, Isabelle is about the only piece of software I don't
like the idea of trusting to a package manager anyway, but I can
see how providing binary packages might help people get started
with Isabelle faster. However, it'd probably only save < 1 hour
of finding and following the installation instructions. If the
ebuild compiles from source, I suspect it'd take
somewhat longer than that to install.
The latter, pretty much by definition, is not an issue for Gentoo users
;-). Building a complete system, particularly with KDE and OpenOffice
installed, usually takes a couple of days.
As to the former, the major benefit of the emerge system is not
automatic installation (although that is a convenience) but the ability
to track all files associated with the core install of the software,
and the ability to cleanly and automatically remove old/upgrade to new
versions of said software. The case of root vs. user logic builds,
however, is a sticky one. Normal practice would be for the "builtin"
logic to be built and protected, and user experimentation on top of
that or replacing it would take place in a user directory. I gather
that it is normal for each researcher to have their own copy or copies
of Isabelle which are altered, and for there to be no "installed"
benchmark from which everyone diverges? (For instance, the way Firefox
has a core browser installed but each user may significantly alter its
behavior for themselves via config and plugin extensions?) This
definitely would explain the absence of most major proof software from
Gentoo and other distributions.
Anyway, sorry to cause all the fuss. If it works, it works. Certainly
the binaries seem functional on Gentoo in a "normal" install.
Cheers,
CY
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
Email Gateway (Aug 17 2022 at 14:46):From: Makarius <makarius@sketis.net>
Which means that there is no point to package Isabelle like this, because
it can be put into a single directory of the user's choice, and removed
with rm -rf.
So is there actually a problem you are trying to solve here, or is this
just the fun of playing with package managers? (I know this only too
well, because I used to entertain myself like this many years ago.)
Makarius
Email Gateway (Aug 17 2022 at 14:46):From: C Y <smustudent1@yahoo.com>
--- Makarius <makarius@sketis.net> wrote:
I guess you could say the "problem" I was trying to solve was providing
a convenient installation method for Isabelle within the framework of
the Gentoo system. My own experience with software outside the package
management system is somewhat mixed, as I have on more than one
occasion had "abandoned" programs hide for some time in isolated
directories and cause trouble when trying to run newer versions of the
same software. Or, on rarer occasions, a mistake on my part results in
the accidental corruption or removal of a user level tree in some
fashion. Also, binary only packages will age as core system libraries
are updated, eventually resulting in a non-working setup. (For
example, I cannot currently run Wolfram's MathReader.) All of these
situations can be avoided with a managed install in Gentoo, which not
only tracks the package but has an automated way to rebuild any
software that breaks as a result of an upgrade to some other library.
I grant that Isabelle might be a less logical prospect for package
management then most software - I am more accustomed to the model of
having a "core" set of functionality defined in a program which is
shared among multiple users and has the user specific
code/functionality/settings defined in the user directory. If Isabelle
doesn't have a logical "core" that should be protected/shared, that
does tend to make it a less attractive prospect. That also means I
need to make a much more careful study of how Isabelle works.
I seem to have stirred up a bit of a hornet's nest, for which I
apologize - that was not my intention. Mostly my thinking was that I
would like to see tools such as Isabelle in much wider use, and one way
to help might be to "incorporate" Isabelle as a standard package in
Gentoo. Isabelle looks to be one of the best tools in this particular
field of research, so it was a natural place to start. If there are
sound reasons for avoiding package management then that is no problem.
Cheers,
CY
Do You Yahoo!?
Tired of spam? Yahoo! Mail has the best spam protection around
http://mail.yahoo.com
Email Gateway (Aug 17 2022 at 14:47):From: Gerwin Klein <gerwin.klein@nicta.com.au>
No, it's the other way around. By default ~/isabelle/heaps is looked in first.
Cheers,
Gerwin
Last updated: May 03 2024 at 04:19 UTC