informalsystems/modelator

Model.parse_file fails after fresh installation

rnbguy opened this issue · 4 comments

This error persists regardless of how modelator is installed - via poetry add or pip install (confirmed on fresh docker instances).

>>> tlapath = "/path/to/tla/file"
>>> from modelator.Model import Model
>>> m = Model.parse_file(file_name=tlapath)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/user/.cache/pypoetry/virtualenvs/mbt-demo-XXX-py3.10/lib/python3.10/site-packages/modelator/Model.py", line 44, in parse_file
    m._parse()
  File "/home/user/.cache/pypoetry/virtualenvs/mbt-demo-XXX-py3.10/lib/python3.10/site-packages/modelator/Model.py", line 53, in _parse
    parse(tla_file_name=self.tla_file_path, files=self.files_contents)
  File "/home/user/.cache/pypoetry/virtualenvs/mbt-demo-XXX-py3.10/lib/python3.10/site-packages/modelator/parse.py", line 28, in parse
    result = apalache_pure(json=json_command)
  File "/home/user/.cache/pypoetry/virtualenvs/mbt-demo-XXX-py3.10/lib/python3.10/site-packages/modelator_py/apalache/pure.py", line 137, in apalache_pure
    ret["files"] = read_apalache_output_into_memory(dirname)
  File "/home/user/.cache/pypoetry/virtualenvs/mbt-demo-XXX-py3.10/lib/python3.10/site-packages/modelator_py/apalache/pure.py", line 60, in read_apalache_output_into_memory
    subdirs = get_dirnames_in_dir(full_dirname)
  File "/home/user/.cache/pypoetry/virtualenvs/mbt-demo-XXX-py3.10/lib/python3.10/site-packages/modelator_py/helper.py", line 18, in get_dirnames_in_dir
    bases = os.listdir(path)
FileNotFoundError: [Errno 2] No such file or directory: '/tmp/modelator-py-apalache-temp-dir-zrdj3ox3/out'

@hvanz do you have any idea about this?

It's because the JAR files are not getting downloaded and set up correctly.

Right now modelator looks for jar files at $(pwd)/jars/{apalache,tla2tools}*.jar.

I would suggest,

  1. Auto-fetch the jar files from Github releases.
  2. Store them at user-specific data dirs.

Use something like appdirs to manage these data dirs.

Duplicate of #212