Conversation
There was a problem hiding this comment.
Pull Request Overview
This PR adds a health check endpoint to the JSON RPC server to allow external callers to verify that the service is operational.
- Introduces a new
healthmethod that returns a simple "OK" status - Adds comprehensive documentation for the new endpoint
- Includes test coverage for the health check functionality
Reviewed Changes
Copilot reviewed 5 out of 5 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
json-rpc/src/main/scala/com/github/apalachemc/apalache/jsonrpc/ExplorationServiceResult.scala |
Adds HealthCheckResult case class to represent the health check response |
json-rpc/src/main/scala/com/github/apalachemc/apalache/jsonrpc/JsonRpcServer.scala |
Implements the health() method in ExplorationService and adds the method to the JSON-RPC dispatcher |
json-rpc/src/test/scala/com/github/apalachemc/apalache/jsonrpc/TestExplorationService.scala |
Adds test case to verify the health check functionality |
json-rpc/README.md |
Documents the new health check method with input/output examples and curl command |
.unreleased/features/health-check.md |
Adds changelog entry for the new feature |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| @@ -30,6 +30,8 @@ object NextModelStatus { | |||
| val UNKNOWN = "UNKNOWN" | |||
| } | |||
|
|
|||
There was a problem hiding this comment.
The HealthCheckResult case class should have documentation similar to other result classes in this file. Consider adding a ScalaDoc comment that describes the purpose and the status parameter. For example:
/**
* The result of a health check.
* @param status
* the health status, typically "OK"
*/
case class HealthCheckResult(status: String) extends ExplorationServiceResult| /** | |
| * The result of a health check. | |
| * @param status | |
| * the health status, typically "OK" | |
| */ |
thpani
left a comment
There was a problem hiding this comment.
If it always returns "OK", I'd prefer to call it "ping" and return some generic value, but that's probably nitpicking 😄
This is a simple PR, adding a health check method, to help the external callers see, whether the service is up.
make fmt-fix(or had formatting run automatically on all files edited)./unreleased/for any new functionality