On Tue, 20 May 2014, David Matthews wrote:
Cygwin does work for me, but unfortunately, having to install it is a stopper for some of my potential users. I tried compiling under MinGW with __CYGWIN__ set, but it doesn?t work. Would it be difficult to separate the choice between polystub.c being a standard C application and a Windows application from the __CYGWIN__ flag?
Why does the user need to install Cygwin? If you build an application under Cygwin you just need to put the Cygwin DLL and perhaps a few library DLLs in the same folder as your application. Windows always searches for DLLs first in the same folder as the executable.
That default DLL behaviour of Windows is indeed very convenient, although it is unexpected for a Unix person that there is nothing else to do :-) Starting with Cgywin 1.7 from 1-2 years ago that scheme works smoothly, with any number of cygwin.dll versions on the same system. (In the past it was a well-known problem of Cygwin to allow at most one instance.)
Note that for Isabelle we do ship a full Cygwin, since there are additional tools that need a POSIX-ish environment, like E prover, SPASS etc. I have a mostly automated procedure to make a shrinked-wrapped Cygwin distribution, which is then booted up with the help of an external Windows program, which happens to be a JVM application here. (Due to missing POSIX file-system permissions, some black art needs to be applied after unpacking the self-extracting Windows 7zip.)
Just try http://isabelle.in.tum.de/dist/Isabelle2013-2.exe yourself to get an idea how it looks to the end-user. If there is any interest, I can explain further how it is done. I have offered this to various other prover people, but so far they wanted to stay within their small Unix-only world, or imitate Unix-style command-line tinkering directly in the Cygwin shell.
Makarius