search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
439 stars 40 forks source link

Add Apalache.tla to the pre-built package #1791

Open nano-o opened 2 years ago

nano-o commented 2 years ago

Apalache.tla is needed if one is working with the TLA+ Toolbox, but it's not included in the pre-built package. The installation documentation could also briefly mention how to set it up in the Toolbox.

konnov commented 2 years ago

How are you importing the pre-built package in the Toolbox?

nano-o commented 2 years ago

I meant that I just added a directory containing Apalache.tla to the TLA+ library path in the Toolbox. That's under Files->Preferences->TLA+ Preferences.

shonfeder commented 2 years ago

We do ship Apalache.tla in the uberjar that we distribute. But not sure how that interacts with the tlatoolbox.

konnov commented 2 years ago

I meant that I just added a directory containing Apalache.tla to the TLA+ library path in the Toolbox. That's under Files->Preferences->TLA+ Preferences.

That's strange. I just added a directory that contains Apalache.tla and Toolbox did not complain about missing files.

nano-o commented 2 years ago

Yes, that works. I'm just saying that when I downloaded the pre-built package it was not obvious where to find Apalache.tla Maybe it's somewhere in the jar file but I didn't think of looking inside the jar. So I was suggesting to include Apalache.tla somewhere obvious in the pre-built package and to make a note in the install instructions to configure the Toolbox's library path.

nano-o commented 2 years ago

This is really not a big deal but might be a point of friction from someone trying Apalache for the first time.

konnov commented 2 years ago

Yes, that works. I'm just saying that when I downloaded the pre-built package it was not obvious where to find Apalache.tla Maybe it's somewhere in the jar file but I didn't think of looking inside the jar. So I was suggesting to include Apalache.tla somewhere obvious in the pre-built package and to make a note in the install instructions to configure the Toolbox's library path.

I see. Yeah, for some reason, this does not work, though we are adding Apalache.tla to tla2sany/StandardModules/ of the jar file. I guess, we have to do it somewhat differently, if we want Toolbox to pick it up. Have to check it with Markus.

shonfeder commented 2 years ago

Given our current packaging and distribution goals and strategy, it might make the most sense just to document where users can find our TLA modules in the source tree and where to put them if they want to use it with TLA+ Toolbox?