Re: [isabelle] polyml 4.2.0?

--- Martin Ellis <m.a.ellis at> 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.


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.