Manage Apalache server #1115
Manage Apalache server #1115
Conversation
thpani
force-pushed
the
th/manage-shai
branch
4 times, most recently
from
fd5ef83
to
23261e0
Compare
Node.js 18 has been our required version since 9661448. Fixes an issue with octokit not finding a global `fetch()`.
There was a problem hiding this comment.
Great work, because everything works! I had a noodle around with some idioms trying to streamline the Either/async interactions, and the tar extraction.
Most of those suggestions are in the comments here, but I've also open a PR into this draft in case you want to see them all together or merge them in: #1116
quint/src/quintVerifier.ts
Outdated
| // Connection or pinging failed, download Apalache | ||
| console.log("Couldn't connect to Apalache, downloading latest supported release") | ||
| const distDir = await fetchApalache() |
There was a problem hiding this comment.
Does this mean we will hit the github API everytime we need to start shai?
Could we do something like
- Check if there a correct minor version installed in the quint assets, and if so, just start that.
- If it's not there, then query for the versions etc.
Then we could have an update command to update apalache maybe? Or check a timestamp on the dir to see if it past some time frame and prompt for an update?
WDYT?
There was a problem hiding this comment.
Does this mean we will hit the github API everytime we need to start shai?
Yes. Could you articulate what issue you see with that?
It takes an average of 360ms on my machine.
We already have a pathway for performance junkies, which is to launch Shai separately.
So what you suggest may be an incremental improvement, but I'm hesitant to include it as long as we don't know if it's necessary.
There was a problem hiding this comment.
Beyond micro improvements, I have the aesthetic preference of not wanting my CLI tools to depend on hitting external APIs everytime I invoke them, esp when. it'll almost always be a wasted call.
But this also isn't a sticking point for me. We can always follow up here with incremental improvements in behavior and perf.
Co-authored-by: Shon Feder <[email protected]>
Co-authored-by: Shon Feder <[email protected]>
thpani
force-pushed
the
th/manage-shai
branch
2 times, most recently
from
3377f23
to
f9dd4f4
Compare
| ### Added | ||
| ### Changed | ||
|
|
||
| - The `verify` command now manages Apalache server, if no already running | ||
| instance is detected (#1115) | ||
|
|
There was a problem hiding this comment.
This is a feature add, not a breaking change, iiuc?
| ### Added | |
| ### Changed | |
| - The `verify` command now manages Apalache server, if no already running | |
| instance is detected (#1115) | |
| ### Added | |
| - The `verify` command now manages Apalache server, if no already running | |
| instance is detected (#1115) | |
| ### Changed |
There was a problem hiding this comment.
Do we use these categories in a way that diverges from https://keepachangelog.com/?
They simple state
Changedfor changes in existing functionality.
Whether this is a new feature, or modification of an existing one is largely up to interpretation. I'd treat it as a changed feature, as it does not expose additional core functionality. Rather, it improves UX.
There was a problem hiding this comment.
I will merge this PR, since Igor wanted to send install instructions for the summer school.
LMK if I should follow up with an updated changelog.
There was a problem hiding this comment.
Ah. I take "changes for existing functionality" to entail breaking changes. Otherwise, none of the categories entail breaking changes, and I also don't know how you can change existing functionality without that possibly breaking previous expectation about the API. That said, I can see how disagreement of the interpretation here is possible.
Apparently there has been a long-onging debate about this, lol: olivierlacan/keep-a-changelog#41
Perhaps we should add a "Breaking changes" section?
I don't think my view is not widely enough shared to require any change to your entry.
There was a problem hiding this comment.
I see – yeah, it looks like the keepachangelog sections are a bit orthogonal to indicating breaking changes. Incidentally, also Removed may indicate a breaking change, so I guess in this taxonomy breaking changes are scattered across sections.
If we want to list breaking changes, we can either prefix individual items with a qualifier or break them into a separate section, as you suggested.
Manage Apalache server from Quint, as sketched in RFC 008.
I ended up reworking most of the retry logic for obtaining a gRPC connection, which blows up this PR a bit.
Closes #823
Documentation added for any new functionalityCHANGELOG.mdfor any new functionalityFeature table onREADME.mdupdated for any listed functionality