Add ADR008: Obtaining and Launching Apalache

[thpani]

This RFC discusses the problem space and proposes a solution for obtaining and launching Apalache, in support of the quint verify command.

I would like to receive feedback on the current proposal before expanding it further.

Towards #823, closes #701

[Kukovec]

I think this aptly covers most reasonable options, and I personally agree with the "Proposed Solution" part, i.e. I prefer avoiding package managers when GH will do. Obviously, the version stuff is TBD, so I can't really comment on it. I'll just make a note here for future reference to discuss the scenario when Apalache is both present, and outdated, in the sense that it might not be a bad idea for the Quint plugin to notify the user that a newer version of Apalache is available, even if it's technically not "necessary" for feature support (and either DL it, or have them update manually).

[bugarela]

Looks very good. I was feeling very pessimistic while reading the options, but at the end you found a really good solution 🎉

[konnov]

Looks good! The solution provides us with a good balance between simple behaviour by default and manual setup, if needed

[thpani]

I've added a section with options for managing the Apalache version from Quint.

Personally, I'm torn between 3.3.2 and 3.3.4, but maybe one of you has better ideas.
@konnov @bugarela @Kukovec

[shonfeder]

Great writeup!

[shonfeder]

Could we name the RFCs sequentially starting with #1062?

Using the same numbering for RFCs and ADRs isn't helpful, ime, since they (should) serve pretty different purposes!

Suggested change

	# RFC008: Obtaining and Launching Apalache from Quint
	# RFC001: Obtaining and Launching Apalache from Quint

[shonfeder]

Unless this is actually an ADR? Is seems like it may be.

And what is the difference? I guess maybe more thought is needed here 😅

[thpani]

I think this has evolved into an ADR. I will revamp it a bit, to record the discussions on this PR.

There is an advantage though in sharing a single counter between RFCs and ADRs: for RFCs that grow up to be an ADR, both documents will share the same index, and their correspondence is easily identifiable.

[shonfeder]

I don't think I agree with the premise that ADRs are an evolutionary stage of RFCs 😅 IMO, they call for quite different scope and content.

But this is part of a larger process discussion that doesn't effect this PR. I think this is an ADR 👍

[konnov]

I know we have been discussing that multiple times. I also think that RFCs and ADRs are related. This may be as simple as a usability problem: When looking for RFCs or ADRs, one may see gaps in numbering. If we consider the (unique) document number to be the most important attribute, then we could call documents like 002rfc and 003adr, meaning that "rfc" and "adr" are just tags of the envisioned document content.

[shonfeder]

They can be related, sure. But that doesn't mean ADRs are "evolved" RFC. IMO, reading on the intent and traditions around either makes it immediately clear that they have been and should be distinct documents, with different content and purposes. See, for instance:

• https://news.ycombinator.com/item?id=26057068
• https://engineering.atspotify.com/2020/04/when-should-i-write-an-architecture-decision-record/
• https://medium.com/@klaus.haeuptle/shaping-architecture-decisions-from-request-for-comments-rfc-to-documenting-architecture-11dad9877342

If we consider the (unique) document number to be the most important attribute

Why would we consider this? The document number is essentially arbitrary afaik. "the envisioned document content" seems much more important than the order in which documents were drafted imo.

[thpani]

I believe we have some misunderstanding here.
Nobody contested that RFC and ADR (if both present) should be distinct documents, or that they serve different purposes.
At the same time, I find it only economical to reuse and/or evolve – if applicable – those (large!) parts of these documents that serve the same purpose, i.e., communicating context and options.

But this discussion is unrelated to the technical contents of this PR. If you believe this should be addressed, I would propose to take it up in a separate issue or GH discussion.

[shonfeder]

Since this is a 2sec delay on every invocation of the verify command, I think it's not necessarily negligible?

[thpani]

Relative to usual Apalache runtime, I think it is?

[bugarela]

I guess if it was really negligible, then there would be no reason for us to consider managing the server in any scenario. Perhaps

Suggested change

	server vs. JVM startup time for an on-demand approach; at the time of writing,
	a freshly launched `apalache-mc server` takes ~125MB of memory, while JVM
	startup time is negligable (< 2sec).
	server vs. JVM startup time for an on-demand approach; at the time of writing,
	a freshly launched `apalache-mc server` takes ~125MB of memory, while JVM
	startup time is negligible for most runs (< 2sec).

One example scenario where this is not negligible may be running the apalache simulator with a few runs to iterate over something (once we have a command for that)

[thpani]

then there would be no reason for us to consider managing the server in any scenario

ergonomics, I think

running the apalache simulator with a few runs to iterate over something

I think what you describe here is still a single invocation of the simulate command in Apalache? Otherwise, we'd probably want the more fine-grained interface described in Apalache RFC-010?

[shonfeder]

If you are running 10-step checks while developing a small spec, that 2 sec startup per invocation can easily be your biggest bottleneck, in my limited experience.

I distinctly note the snappier response when running with a server in the background.

[konnov]

It looks to me that there are two main user stories here:

1. A first time user tries to run quint verify. They want to try the command and definitely do not want to manage the server (they probably even do not know what it means).
2. An experienced user runs quint verify periodically. They would prefer to have (one instance of) the server in the background.

At this point of development, I would prioritise the first-time user over the experienced user. However, we should give the experienced user an option to optimize their workflow by running the server in the background. As far as I understand, there is such an option.

[shonfeder]

An option not discussed here afaict is tying apalache's lifetime to the quint processes lifetime, e.g., by:

• Having an interactive terminal session for checking specs, akin to sbt
• Managing the server from the vs-code extension.

I think these can be postponed as possibly later feature, but the should be noted here for consideration.

[thpani]

I really meant this to apply regardless of how verification is invoked. Could be the CLI, VSCode, or another frontend. I think discussing front-end options is orthogonal to this document, since all of them need to somehow spawn and connect to a Shai instance, and ideally this ADR should provide a transparent solution for all of them.

This also came up in @bugarela's review, I will revise this paragraph to be less ambiguous.

[thpani]

I've updated §§ 3.2.4 and 4 of this doc to match our main branch wrt to pinning a Quint version.

Please take another look!

[bugarela]

Looks great! Thanks for taking such good care of this ✨

[shonfeder]

Looks great!

Just a few notes and incidental suggestions from me