Add experimental support to invoke a TLAPS installation inside a Windows

subsystem for Linux on Windows 10.

Activate by setting C:\Windows\system32\wsl.exe as the TLAPM executable
in the Toolbox's TLAPS preference page under "Location of tlapm".  It
expects a WSL distro with a standard TLAPS installation (tested with
Ubuntu 18.04 and TLAPS 1.4.5).

[Feature][Toolbox][TLAPS]

org.lamport.tla.toolbox.tool.prover/src/org/lamport/tla/toolbox/tool/prover/job/ProverJob.java

@@ -650,6 +650,19 @@ public class ProverJob extends Job {
 
         command.add(tlapmPath.toOSString());
 
+		// Use Windows Subsystem for Linux instead of Cygwin. This is experimental and
+		// a hack.  A user has to enter wsl.exe or C:\Windows\system32\wsl.exe on the
+        // Toolbox's preference page.  The next if block the appends 'tlapm'. 
+        final boolean useWSL = tlapmPath.toOSString().contains("wsl.exe");
+        if (useWSL) {
+			// Assume tlapm is on PATH in the Linux subsystem. With this, prefixing the
+			// command with 'wsl' tells Windows to invoke the binary (tlapm) via WSL. I
+			// expect this to only work with a single WSL distro installed (otherwise, we
+			// probably have to choose a distro). More information and how to install WSL is
+			// at https://docs.microsoft.com/en-us/windows/wsl/wsl2-install.
+    		command.add("tlapm");
+        }
+
         if (toolboxMode)
         {
             command.add("--toolbox");
@@ -721,12 +734,26 @@ public class ProverJob extends Job {
         if (pathList != null) {
             for (int i=0; i < pathList.length; i++) {
                 command.add("-I") ;
+                if (useWSL) {
+					// 'wslpath' is executed inside the Linux subsystem. It converts an UNC (?) path
+					// such as "C:\\Users\\markus\\Library\\dir\\" to something that can be resolved
+					// in the Linux subsystem. Unfortunately, pathList[n] =
+					// "C:\Users\markus\Library\dir" which is why we replace \\ with \\\\
+					// backslashes.
+    				command.add(String.format("$(wslpath %s)", pathList[pathList.length - i - 1].replace("\\", "\\\\")));
+                } else {
                     command.add(pathList[pathList.length - i - 1]) ;
                 }
             }
+        }
         
+        if (useWSL) {
+        	// See pathList above about wslpath.  This path here is the actual spec to be verified.
+    		command.add(String.format("$(wslpath %s)", module.getLocation().toOSString().replace("\\", "\\\\")));
+        } else {
             // why just the last segment?
             command.add(module.getLocation().toOSString());
+        }
      
         // for debugging
         // for (int i=0; i<command.size(); i++) {