Hi Chris, If you want an easily distributable standalone PolyML, you can build it in MinGW (msys2) instead of Cygwin with following steps (from Isabelle): (I tested and succeeded in Windows 10)
MinGW for native Windows support ================================ - always "Run as administrator ..." - http://sourceforge.net/projects/msys2 target c:\msys64 - http://sourceforge.net/projects/mingw-w64 mingw-w64-install.exe i686-4.9.3-win32-dwarf-rt_v4-rev0 x86_64-4.9.3-win32-seh-rt_v4-rev0 target c:\msys64 - within msys shell: pacman --needed -Sy bash pacman pacman-mirrors msys2-runtime after restart of msys shell: pacman -Su pacman -S make diffutils texinfo gmp-devel mingw-w64-i686-gmp mingw-w64-x86_64-gmp I think the key is to use GCC 4.9.x instead of any higher versions (5.x, 6.x). Once above steps are done, you can easily build 32-bit or 64-bit PolyML in MinGW command line using normal steps (configure, make, make install). However, the PolyML built in this way, cannot be used to build HOL4, but I think this is an issue of HOL4, which always depends on PolyML's Posix module which is not available in Windows with building steps described above. P. S. Using "Bash on Ubuntu on Windows 10" subsystem is definitely a short path, but I found some big theories can't be built in HOL4 running in this mode. For instance, CakeML. But I'm not sure if my once observation is really an issue of the Linux subsystem. Hope this helps, Chun Tian On 1 May 2017 at 20:32, Chris Cannam <[email protected]> wrote: > That's good to know, thanks. I'm guessing this has a runtime dependency > on other Cygwin or WSL libraries and can't easily be distributed > standalone? > > I'm primarily wondering what is the most minimal possible installation > that I can ask a Windows user (who probably starts without either Cygwin > or WSL installed) to make, in order to make use of a script that happens > to involve running an SML program. For this purpose it doesn't actually > have to be a REPL, though that would be nice to have generally. Just > running a program and presenting the output would be enough. > > > Chris > > On Mon, 1 May 2017, at 19:12, [email protected] wrote: > > Building under Cygwin or with the official Linux subsystem gives you > > this. > > > > Michael > > > > On 1/5/17, 19:49, "[email protected] on behalf of Chris > Cannam" > > <[email protected] on behalf of [email protected]> > > wrote: > > > > Hello -- I'm wondering whether there is a Windows build of Poly/ML > > available that can be used from a within command prompt or executed > > from > > a Powershell script, in the same sort of way as SML/NJ can be on > > Windows, or as Poly/ML can on other platforms. > > > > As far as I can see the Windows distribution contains an executable > > that > > always opens its own window and provides its own interactive prompt, > > which (although nice enough) is not quite what I want at the moment. > > > > Is there such a thing out there? > > > > Thanks, > > > > > > Chris > > _______________________________________________ > > polyml mailing list > > [email protected] > > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > > > > > _______________________________________________ > polyml mailing list > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml > -- Chun Tian (binghe) University of Bologna (Italy)
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
