Re: [isabelle] polyml 4.2.0?

--- Makarius <makarius at> 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

> 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.)


Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 

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