This is a report on an elusive problem with Poly/ML on Cygwin on Vista that may be of use to others (and perhaps someone else can pin the problem down more closely or suggest a better solution?).

An executable pp-ml.exe written in Poly/ML using PolyML.export and gcc on Cygwin on Vista sometimes fails with a segmentation fault and a stack dump like this:

Exception: STATUS_ACCESS_VIOLATION at eip=610E384A eax=1A75CE64 ebx=01186388 ecx=75F9A620 edx=77715CA4 esi=011863E0 edi=1AD5CE64 ebp=1AD5CD98 esp=1AD5CD60 program=C:\cygwin\home\rda\bld\pp\OpenProofPower-2.9.1w2\src\pp-ml.exe, pid 2968, thread unknown (0x218) cs=001B ds=0023 es=0023 fs=003B gs=0000 ss=0023 Stack trace: Frame Function Args 1AD5CD98 610E384A (01186388, 1AD5CDD4, 610E3810, 01186388) End of stack trace

The failure is probably happening in a call of PolyML.SaveState.saveChild and seems to be highly erratic: pp-ml job is just to load a state, compile a file of ML source and then save the resulting state; it has already been used to do that scores of times before it failed. It has not been known to fail on Windows XP. It appears to be happening because gcc creates binaries that are not flagged as "Terminal Server Aware". The following command fixes the problem:

peflags --tsaware=true pp-ml.exe

There may be gcc options to set the flag, but I couldn't find them.

Regards,

Rob.

David,

Many thanks. It's been a few years since I last used Visual Studio and I never progressed beyond beginner status, so I think MSYS and MinGW will minimise the culture shock for me for the time being!

On 17 Feb 2011, at 09:24, David Matthews wrote:

I think I actually built that using Msys/Mingw. If you install them you can build from source exactly as you would on Unix or cygwin.

Done. But when I do PolyML.export("hw", main) and run the following in an MSYS shell:

gcc -o hw hw.obj -L/usr/lib -lpolymain -lpolyml

then I get a complaint that there is an undefined reference to 'WinMain@16'. I managed to devise a more complicated gcc command line that works by looking at how the Poly/ML installation creates poly.exe, but the result is a Windows application which just flashes up a window and executes immediately. Can I create a console application? I.e., an application with a C/C++ main() and C/C++ console I/O rather than a WinMain() and a GUI?

Aside: for the record, the more complicated command line that worked was:

gcc -o hw -mwindows -Wl,-u -Wl,_WinMain@16 hw.obj -L/usr/lib -lpolymain -lpolyml

There are other possibilities. There are project files for Visual C++ 6 which should work under newer versions of Visual C++. I think it's now possible to download Visual C++ Express free from Microsoft but you'll also need a version of MASM if you want to build Poly/ML from source.

Regards,

Rob.

Regards, David

On 16/02/2011 16:56, Rob Arthan wrote:

...

I have installed Poly/ML on MS Windows using the precompiled binary. Now I want to start building my own applications. What do I need for the equivalent in MS Windows of the following command line that I would use on UNIX?

cc -o hello hello.o -lpolymain -lpolyml

I.e., where do I find the polymain and polyml DLLs and what developer kits can I use? E.g., will MinGW work? And which developer kits are recommended?

Regards,

Rob.

_______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

---

polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml