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
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
