informalsystems/modelator

[Suggestion] Checking for Apalache jar whenever a modelator is imported

ivan-gavran opened this issue · 3 comments

ivan-gavran commented

At the moment, there is a CLI command check-apalache-jar which checks if a desired version of Apalache exists, and downloads it if necessary.
This still leaves the users of Modelator (and Atomkraft, by extension) with one extra command to run in order to obtain what should be considered as an integral part of the software.

Thus, I suggest a following change:

  • we check for a default apalache jar whenever Modelator is imported (we place that check inside __init__.py file)
  • we allow users to use whatever other version of Apalache they want by calling the existing check-apalache-jar. I would suggest, though, to rename it to set-apalache-jar, but keep the functionality the same (if the jar does not exist and is supported, it should be downloaded).
  • furthermore, in order to avoid the risk of users failing to use Modelator because they do not have an active internet connection, I would allow them to provide a path to whatever version of Apalache they have on their system from before (inside the set-apalache-jar command).

@hvanz , @andrey-kuprianov : I would like to hear your thoughts on this suggestion. (The broader context is the work simplifying the atomkraft tutorial.)

andrey-kuprianov commented

There is already work in that direction: #242.

I am not sure at the moment what's the best course of action. I am in the process of evaluating the combined CLI of Modelator & Atomkraft; I will come with concrete suggestions on Monday.

  • 👍1
ivan-gavran commented

An alternative approach would be to ship one (and always only one!) jar of Apalache together with Modelator.
This avoids the problem of forcing unexpected network requirements/waiting onto users when they don't expect it: installation process really is the moment when users are expecting a bit longer waits and definitely are having an active connection to the internet.

ivan-gavran commented

As we discussed synchronously, a good place for doing so would be when initializing a project (atomkraft init...).
Thus, a model checker would be downloaded only when the first project is initialized.