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
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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and