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