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/INST...
The main build process is described in Scala here: http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/src/Pure/Admin/bu...
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_sy...
Here is a portable way to invoke Cygwin GNU bash from ML: http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/src/Pure/System/b...
For $ISABELLE_BASH_PROCESS use this little C program: http://isabelle.in.tum.de/repos/isabelle/file/9c634887be9e/Admin/bash_proces...
So while Poly/ML is running as native Windows application, the surrounding system environment is that of Cygwin (shell etc.).
Makarius