Re: [isabelle] polyml 4.2.0?



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





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