Dear developers --
PolyML had been working great for me, but I wanted to move to a more recent version of HOL4, which demands a newer version of PolyML. I run on cygwin and find two issues:
1) Out of the box, 5.7.1 and 5.8 (which, by the way is not advertised as the latest release on polyml.org) do not build. This is because statistics.cpp and statistics.h in libpolyml seem to assume that HAVE_WINDOWS_H means you are building for Windows and does not take Cygwin into account. Cygwin has gettimeofday, etc. I found that the system builds if every
#ifdef HAVE_WINDOWS_H
is replaced by
#if defined(HAVE_WINDOWS_H) && ! defined(__CYGWIN__)
It may be easier just to suppress HAVE_WINDOWS_H in the presence of __CYGWIN__, though I have not confirmed that as a proper solution.
2) The system thus built fails to run Holmake properly, crashing with signal B (11) (SEGV, I believe). It works if I run Holmake with -j1 (default is something like -j4), which means that multiple concurrent instances of poly interfere with each other in some way, near as I can tell.
Regards - Eliot Moss