On 28/03/2019 11:37, Eliot Moss wrote: > > My whole setup on my laptop is Cygwin based. If I can use Cygwin > HOL4 and Windows polyml, that would be ok, but I can also imagine > a number of ways that would break, particularly around handling > filenames ... What do you think?
We used to have Cygwin for Isabelle over many years, but more recently the underlying Poly/ML has become native Windows: it is more stable and more scalable. Here are some notes on how to build Poly/ML with MinGW (using a rather old version of gcc/g++): http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/Admin/polyml/INSTALL-MinGW The main build process is described in Scala here: http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/src/Pure/Admin/build_polyml.scala Here are some ML operations to standardize file names (wrt. Cygwin notation for drive letters, not MinGW): http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/src/Pure/ML/ml_system.ML Here is a portable way to invoke Cygwin GNU bash from ML: http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/src/Pure/System/bash.ML For $ISABELLE_BASH_PROCESS use this little C program: http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/Admin/bash_process/bash_process.c So while Poly/ML is running as native Windows application, the surrounding system environment is that of Cygwin (shell etc.). Makarius _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
