Merge pull request #145 from freespek/th/fix-apalache-path

Fix Apalache path

solarkraft/.devcontainer/Dockerfile

@@ -1,4 +1,4 @@
 # Force platform to linux/amd64; there is no Z3 release for linux/arm64:
 # https://github.com/Z3Prover/z3/issues/7201
 FROM --platform=linux/amd64 mcr.microsoft.com/devcontainers/typescript-node:20-bookworm
-ENV PATH="/opt/apalache/bin/:${PATH}"
+ENV PATH="/opt/apalache/bin:${PATH}"

solarkraft/src/verify.ts

@@ -30,12 +30,10 @@ import { JSONbig, Result } from './globals.js'
 
 type ApalacheResult = Result<void>
 
-// Looks for the Apalache path under $APALACHE_HOME. If undefined, uses /opt/apalache
-const APALACHE_DIST =
-    typeof process.env.APALACHE_HOME === 'undefined'
-        ? '/opt/apalache'
-        : process.env.APALACHE_HOME
-const APALACHE_BIN = path.join(APALACHE_DIST, 'bin', 'apalache-mc')
+// Look for Apalache under $APALACHE_HOME/bin/. If undefined, assumes that `apalache-mc` is in $PATH.
+const APALACHE_BIN = process.env.APALACHE_HOME
+    ? path.join(process.env.APALACHE_HOME, 'bin', 'apalache-mc')
+    : 'apalache-mc'
 
 /**
  * Parse the TLA+ file at `monitorTlaPath` and return its JSON IR.
@@ -55,7 +53,7 @@ function getApalacheJsonIr(monitorTlaPath: string): Result<string> {
     // Check for `typecheck` errors
     if (apalacheParse.status != 0) {
         return left(
-            `Parsing monitor file ${monitorTlaPath} failed:\n${apalacheParse.stderr}`
+            `Parsing monitor file ${monitorTlaPath} failed:\n${apalacheParse.error ?? apalacheParse.stderr}`
         )
     }