Merge pull request #1115 from informalsystems/th/manage-shai

Manage Apalache server
informalsystems · Aug 25, 2023 · fbda4d5 · fbda4d5
2 parents dd22552 + c58464f
commit fbda4d5
Show file tree

Hide file tree

Showing 6 changed files with 571 additions and 210 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -25,7 +25,7 @@ jobs:
       - uses: actions/checkout@v2
       - uses: actions/setup-node@v2
         with:
-          node-version: "17"
+          node-version: "18"
       - run: npm install
       - run: npm run format-check || (echo "Run 'npm run format'" && exit 1)
 
@@ -40,7 +40,7 @@ jobs:
       - uses: actions/checkout@v2
       - uses: actions/setup-node@v2
         with:
-          node-version: "17"
+          node-version: "18"
       - run: npm install
       - run: npm run format-check || (echo "Run 'npm run format'" && exit 1)
 
@@ -57,7 +57,7 @@ jobs:
       - uses: actions/checkout@v2
       - uses: actions/setup-node@v2
         with:
-          node-version: "17"
+          node-version: "18"
       - run: npm install
       - run: npm run compile
       - run: npm test
@@ -73,7 +73,7 @@ jobs:
       - uses: actions/checkout@v2
       - uses: actions/setup-node@v2
         with:
-          node-version: "17"
+          node-version: "18"
       - run: npm install
       - name: Compile and update test fixtures
         run: npm run generate
@@ -92,7 +92,7 @@ jobs:
       - uses: actions/checkout@v2
       - uses: actions/setup-node@v2
         with:
-          node-version: "17"
+          node-version: "18"
       - run: cd ./quint && npm ci
       - run: cd ./quint && npm run compile && npm link
       - name: Ensure all dependencies are specified
@@ -139,7 +139,7 @@ jobs:
       - uses: actions/checkout@v2
       - uses: actions/setup-node@v2
         with:
-          node-version: "17"
+          node-version: "18"
       - run: cd ./quint && npm ci
       - run: cd ./quint && npm run compile && npm link
       - name: Ensure all dependencies are specified
@@ -176,7 +176,7 @@ jobs:
       - uses: actions/checkout@v2
       - uses: actions/setup-node@v2
         with:
-          node-version: "17"
+          node-version: "18"
       - run: cd ./quint && npm install
       - run: cd ./quint && npm run antlr
 
@@ -190,7 +190,7 @@ jobs:
       - uses: actions/checkout@v2
       - uses: actions/setup-node@v2
         with:
-          node-version: "17"
+          node-version: "18"
       - name: Install quint deps
         run: cd ./quint && npm install
       - name: Install yalc

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -9,6 +9,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 ### Changed
+
+- The `verify` command now manages Apalache server, if no already running
+  instance is detected (#1115)
+
 ### Deprecated
 ### Removed
 ### Fixed

diff --git a/quint/apalache-dist-tests.md b/quint/apalache-dist-tests.md
@@ -4,96 +4,37 @@
 bash -
 -->
 
-These tests check for error handling around misconfiguration or corruption of
-the apalache distribution. They are in a separate file from `apalache-test.md`
-since they presuppose a broken environment, whereas the apalache integration
-tests assume a working environment.
+These tests check management of the Apalache server from Quint.
+They are in a separate file from `apalache-test.md` since they presuppose an
+environment in which Apalache server has not been started.
 
+### Inability to connect to the server downloads Apalache
 
-### Problems with the Apalache distribution
+There is no Apalache server running. This will try to load the proto file
+dynamically, using gRPC reflection, recognize that the server is not available,
+fetch a tagged Apalache release and spawn a server in the background.
 
-#### Setting a Non-existent `APALACHE_HOME` produces an error
+The second time we call Apalache, we already have an up-to-date Apalache
+distribution on-disk. Quint re-uses this distribution and does not download
+again.
 
-<!-- !test in invalid APALACHE_DIST -->
-```
-APALACHE_DIST=/does/not/exist quint verify ../examples/language-features/booleans.qnt
-```
-
-<!-- !test exit 1 -->
-<!-- !test err invalid APALACHE_DIST -->
-```
-error: Specified APALACHE_DIST /does/not/exist does not exist.
-```
-
-#### Setting a corrupted `APALACHE_DIST` produces an error
-
-(The `_build` dir exists, but doesn't have the expected structure of the
-Apalache distribution.)
-
-<!-- !test in corrupted APALACHE_DIST -->
-```
-APALACHE_DIST=_build quint verify ../examples/language-features/booleans.qnt 2> >(sed "s:$PWD/::g" >&2)
-```
-
-<!-- !test exit 1 -->
-<!-- !test err corrupted APALACHE_DIST -->
-```
-error: Apalache distribution is corrupted: cannot find _build/lib/apalache.jar. Ensure the APALACHE_DIST environment variable points to the right directory.
-```
-
-#### Extracting the proto file from a corrupted jar file produces an error
-
-We set up a valid looking distribution, but with an invalid jar file.
-
-<!-- !test in corrupted apalache.jar -->
-```
-mkdir -p _build/corrupt-dist-test/lib && touch _build/corrupt-dist-test/lib/apalache.jar
-mkdir -p _build/corrupt-dist-test/bin && touch _build/corrupt-dist-test/bin/apalache-mc
-APALACHE_DIST=_build/corrupt-dist-test quint verify ../examples/language-features/booleans.qnt 2> >(sed "s:$PWD/::g" >&2)
-```
-
-<!-- !test exit 1 -->
-<!-- !test err corrupted apalache.jar -->
-```
-error: Apalache distribution is corrupted. Could not extract proto file from apalache.jar.
-```
-
-### Inability to connect to the server produces an errer (`APALACHE_DIST` unset)
-
-We now do not set `APALACHE_DIST`, which will try to load the proto file
-dynamically, using gRPC reflection, but expect that the server is not already
-running.
 
 <!-- !test in server not running -->
 ```
-quint verify ../examples/language-features/booleans.qnt
-```
-
-<!-- !test exit 1 -->
-<!-- !test err server not running -->
-```
-error: Failed to obtain a connection to Apalache after 5 seconds.
-```
-
-### Inability to connect to the server produces an errer (`APALACHE_DIST` set)
-
-We now assume a correctly configured installation of Apalache in
-`APALACHE_DIST`, but expect that the server is not already running.
-
-See https://github.com/informalsystems/quint/issues/823 for plans to manage the
-server, making this error case all but impossible.
-
-<!-- !test program
-APALACHE_DIST=_build/apalache PATH=_build/apalache/bin:$PATH bash -
--->
-
-<!-- !test in sever errors and connections -->
-```
-quint verify ../examples/language-features/booleans.qnt
+quint verify ../examples/language-features/booleans.qnt | \
+  sed 's!https://.*!(asseturl)!'
+quint verify ../examples/language-features/booleans.qnt | \
+  sed 's!\(Using existing Apalache distribution in \).*!\1(distdir)!'
 ```
 
-<!-- !test exit 1 -->
-<!-- !test err sever errors and connections  -->
+<!-- !test out server not running -->
 ```
-error: Failed to obtain a connection to Apalache after 5 seconds.
+Couldn't connect to Apalache, checking for latest supported release
+Downloading Apalache distribution from (asseturl)
+Launching Apalache server
+Shutting down Apalache server
+Couldn't connect to Apalache, checking for latest supported release
+Using existing Apalache distribution in (distdir)
+Launching Apalache server
+Shutting down Apalache server
 ```