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
HI Eliot, Thanks for that report. I've updated the website and changed statistics.cpp in git master so that it now compiles on Cygwin. I'll backport that to fixes-5.8 once it's had a bit of testing.
Trying to support Poly/ML on Cygwin has always been a bit of a problem. If possible it's better to use the native Windows versions. There are ways to build it yourself from source using Visual Studio or Msys or there is an installer available on GitHub. Another alternative is to use Linux Subsystem for Windows.
Regards, David
On 27/03/2019 02:03, Eliot Moss wrote:
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:
- 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.
- 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 _______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On 3/28/2019 4:24 AM, David Matthews wrote:
HI Eliot, Thanks for that report.? I've updated the website and changed statistics.cpp in git master so that it now compiles on Cygwin.? I'll backport that to fixes-5.8 once it's had a bit of testing.
Trying to support Poly/ML on Cygwin has always been a bit of a problem. If possible it's better to use the native Windows versions.? There are ways to build it yourself from source using Visual Studio or Msys or there is an installer available on GitHub.? Another alternative is to use Linux Subsystem for Windows.
Thank you, David.
My whole setup on my laptop is Cygwin based. If I can use Cygwin HOL4 and Windows polyml, that would be ok, but I can also imagine a number of ways that would break, particularly around handling filenames ... What do you think?
I'm happy to help with testing if that would be useful. The failures with parallel makes (-j4) are manageable but troubling. Something has changed in the interim to break that. I can't say with certainty what I was running before ... but pre 5.7 anyway. From (say) a year or so ago.
Regards - Eliot
On 28/03/2019 11:37, Eliot Moss wrote:
My whole setup on my laptop is Cygwin based.? If I can use Cygwin HOL4 and Windows polyml, that would be ok, but I can also imagine a number of ways that would break, particularly around handling filenames ...? What do you think?
We used to have Cygwin for Isabelle over many years, but more recently the underlying Poly/ML has become native Windows: it is more stable and more scalable.
Here are some notes on how to build Poly/ML with MinGW (using a rather old version of gcc/g++):
http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/Admin/polyml/INST...
The main build process is described in Scala here: http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/src/Pure/Admin/bu...
Here are some ML operations to standardize file names (wrt. Cygwin notation for drive letters, not MinGW):
http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/src/Pure/ML/ml_sy...
Here is a portable way to invoke Cygwin GNU bash from ML: http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/src/Pure/System/b...
For $ISABELLE_BASH_PROCESS use this little C program: http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/Admin/bash_proces...
So while Poly/ML is running as native Windows application, the surrounding system environment is that of Cygwin (shell etc.).
Makarius
On 3/28/2019 6:50 AM, Makarius wrote:
On 28/03/2019 11:37, Eliot Moss wrote:
My whole setup on my laptop is Cygwin based.? If I can use Cygwin HOL4 and Windows polyml, that would be ok, but I can also imagine a number of ways that would break, particularly around handling filenames ...? What do you think?
We used to have Cygwin for Isabelle over many years, but more recently the underlying Poly/ML has become native Windows: it is more stable and more scalable.
Dear Makarius --
I'll run this by Michael Norrish (HOL4 maintainer) as to what would make things work with HOL4, but I am concerned that this is growing into something more complex, where I (or he) will be taking on more maintenance responsibility. In the past HOL4 did not need to know about Cygwin. I only glanced at what you sent, but it seems that HOL4 will need to be adjusted to convert filenames, etc.
At least polyml works with Holmake -j1 for now ...
Regards - Eliot
Eliot Moss wrote:
My whole setup on my laptop is Cygwin based. If I can use Cygwin HOL4 and Windows polyml, that would be ok, but I can also imagine a number of ways that would break, particularly around handling filenames ... What do you think?
I used MobaXterm to run HOL4. HOL4 runs fine on it, unfortunately the hol-vim plugin does not work there.
MobaXterm is a cygwin-based distribution for Windows:
https://mobaxterm.mobatek.net/download-home-edition.html
For compiling polyml on MobaXterm you need a minor tweak in configure:
https://stackoverflow.com/questions/55097775/compiling-poly-ml-on-mobaxterm-...
And you need to install make and g++ via mobapt or apt-get.
- Gergely
On 3/28/2019 11:24 AM, Gergely Buday wrote:
Eliot Moss wrote:
My whole setup on my laptop is Cygwin based. If I can use Cygwin HOL4 and Windows polyml, that would be ok, but I can also imagine a number of ways that would break, particularly around handling filenames ... What do you think?
I used MobaXterm to run HOL4. HOL4 runs fine on it, unfortunately the hol-vim plugin does not work there.
MobaXterm is a cygwin-based distribution for Windows:
https://mobaxterm.mobatek.net/download-home-edition.html
For compiling polyml on MobaXterm you need a minor tweak in configure:
https://stackoverflow.com/questions/55097775/compiling-poly-ml-on-mobaxterm-...
And you need to install make and g++ via mobapt or apt-get.
Thank you, Gergely for the suggestions.
... but I already have a significant Cygwin installation. This would seem to duplicate that. (And it's known that having more than one Cygwin installation can lead to interferences if one does not take particular care.) I'm not quite seeing the advantages here ...
I run HOL4 under emacs and use unicode capabilities and the HOL4 emacs setup. (So lacking vim won't bother me, but not operating with emacs would.) I run this all under Cygwin's X windows support.
Here's a further wondering. It sounds as if your setup is using a (possibly stripped down) Cygwin to build polyml. Are you running polyml 5.7, 5.7.1, or 5.8? An earlier version worked well for me, but these later ones fail with HOL4 unless I use -j1 (the default is -j4) for Hol's build, Holmake, etc. David has fixed the failure-to-compile problem that I reported, so 5.8 should compile going forward. So, does your setup actually work properly with polyml 5.8? I would be a bit surprised unless you're actually doing a Windows native build instead of a Cygwin/MobaXterm build.
Regards - Eliot
Eliot Moss wrote:
Thank you, Gergely for the suggestions.
... but I already have a significant Cygwin installation. This would seem
to
duplicate that. (And it's known that having more than one Cygwin
installation
can lead to interferences if one does not take particular care.) I'm not
quite
seeing the advantages here ...
I just described what I did and that it works.
I think the real problem here is that there's no standard framework under Windows that supports open source software.
Cygwin's user interface is dated and package management is cumbersome.
The Windows Subsystem for Linux is not really open, one cannot install her favourite distribution easily.
MobaXterm's ease of installation -- one file -- lets my students to start with POSIX shell and basic open source software (with an X server) but their choice of busybox has its drawbacks and it is again not open source.
I run HOL4 under emacs and use unicode capabilities and the HOL4 emacs setup. (So lacking vim won't bother me, but not operating with emacs would.) I run this all under Cygwin's X windows support.
Here's a further wondering. It sounds as if your setup is using a
(possibly
stripped down) Cygwin to build polyml. Are you running polyml 5.7, 5.7.1,
or
5.8? An earlier version worked well for me, but these later ones fail
with
HOL4 unless I use -j1 (the default is -j4) for Hol's build, Holmake, etc.
David
has fixed the failure-to-compile problem that I reported, so 5.8 should compile going forward. So, does your setup actually work properly with polyml 5.8? I would be a bit surprised unless you're actually doing a
Windows
native build instead of a Cygwin/MobaXterm build.
I ran polyml 5.7.1 . With polyml 5.8 I get the following:
make[3]: Entering directory '/home/mobaxterm/5.8/polyml-5.8/libpolyml' /bin/sh ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Ilibffi/include -Wall -DMODULEDIR="/home/mobaxterm/5.8/polyml-5.8/lib/polyml/modules" -O3 -Ilibffi/include -MT statistics.lo -MD -MP -MF .deps/statistics.Tpo -c -o statistics.lo statistics.cpp libtool: compile: g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Ilibffi/include -Wall -DMODULEDIR="/home/mobaxterm/5.8/polyml-5.8/lib/polyml/modules" -O3 -Ilibffi/include -MT statistics.lo -MD -MP -MF .deps/statistics.Tpo -c statistics.cpp -DDLL_EXPORT -DPIC -o .libs/statistics.o statistics.cpp: In member function 'virtual void Statistics::Init()': statistics.cpp:209:39: error: cannot convert 'timeval*' to 'LPFILETIME {aka _FILETIME*}' for argument '1' to 'void GetSystemTimeAsFileTime(LPFILETIME)' GetSystemTimeAsFileTime(&startTime);
David, do you have an idea what's this and how could I fix it? I have g++ 7.3.0.
- Gergely
On 3/29/2019 7:55 AM, Gergely Buday wrote:
I ran polyml 5.7.1 . With polyml 5.8 I get the following:
make[3]: Entering directory '/home/mobaxterm/5.8/polyml-5.8/libpolyml' /bin/sh ../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Ilibffi/include -Wall -DMODULEDIR="/home/mobaxterm/5.8/polyml-5.8/lib/polyml/modules" -O3 -Ilibffi/include -MT statistics.lo -MD -MP -MF .deps/statistics.Tpo -c -o statistics.lo statistics.cpp libtool: compile: g++ -DHAVE_CONFIG_H -I. -I.. -O3 -Ilibffi/include -Wall -DMODULEDIR="/home/mobaxterm/5.8/polyml-5.8/lib/polyml/modules" -O3 -Ilibffi/include -MT statistics.lo -MD -MP -MF .deps/statistics.Tpo -c statistics.cpp -DDLL_EXPORT -DPIC -o .libs/statistics.o statistics.cpp: In member function 'virtual void Statistics::Init()': statistics.cpp:209:39: error: cannot convert 'timeval*' to 'LPFILETIME {aka _FILETIME*}' for argument '1' to 'void GetSystemTimeAsFileTime(LPFILETIME)' GetSystemTimeAsFileTime(&startTime);
David, do you have an idea what's this and how could I fix it? I have g++ 7.3.0.
That's the problem I reported; David has a fix for that he is testing.
I worked around it (not sure it's the "right" fix) by changing every
#ifdef HAVE_WINDOWS_H
in statistics.cpp and statistics.h to read
#if defined(HAVE_WINDOWS_H) && !defined(__CYGWIN__)
Regards - EM
On 29/03/2019 12:34, Eliot Moss wrote:
That's the problem I reported; David has a fix for that he is testing.
I worked around it (not sure it's the "right" fix) by changing every
? #ifdef HAVE_WINDOWS_H
in statistics.cpp and statistics.h to read
? #if defined(HAVE_WINDOWS_H) && !defined(__CYGWIN__)
The reaon I didn't do that everywhere was that by using the Windows shared memory mechanism the statistics can be read using the performance monitor plug-in that is installed by the Poly/ML Windows installer.
To be honest I'm not sure it's worth it and it may be time to try to simplify the selection of native Windows code. It should probably use "#ifdef _WIN32" rather than "defined(HAVE_WINDOWS_H) && !defined(__CYGWIN__)". A few things may not work, though if Windows-code is completely excluded from Cygwin. I don't know any way to get the number of physical processors except through Windows calls. There is also some Cygwin-specific code to implement OS.Process.system.
David
On 29/03/2019 12:55, Gergely Buday wrote:
I think the real problem here is that there's no standard framework under Windows that supports open source software.
Cygwin's user interface is dated and package management is cumbersome.
The Windows Subsystem for Linux is not really open, one cannot install her favourite distribution easily.
MobaXterm's ease of installation -- one file -- lets my students to start with POSIX shell and basic open source software (with an X server) but their choice of busybox has its drawbacks and it is again not open source.
Have you tried this (relatively recent) project?
The package manager for Windows Chocolatey - Software Management Automation
Makarius
-
buday.gergely＠uni-eszterhazy.hu -
David.Matthews＠prolingua.co.uk -
gbuday＠gmail.com -
makarius＠sketis.net -
moss＠cs.umass.edu