search

informalsystems / modelator-py

Utilities for the TLA+ ecoystem and model-based testing using TLA+.
Apache License 2.0
28 stars 2 forks source link

Apalache path has issues on mac cause of the space in path #71

Open udit-gulati opened 1 year ago

udit-gulati commented 1 year ago

Ref:

(env) uditgulati@Udits-MacBook-Air transfer % modelator apalache info
Default location for JAR file: /Users/uditgulati/Library/Application Support/modelator/checkers
Looking for version: 0.30.1
Looking for file: /Users/uditgulati/Library/Application Support/modelator/checkers/apalache/lib/apalache-0.30.1.jar
WARNING:root:Error while checking the existence of the jar file
Apalache JAR file not found
(env) uditgulati@Udits-MacBook-Air transfer % ls /Users/uditgulati/Library/Application Support/modelator/checkers/apalache/lib/
ls: /Users/uditgulati/Library/Application: No such file or directory
ls: Support/modelator/checkers/apalache/lib/: No such file or directory
(env) uditgulati@Udits-MacBook-Air transfer % ls /Users/uditgulati/Library/Application\ Support/modelator/checkers/apalache/lib/apalache-0.30.1.jar
/Users/uditgulati/Library/Application Support/modelator/checkers/apalache/lib/apalache-0.30.1.jar
rnbguy commented 1 year ago

Hmm. This is strange. Can you please tell me the output of atomkraft model apalache get with the jar file present?

Also, does this persist if you delete the jar and do a fresh atomkraft model apalache get ?