-
Notifications
You must be signed in to change notification settings - Fork 31
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Manage Apalache server #1115
Manage Apalache server #1115
Conversation
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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]>
3377f23
to
f9dd4f4
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks great! Just one Q. and a suggestion in the deps.
### Added | ||
### Changed | ||
|
||
- The `verify` command now manages Apalache server, if no already running | ||
instance is detected (#1115) | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we use these categories in a way that diverges from https://keepachangelog.com/?
They simple state
Changed
for 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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.md
for any new functionalityFeature table onREADME.md
updated for any listed functionality