I am trying to understand my options for using Poly/ML on MinGW for building windows applications coded in Standard ML.
There is a bug reported in http://sourceforge.net/p/mingw/bugs/2043/ that you have to work around to build Poly/ML with the current MinGW. The work-around is to run configure with CXXFLAGS="-D_GLIBCXX_HAVE_FENV_H=1? in the environment. (I suspect I should also throw -O3 in there too, as I think that setting CXXFLAGS replaces its initial setting of -O3 inside the makefiles. Is that right?)
Having got Poly/ML to compile, I found that polyc gives errors like the following when asked to compile a source file:
gcc.exe: error: C:/DOCUME~1/rda/LOCALS~1/Temp/polyobj.2724.obj: No such file or directory
If I create an object file from the Poly/ML GUI using PolyML.export, polyc will link it. If I understand what is going on correctly, the resulting program is a Windows application that brings up the Poly/ML GUI to provide the standard input, output and error channels, unless it is run with standard input and output connected to pipes, in which case it works like a pipe. I think I may end up having to package the Standard ML parts of my application as a server, with the GUI provided by clients implemented in some other language. Are there any other options?
Regards,
Rob.
Rob,
On 18/05/2014 17:36, Rob Arthan wrote:
I am trying to understand my options for using Poly/ML on MinGW for building windows applications coded in Standard ML.
There is a bug reported in http://sourceforge.net/p/mingw/bugs/2043/ that you have to work around to build Poly/ML with the current MinGW. The work-around is to run configure with CXXFLAGS="-D_GLIBCXX_HAVE_FENV_H=1? in the environment. (I suspect I should also throw -O3 in there too, as I think that setting CXXFLAGS replaces its initial setting of -O3 inside the makefiles. Is that right?)
I suspect it is. I wasn't aware of the need for _GLIBCXX_HAVE_FENV_H=1 but it's quite a while since I last used Mingw. It isn't clear from the link whether this is something the Poly/ML configure should do or not.
Having got Poly/ML to compile, I found that polyc gives errors like the following when asked to compile a source file:
gcc.exe: error: C:/DOCUME~1/rda/LOCALS~1/Temp/polyobj.2724.obj: No such file or directory
Again, I haven't tried this with Mingw. I'll take a look.
If I create an object file from the Poly/ML GUI using PolyML.export, polyc will link it. If I understand what is going on correctly, the resulting program is a Windows application that brings up the Poly/ML GUI to provide the standard input, output and error channels, unless it is run with standard input and output connected to pipes, in which case it works like a pipe. I think I may end up having to package the Standard ML parts of my application as a server, with the GUI provided by clients implemented in some other language. Are there any other options?
I think there are three possible options for building Poly/ML on Windows: Mingw, Visual C or Cygwin. If you use Mingw or Visual C you are building the native Windows version. This version does put up the GUI, as you say, if the standard input and output are missing. This is actually done by the RTS before the ML code is entered so applies equally to functions exported with PolyML.export as to the usual Poly/ML read-eval-print loop. Actually, it occurs to me that it is now possible to write the GUI in ML and include it as part of the top-level root function in Windows. This would allow a user-exported function to completely by-pass it. I think a GUI is necessary for Windows applications since that is what Windows users would expect.
Using Cygwin might be a possibility if you are thinking of providing a separate GUI. The package that Makarius has provided for running Isabelle on Windows uses Poly/ML under Cygwin but all the user interaction is through jEdit. There might be issues, though, if you wanted the ML code to access the Windows filing system because Cygwin imposes its own view of the filing system.
Regards, David
David,
On 19 May 2014, at 15:42, David Matthews <David.Matthews at prolingua.co.uk> wrote:
Rob,
On 18/05/2014 17:36, Rob Arthan wrote:
I am trying to understand my options for using Poly/ML on MinGW for building windows applications coded in Standard ML.
There is a bug reported in http://sourceforge.net/p/mingw/bugs/2043/ that you have to work around to build Poly/ML with the current MinGW. The work-around is to run configure with CXXFLAGS="-D_GLIBCXX_HAVE_FENV_H=1? in the environment. (I suspect I should also throw -O3 in there too, as I think that setting CXXFLAGS replaces its initial setting of -O3 inside the makefiles. Is that right?)
I suspect it is. I wasn't aware of the need for _GLIBCXX_HAVE_FENV_H=1 but it's quite a while since I last used Mingw. It isn't clear from the link whether this is something the Poly/ML configure should do or not.
I agree that it wasn?t very clear whether this was thought to be a bug in the MinGW header files or not.
Having got Poly/ML to compile, I found that polyc gives errors like the following when asked to compile a source file:
gcc.exe: error: C:/DOCUME~1/rda/LOCALS~1/Temp/polyobj.2724.obj: No such file or directory
Again, I haven't tried this with Mingw. I'll take a look.
Thanks.
If I create an object file from the Poly/ML GUI using PolyML.export, polyc will link it. If I understand what is going on correctly, the resulting program is a Windows application that brings up the Poly/ML GUI to provide the standard input, output and error channels, unless it is run with standard input and output connected to pipes, in which case it works like a pipe. I think I may end up having to package the Standard ML parts of my application as a server, with the GUI provided by clients implemented in some other language. Are there any other options?
I think there are three possible options for building Poly/ML on Windows: Mingw, Visual C or Cygwin. If you use Mingw or Visual C you are building the native Windows version. This version does put up the GUI, as you say, if the standard input and output are missing. This is actually done by the RTS before the ML code is entered so applies equally to functions exported with PolyML.export as to the usual Poly/ML read-eval-print loop. Actually, it occurs to me that it is now possible to write the GUI in ML and include it as part of the top-level root function in Windows. This would allow a user-exported function to completely by-pass it. I think a GUI is necessary for Windows applications since that is what Windows users would expect.
I would actually have expected the ?GUI? to be a command prompt window. I.e., I would have expected poly to be a console application. This is how python comes, for example. Something that behaves like a console application is what cc on MinGW seems to give you if you don?t give it any of the Windows-specific command line options when you compile a standard C program.
Using Cygwin might be a possibility if you are thinking of providing a separate GUI. The package that Makarius has provided for running Isabelle on Windows uses Poly/ML under Cygwin but all the user interaction is through jEdit. There might be issues, though, if you wanted the ML code to access the Windows filing system because Cygwin imposes its own view of the filing system.
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?
Regards,
Rob.
Rob,
On 20/05/2014 06:57, Rob Arthan wrote:
I agree that it wasn?t very clear whether this was thought to be a bug in the MinGW header files or not.
I may have a look and see if this is something I can fix easily but there's no point if they are going to fix in Mingw anyway. Last time I used Mingw I didn't have this problem.
I would actually have expected the ?GUI? to be a command prompt window. I.e., I would have expected poly to be a console application. This is how python comes, for example. Something that behaves like a console application is what cc on MinGW seems to give you if you don?t give it any of the Windows-specific command line options when you compile a standard C program.
What exactly do you mean by a console application? There is a legacy console mode but it is very inconvenient to use. Cutting and pasting in particular are not at all intuitive. Why exactly do you want to use console mode? More generally, what exactly is it that you want to do that the present version of Poly/ML will not let you do? If you have an ML program that you want to run as a process with a separate GUI application that is easy. Just create the input and output pipes and pass them as arguments in the CreateProcess call. The ML process will be completely invisible and all the user will see is your GUI. That's how I normally run Poly/ML.
The only circumstance where the present system may not work satisfactorily is if you have written a GUI application in ML itself, for instance the mlEdit example in mlsource/extra/Win/Examples. When the user double-clicks on the application to run it there would be an extra window because the RTS creates its own GUI.
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.
David
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
David,
On 20 May 2014, at 13:07, David Matthews <David.Matthews at prolingua.co.uk> wrote:
Rob,
On 20/05/2014 06:57, Rob Arthan wrote:
I agree that it wasn?t very clear whether this was thought to be a bug in the MinGW header files or not.
I may have a look and see if this is something I can fix easily but there's no point if they are going to fix in Mingw anyway. Last time I used Mingw I didn't have this problem.
As the work-around just involves setting an environment variable when you run configure, I don?t think it is worth spending much time on.
I would actually have expected the ?GUI? to be a command prompt window. I.e., I would have expected poly to be a console application. This is how python comes, for example. Something that behaves like a console application is what cc on MinGW seems to give you if you don?t give it any of the Windows-specific command line options when you compile a standard C program.
What exactly do you mean by a console application?
I mean the kind of thing that Visual Studio creates if you select ?Win32 Console Application? when you create a new C++ project. I.e., a program with the standard C interface to the operating system, i.e., an entry point called main.
There is a legacy console mode but it is very inconvenient to use. Cutting and pasting in particular are not at all intuitive. Why exactly do you want to use console mode?
I didn?t say that it was what I wanted: it is all I would have expected (as in ?I always expect pain when I upgrade my operating system?). I agree that cut and paste are clunky in command prompt windows, so it is great to have something nicer.
More generally, what exactly is it that you want to do that the present version of Poly/ML will not let you do?
This isn?t much of a problem for me, but what you are offering is rather inconvenient for anyone who wants to write ML programs that present the kind of interface that Windows command line programs like ?sort" offer (with cmd.exe and the C runtime providing interactive input and output from a console window and redirection of standard input and output to files). Such things can be written portably using standard C or standard C++ and, it would be nice to be able to code similar things in ML without needing a wrapper to call them on Windows.
If you have an ML program that you want to run as a process with a separate GUI application that is easy. Just create the input and output pipes and pass them as arguments in the CreateProcess call. The ML process will be completely invisible and all the user will see is your GUI. That's how I normally run Poly/ML.
This is for the scenario where I write (in some other language) a GUI that is going to start my ML program and interact with it via files or pipes or suchlike. Is that right?
The only circumstance where the present system may not work satisfactorily is if you have written a GUI application in ML itself, for instance the mlEdit example in mlsource/extra/Win/Examples.
How do you compile the code in that directory? It doesn?t seem to contain the source file for mlEdit that the documentation for the Windows interface refers to.
When the user double-clicks on the application to run it there would be an extra window because the RTS creates its own GUI.
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 might be an option, but it seems like quite an overhead to have to include something that provides vast amounts of functionality to emulate UNIX that I just don?t need and is a potential source of problems. So I was trying to explore the options for having libpolyml use standard C++ libraries (and not the Windows GUI libraries) without emulating UNIX.
I am also thinking about the possibility of packaging an ML program as a Windows service (by providing my own libpolymain with entry points ServiceMain etc.) and thought that would be incompatible with the Windows GUI stuff, but maybe it will work with libpolyml compiled as it is presently or maybe it just doesn?t make sense. I will have to do some experiments.
Regards,
Rob.
Rob,
On 24/05/2014 14:29, Rob Arthan wrote:
What exactly do you mean by a console application?
I mean the kind of thing that Visual Studio creates if you select ?Win32 Console Application? when you create a new C++ project. I.e., a program with the standard C interface to the operating system, i.e., an entry point called main.
This isn?t much of a problem for me, but what you are offering is rather inconvenient for anyone who wants to write ML programs that present the kind of interface that Windows command line programs like ?sort" offer (with cmd.exe and the C runtime providing interactive input and output from a console window and redirection of standard input and output to files). Such things can be written portably using standard C or standard C++ and, it would be nice to be able to code similar things in ML without needing a wrapper to call them on Windows.
I see. I have to say that I'm really surprised that anyone would actually want to build a console application; I'd always regarded it as a legacy from DOS. It's quite easy, though, to do it if you want to. Console applications just have the "console" subsystem set in the EXE header rather than "windows" so to build a console application you just need the /SUBSYSTEM:CONSOLE option to the linker (-mconsole with GCC). By default, setting /SUBSYSTEM:CONSOLE also changes the entry point but since poly uses the WinMain entry point you have to change it back again with a /ENTRY:WinMainCRTStartup option. To build a console application under Mingw/Msys just change -mwindows to -mconsole.
There were a couple of issues when I tried this to build poly: control-C was not handled properly and the console stream wasn't recognised as interactive. I've fixed these in SVN trunk.
This is for the scenario where I write (in some other language) a GUI that is going to start my ML program and interact with it via files or pipes or suchlike. Is that right?
Correct.
The only circumstance where the present system may not work satisfactorily is if you have written a GUI application in ML itself, for instance the mlEdit example in mlsource/extra/Win/Examples.
How do you compile the code in that directory? It doesn?t seem to contain the source file for mlEdit that the documentation for the Windows interface refers to.
The code for mlEdit is in mlEdit.sml. It's definitely there in every polyml directory I've looked at. You need to build the Windows GUI code first: PolyML.make "mlsource/extra/Win"; and then use "mlsource/extra/Win/Examples/mlEdit";
That might be an option, but it seems like quite an overhead to have to include something that provides vast amounts of functionality to emulate UNIX that I just don?t need and is a potential source of problems. So I was trying to explore the options for having libpolyml use standard C++ libraries (and not the Windows GUI libraries) without emulating UNIX.
Agreed. I was just trying to suggest an easy way to get a console-like window.
I am also thinking about the possibility of packaging an ML program as a Windows service (by providing my own libpolymain with entry points ServiceMain etc.) and thought that would be incompatible with the Windows GUI stuff, but maybe it will work with libpolyml compiled as it is presently or maybe it just doesn?t make sense. I will have to do some experiments.
You could certainly do that if it made sense for your application. Services are essentially the equivalent of Unix daemons.
Regards, David
On Mon, 19 May 2014, David Matthews wrote:
Using Cygwin might be a possibility if you are thinking of providing a separate GUI. The package that Makarius has provided for running Isabelle on Windows uses Poly/ML under Cygwin but all the user interaction is through jEdit.
Isabelle/jEdit is merely the front-end. The actual connectivity happens via Isabelle/Scala, which is just a JVM plus some Scala-implemented jars. All the system plumbing is done via the Java APIs, which might sound odd, since Java traditionally achieves platform-indepence by omitting important platform-specific operations (e.g. POSIX kill), but in Java 7 it has greatly improved.
The JVM process could be replaced by some more native Windows program, but we depend on the JVM anyway, so it is the canonical solution.
There are also some funny add-on scripts, e.g. to make a named pipe on Unix, but on Windows we are using regular TCP sockets to connect the ML process.
There might be issues, though, if you wanted the ML code to access the Windows filing system because Cygwin imposes its own view of the filing system.
Here we merely use POSIX-ish notation, e.g. /cygdrive/c instead of C:\ The Isabelle/Scala library has operations to convert between different formats, and gives the ML process what it expects. This also works for Windows network paths //server/share/foo/bar -- better than TeXlive on that platform.
The jEdit editor has its own traditions to iron out Windows vs. POSIX differences, such that users of Isabelle/jEdit can refer to things like $ISABELLE_HOME/src/HOL/HOL.thy literally in that Isabelle-specific notation, just by coincidence.
Makarius
-
David.Matthews＠prolingua.co.uk -
makarius＠sketis.net -
rda＠lemma-one.com