You may find that the release version of PolyML 5.6 doesn’t work with the development version of HOL4. If you experience any problems then try the fixes branch of Poly/ML:
https://github.com/polyml/polyml/tree/fixes-5.6 For example, you can do $ git checkout fixes-5.6 after cloning the Poly/ML repository. Anthony > On 24 May 2016, at 09:47, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote: > > PolyML 5.6 is supported by the development version of HOL4 (i.e., the head of > the master branch), and has been for a while. > > On 24 May 2016 at 18:39, Chun Tian (binghe) <binghe.l...@gmail.com> wrote: > Hi all, > > But still, PolyML 5.6 is not supported yet, right? I have to use latest Poly > ML 5.5.x to build HOL4 (Git master) on Mac OS X. > > Regards, > > Chun Tian (binghe) > University of Bologna > > On 24 May 2016 at 07:29, Thomas Tuerk <tho...@tuerk-brechen.de> wrote: > Hi Michael, > > thanks. That did the trick. The new libraries were installed there, but > the old ones were still in there causing trouble. Anyhow, purging the > old ones solved the issue. > > Many thanks > > Thomas > > On 24/05/16 07:23, Michael Norrish wrote: > > It looks to me as if you have a very old libpoly installed in > > /usr/local/lib (or perhaps somewhere else on your LD_LIBRARY_PATH). I'd > > guess that you need to purge those files (and make sure that the 5.6 > > library files end up there as well). > > > > Michael > > > >> On 24 May 2016, at 14:50, Thomas Tuerk <tho...@tuerk-brechen.de> wrote: > >> > >> Hi all, > >> > >> I have a problem installing HOL 4, which is puzzling me. It would be > >> great if someone had a idea how to help me. > >> > >> I wanted to update my HOL 4 installation. I had an old PolyML installed > >> and got the error message that at least version 5.5.1 is needed. So, I > >> installed the latest version 5.6 and then ran > >> > >> poly < tools/smart-configure.sml > >> > >> I got a strange error message. I also tried with versions 5.5.2, 5.5.1 > >> with same effect: > >> > >> ----------------------------------------------------- > >> Poly/ML 5.5.1 Release > >> > >> HOL smart configuration. > >> > >> Determining configuration parameters: holdir OS poly polymllibdir > >> OS: linux > >> poly: /usr/local/bin/poly > >> polyc: /usr/local/bin/polyc > >> polymllibdir: /usr/local/lib > >> holdir: /home/thtuerk/HOL > >> DOT_PATH: /usr/bin/dot > >> > >> Configuration will begin with above values. If they are wrong > >> press Control-C. > >> > >> Will continue in 1 seconds. > >> > >> Loading system specific functions > >> Compiling system specific functions (sml) > >> Beginning configuration. > >> Making mllex > >> Making mlyacc > >> > >> The exported object file has version 5.51 but this library supports > >> 5.10-5.50 > >> Failed to make mlyacc > >> ----------------------------------------------------- > >> > >> Does anyone have an idea library this error message is about? I briefly > >> started debugging, but have not put much time into it yet? Has anyone > >> encountered this problem before. > >> > >> Best > >> > >> Thomas Tuerk > >> > >> ------------------------------------------------------------------------------ > >> Mobile security can be enabling, not merely restricting. Employees who > >> bring their own devices (BYOD) to work are irked by the imposition of MDM > >> restrictions. Mobile Device Manager Plus allows you to control only the > >> apps on BYO-devices by containerizing them, leaving personal data > >> untouched! > >> https://ad.doubleclick.net/ddm/clk/304595813;131938128;j > >> _______________________________________________ > >> hol-info mailing list > >> hol-info@lists.sourceforge.net > >> https://lists.sourceforge.net/lists/listinfo/hol-info > > > > > > ________________________________ > > > > The information in this e-mail may be confidential and subject to legal > > professional privilege and/or copyright. National ICT Australia Limited > > accepts no liability for any damage caused by this email or its attachments. > > > > ------------------------------------------------------------------------------ > Mobile security can be enabling, not merely restricting. Employees who > bring their own devices (BYOD) to work are irked by the imposition of MDM > restrictions. Mobile Device Manager Plus allows you to control only the > apps on BYO-devices by containerizing them, leaving personal data untouched! > https://ad.doubleclick.net/ddm/clk/304595813;131938128;j > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > > -- > Chun Tian (binghe) > > ------------------------------------------------------------------------------ > Mobile security can be enabling, not merely restricting. Employees who > bring their own devices (BYOD) to work are irked by the imposition of MDM > restrictions. Mobile Device Manager Plus allows you to control only the > apps on BYO-devices by containerizing them, leaving personal data untouched! > https://ad.doubleclick.net/ddm/clk/304595813;131938128;j > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > > > ------------------------------------------------------------------------------ > Mobile security can be enabling, not merely restricting. Employees who > bring their own devices (BYOD) to work are irked by the imposition of MDM > restrictions. Mobile Device Manager Plus allows you to control only the > apps on BYO-devices by containerizing them, leaving personal data untouched! > https://ad.doubleclick.net/ddm/clk/304595813;131938128;j_______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ Mobile security can be enabling, not merely restricting. Employees who bring their own devices (BYOD) to work are irked by the imposition of MDM restrictions. Mobile Device Manager Plus allows you to control only the apps on BYO-devices by containerizing them, leaving personal data untouched! https://ad.doubleclick.net/ddm/clk/304595813;131938128;j _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
