Re: [isabelle] polyml 4.2.0?



On Sunday 25 June 2006 07:08, Martin Ellis 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.
>
> 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.

No, it's the other way around. By default ~/isabelle/heaps is looked in first.

Cheers,
Gerwin





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