modelator-py

modelator-py copied to clipboard

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

1

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...

udit-gulati

Currently `modelator-py` is a dependency on [`modelator`](https://github.com/informalsystems/modelator). But both of them use the same name for the CLI app. https://github.com/informalsystems/modelator-py/blob/801e8b214217ce977edb655ff0bf3d379b0a91fe/pyproject.toml#L29-L30 Since `modelator-py` because a python library for TLA, I suggest...

rnbguy

ImportError: sys.meta_path is None, Python is likely shutting down

1

I am getting the following error on Python 3.10, ``` Exception ignored in: Traceback (most recent call last): File "/home/XXXX/.cache/pypoetry/virtualenvs/modelator-py-5E8ZuFvv-py3.10/lib/python3.10/site-packages/multiprocess/pool.py", line 268, in __del__ File "/home/XXXX/.cache/pypoetry/virtualenvs/modelator-py-5E8ZuFvv-py3.10/lib/python3.10/site-packages/multiprocess/queues.py", line 375, in put...

rnbguy

Feature: tag outputs with version

1

In [abd3912](https://github.com/informalsystems/modelator-py/commit/abd39125aab952f72772874324240b5333407003) the tool runs without tagging outputs with the version. All outputs should be version tagged in order to help create better bug reports.

danwt

In [abd3912](https://github.com/informalsystems/modelator-py/commit/abd39125aab952f72772874324240b5333407003) there is no support for interrupting long running processes (model checking) in a nice way that will return partial results. The problem is that modeling work often involves...

danwt

[2285f5b](https://github.com/informalsystems/modelator-py/commit/2285f5b57427f5b7b4acd7eb81d73a5cb0bc0fcc) only explicitly supports unix like OS's but _perhaps_ some effort should be invested to support windows too. Supporting three OS's is a lot of work though and requires rigorous...

danwt

In [2285f5b](https://github.com/informalsystems/modelator-py/commit/2285f5b57427f5b7b4acd7eb81d73a5cb0bc0fcc) every parameter is left to the user to specify, but it might be a good idea to specify some sensible defaults. For example: number of workers used could...

danwt

Leave until merge into monorepo

danwt

Operations: add git hooks that will delete empty directories when changing branch

1

Tools in the python ecosystem often leave cache directories (`__pycache__`). These occupy otherwise empty directories when changing branches and get in the way of having a clean workspace. It may...

danwt

Feature: ensure correct JDK used when running Apalache

1

Apalache should be run using the right JDK in order to get it to work on `arm64`.

danwt