Re: [isabelle] polyml 4.2.0?



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

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





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