Fix concurrent downloads of the Apalache distribution

CHANGELOG.md

@@ -20,6 +20,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Removed
 ### Fixed
 
+- Fixed concurrent `quint verify` runs failing with "Could not find or load main class tlc2.TLC" while another run was still downloading the Apalache distribution. The distribution is now unpacked in a temporary directory and moved into place once complete
 - Fixed `and`, `or`, `implies` and `iff` being accepted to combine assignments in actions (e.g. `x > 0 and x' = 1`), a regression in v0.32.0. Use `all { ... }` and `any { ... }` in actions, as documented. In temporal definitions, they can combine actions and temporal formulas, e.g. `init and always(step.orKeep(vars))`
 - Fixed flattening of qualified imports (`import A as C`) when an imported name starts with the qualifier, e.g. `Credits` with `C`, which failed with "Name 'C::Credits' not found"
 - `mustChange` (`<<A>>_v` in TLA+) is now correctly printed in the TLA+ output, so it can be checked with `--backend tlc`. Quint now post-processes the TLA+ produced by Apalache to fix issues in its pretty printer

quint/src/apalache.ts

@@ -389,18 +389,39 @@ async function tryConnect(serverEndpoint: ServerEndpoint, retry: boolean = false
     .map(apalache)
 }
 
-function downloadAndUnpackApalache(apalacheVersion: string): Promise<ApalacheResult<null>> {
+async function downloadAndUnpackApalache(apalacheVersion: string): Promise<ApalacheResult<null>> {
   const url = `https://github.com/apalache-mc/apalache/releases/download/v${apalacheVersion}/apalache.tgz`
-  return fetch(url)
-    .then(
-      // unpack response body
-      res => pipeline(res.body!, tar.extract({ cwd: apalacheDistDir(apalacheVersion), strict: true })),
-      error => err(`Error fetching ${url}: ${error}`)
-    )
-    .then(
-      _ => right(null),
-      error => err(`Error unpacking .tgz: ${error}`)
-    )
+  const distDir = apalacheDistDir(apalacheVersion)
+  // Unpack into a temporary directory and then move it into place, so that other quint processes (e.g., running
+  // in parallel) never see a partially unpacked distribution, which would make them fail to load Apalache or TLC.
+  const tmpDir = fs.mkdtempSync(path.join(distDir, 'download-'))
+  try {
+    let res: Response
+    try {
+      res = await fetch(url)
+    } catch (error) {
+      return err(`Error fetching ${url}: ${error}`)
+    }
+
+    try {
+      await pipeline(res.body!, tar.extract({ cwd: tmpDir, strict: true }))
+    } catch (error) {
+      return err(`Error unpacking .tgz: ${error}`)
+    }
+
+    try {
+      fs.renameSync(path.join(tmpDir, 'apalache'), path.join(distDir, 'apalache'))
+    } catch (error) {
+      // Another process may have moved its complete distribution into place in the meantime, then we use that one
+      if (!fs.existsSync(path.join(distDir, 'apalache'))) {
+        return err(`Error installing the Apalache distribution in ${distDir}: ${error}`)
+      }
+    }
+
+    return right(null)
+  } finally {
+    fs.rmSync(tmpDir, { recursive: true, force: true })
+  }
 }
 
 /**