diff --git a/.unreleased/bug-fixes/sany-tmpdir.md b/.unreleased/bug-fixes/sany-tmpdir.md new file mode 100644 index 0000000000..8cce6d77c8 --- /dev/null +++ b/.unreleased/bug-fixes/sany-tmpdir.md @@ -0,0 +1 @@ +Add extra protection against the SANY race conditions on the filesystem, see #3046 diff --git a/src/universal/bin/apalache-mc b/src/universal/bin/apalache-mc index 45b2f28f73..e9e5dfc32f 100755 --- a/src/universal/bin/apalache-mc +++ b/src/universal/bin/apalache-mc @@ -38,16 +38,24 @@ then JVM_ARGS="${JVM_ARGS} -Xmx4096m" fi +# Avoid SANY concurrency issues: https://github.com/tlaplus/tlaplus/issues/688 +if [ -z "${TMPDIR:-}" ]; then + TMPDIR="$(pwd)/tmp" + mkdir -p "$TMPDIR" +fi +JAVA_IO_TMPDIR=`mktemp -d -t SANYXXXXXXXXXX` + # Check whether the CLI args contains the debug flag if [[ "$*" =~ '--debug' ]] then echo "# Tool home: $DIR" echo "# Package: $APALACHE_JAR" echo "# JVM args: $JVM_ARGS" + echo "# -Djava.io.tmpdir: $JAVA_IO_TMPDIR" echo "#" fi # Run with `exec` to replace the PID, rather than running in a subshell. # This saves one process, and ensures signals are sent to the replacement process # C.f. https://github.com/sbt/sbt-native-packager/blob/e72f2f45b8cab5881add1cd62743bfc69c2b9b4d/src/main/resources/com/typesafe/sbt/packager/archetypes/scripts/bash-template#L141-L142 -exec java $JVM_ARGS -jar "$APALACHE_JAR" "$@" +exec java $JVM_ARGS -Djava.io.tmpdir=$JAVA_IO_TMPDIR -jar "$APALACHE_JAR" "$@"