Skip to content

Commit

Permalink
Don't run the port binding tests
Browse files Browse the repository at this point in the history
We know this works thanks to local testing, and while it is a nice UX
improvement, it doesn't effect essential functionality enough to
complicate our CI configuration to account for it.
  • Loading branch information
Shon Feder committed Feb 2, 2024
1 parent aa56d62 commit 38d4aff
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions test/tla/cli-integration-tests.md
Original file line number Diff line number Diff line change
Expand Up @@ -4001,7 +4001,12 @@ The Apalache server is running on port 8888. Press Ctrl-C to stop.
### server mode: error is nicely reported when port is already in use
NOTE: These tests are skipped because the would complicate our CI process
more than is warranted by the functionality they test. To enable these tests,
remove the `$MDX skip` annotations.
Start socat in the background to occupy the port, save its pid and wait a second to let binding happen
<!-- $MDX skip -->
```sh
$ socat TCP-L:8888,fork,reuseaddr - & echo $! > pid.pid && sleep 1
```
Expand All @@ -4011,6 +4016,7 @@ redirect its output to the file,
save its exit code,
strip logger prompt
and exit with status code of the server
<!-- $MDX skip -->
```sh
$ apalache-mc server --port=8888 1>out 2>out; ext=$? && cat out | sed -E 's/E@.*$//' && exit $ext
...
Expand All @@ -4019,6 +4025,7 @@ Error while starting Apalache server: Failed to bind to address 0.0.0.0/0.0.0.0:
```
Cleanup: kill socat and delete temporary files
<!-- $MDX skip -->
```sh
$ cat pid.pid | xargs kill -9
$ rm pid.pid out
Expand Down

0 comments on commit 38d4aff

Please sign in to comment.