TLAPS in WSL2 - Prover Launch problem

[hejersbo]

Running tlapm installed in WSL2 from Toolbox in Windows gives the following error when I try to launch a proof from the provided Euclid.tla example:

"Error running tlapm. Error code: 3".
Oops, this seems to be a bug in TLAPM.
Please give feedback to developers.

Invalid_argument("index out of bounds")
Raised by primitive operation at file "params.ml", line 227, characters 7-14
Called from file "arg.ml", line 201, characters 12-17
Called from file "arg.ml", line 260, characters 8-27
Called from file "tlapm_args.ml", line 47, characters 4-155
Called from file "tlapm_args.ml", line 212, characters 2-37
Called from file "tlapm.ml", line 348, characters 13-33

version == "1.4.5 (build 33809)"
built_with == "OCaml 4.05.0"
tlapm_executable == "/usr/local/bin/tlapm"
max_threads == 12
library_path == "/usr/local/lib/tlaps"
search_path == << "/usr/local/lib/tlaps" >>
flatten_obligations == TRUE
normalize == TRUE

Toolbox version:
TLA+ Toolbox provides a user interface for TLA+ Tools.
This is Version 1.7.1 of 31 December 2020 and includes:

• SANY Version 2.2 of 20 April 2020
  OS: Windows 10, v.10.0, x86_64 / win32
  Java version: 14.0.1

Toolbox error log:
!SESSION 2023-04-30 10:43:20.064 -----------------------------------------------
eclipse.buildId=1.7.1
java.version=14.0.1
java.vendor=AdoptOpenJDK
BootLoader constants: OS=win32, ARCH=x86_64, WS=win32, NL=en_US
Command-line arguments: -os win32 -ws win32 -arch x86_64

!ENTRY org.lamport.tla.toolbox.product.standalone 1 -1 2023-04-30 10:43:22.091
!MESSAGE TLA+ Toolbox started without arguments.

!ENTRY org.lamport.tla.toolbox.tool.prover.ui 1 -1 2023-04-30 10:43:53.106
!MESSAGE Run method called 0

!ENTRY org.lamport.tla.toolbox.tool.prover.ui 1 -1 2023-04-30 10:43:53.128
!MESSAGE Prover ARGUMENTS: [C:\Windows\System32\wsl.exe, tlapm, --toolbox, 35, 36, --isaprove, -I, $(wslpath L:\usr\local\lib\tlaps\), $(wslpath C:\Users\au382946\Euclid.tla)]

!ENTRY org.lamport.tla.toolbox.tool.prover.ui 1 -1 2023-04-30 10:43:53.129
!MESSAGE TLAPM launched 24

!ENTRY org.lamport.tla.toolbox.tool.prover.ui 1 -1 2023-04-30 10:43:53.478
!MESSAGE Done with proving 374

!ENTRY org.lamport.tla.toolbox.tool.prover.ui 4 0 2023-04-30 10:43:53.485
!MESSAGE Error running tlapm. Report a bug with the error code to the developers at https://github.com/tlaplus/tlapm/issues.

Error code: 3

Ubuntu version:
Distributor ID: Ubuntu
Description: Ubuntu 22.04.1 LTS
Release: 22.04
Codename: jammy

[hejersbo]

Running tlapm from Powershell provides output below, which appears not to fail with the tlapm error that I get when running via the Toolbox.

PS C:> wsl tlapm --cleanfp /mnt/c/Users/au382946/Euclid.tla
** Unexpanded symbols: GCD

** Unexpanded symbols: GCD

** Unexpanded symbols: Next, InductiveInvariant

** Unexpanded symbols: GCD

** Unexpanded symbols: GCD

** Unexpanded symbols: GCD

** Unexpanded symbols: GCD

** Unexpanded symbols: GCD

** Unexpanded symbols: GCD

** Unexpanded symbols: GCD

** Unexpanded symbols: GCD

(* created new "Euclid.tlaps/Euclid.thy" )
( fingerprints written in "Euclid.tlaps/fingerprints" *)

[hejersbo]

Running the proof from WSL2 cmd line seems to work (same args as invoked by Toolbox)

@!!BEGIN
@!!type:obligation
@!!id:2
@!!loc:36:6:36:22
@!!status:trivial
@!!prover:tlapm
@!!already:false
@!!END

@!!BEGIN
@!!type:obligation
@!!id:1
@!!loc:36:3:36:5
@!!status:proved
@!!prover:smt
@!!meth:time-limit: 5; time-used: 0.0 (1%)
@!!already:false
@!!END

(* created new "Euclid_test.tlaps/Euclid_test.thy" )
( fingerprints written in "Euclid_test.tlaps/fingerprints" *)
hejersbo@D42857:/usr/local/lib/tlaps/examples$ tlapm --cleanfp --toolbox 35 36 --isaprove Euclid_test.tla

[hejersbo]

Works now. It was a user error caused by specifying the TLA+ library path for tlaps in the wrong format. Specifying the path as: \wsl$\Ubuntu-20.04\use\local\lib\tlaps\ works.

I will close this.