From c4219f82aa19086e4afe74ed13b2e31a3d8697fc Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Fri, 6 Mar 2020 22:11:21 -0800
Subject: [PATCH] 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]
---
.../toolbox/tool/prover/job/ProverJob.java | 33 +++++++++++++++++--
1 file changed, 30 insertions(+), 3 deletions(-)
diff --git a/org.lamport.tla.toolbox.tool.prover/src/org/lamport/tla/toolbox/tool/prover/job/ProverJob.java b/org.lamport.tla.toolbox.tool.prover/src/org/lamport/tla/toolbox/tool/prover/job/ProverJob.java
index f2623c27c..0b3f159ae 100644
--- a/org.lamport.tla.toolbox.tool.prover/src/org/lamport/tla/toolbox/tool/prover/job/ProverJob.java
+++ b/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") ;
- command.add(pathList[pathList.length - i - 1]) ;
+ 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]) ;
+ }
}
}
- // why just the last segment?
- command.add(module.getLocation().toOSString());
+ 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++) {
--
GitLab