From 1c67973b19bfc0a1368756fbb2ad5443a2c47a38 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 13 Dec 2024 17:16:23 +0100
Subject: [PATCH 1/6] protect against SANY race conditions on the filesystem

---
 src/universal/bin/apalache-mc | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/universal/bin/apalache-mc b/src/universal/bin/apalache-mc
index 45b2f28f73..5689e8028f 100755
--- a/src/universal/bin/apalache-mc
+++ b/src/universal/bin/apalache-mc
@@ -38,6 +38,10 @@ then
     JVM_ARGS="${JVM_ARGS} -Xmx4096m"
 fi
 
+# Avoid SANY concurrency issues: https://github.com/tlaplus/tlaplus/issues/688
+TD=`mktemp -d "$TMPDIR"/SANYXXXXXXXXXX`
+JVM_ARGS="${JVM_ARGS} -Djava.io.tmpdir=$TD"
+
 # Check whether the CLI args contains the debug flag
 if [[ "$*" =~ '--debug' ]]
 then

From d4cd6e147865cc1ed881e48374ff1e8b2e2449cc Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 13 Dec 2024 17:30:18 +0100
Subject: [PATCH 2/6] add release notes

---
 .unreleased/bug-fixes/sany-tmpdir.md | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 .unreleased/bug-fixes/sany-tmpdir.md

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

From ce176b022a83df5e20c86d435adf98559de84ee2 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 13 Dec 2024 17:48:58 +0100
Subject: [PATCH 3/6] handle TMPDIR for docker

---
 src/universal/bin/apalache-mc | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/universal/bin/apalache-mc b/src/universal/bin/apalache-mc
index 5689e8028f..d75083b0cf 100755
--- a/src/universal/bin/apalache-mc
+++ b/src/universal/bin/apalache-mc
@@ -39,7 +39,11 @@ then
 fi
 
 # Avoid SANY concurrency issues: https://github.com/tlaplus/tlaplus/issues/688
-TD=`mktemp -d "$TMPDIR"/SANYXXXXXXXXXX`
+if [ -z "$TMPDIR" ]; then
+    TMPDIR="$(pwd)/tmp"
+    mkdir -p "$TMPDIR"
+fi
+TD=`mktemp -d -p $TMPDIR -t SANYXXXXXXXXXX`
 JVM_ARGS="${JVM_ARGS} -Djava.io.tmpdir=$TD"
 
 # Check whether the CLI args contains the debug flag

From c30a20df18dffde6411e70e85aa4ff6b14a4fb4a Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 13 Dec 2024 17:55:16 +0100
Subject: [PATCH 4/6] refactor a bit to avoid fuzzy output in the integration
 tests

---
 src/universal/bin/apalache-mc | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/universal/bin/apalache-mc b/src/universal/bin/apalache-mc
index d75083b0cf..0bf1985b99 100755
--- a/src/universal/bin/apalache-mc
+++ b/src/universal/bin/apalache-mc
@@ -43,8 +43,7 @@ if [ -z "$TMPDIR" ]; then
     TMPDIR="$(pwd)/tmp"
     mkdir -p "$TMPDIR"
 fi
-TD=`mktemp -d -p $TMPDIR -t SANYXXXXXXXXXX`
-JVM_ARGS="${JVM_ARGS} -Djava.io.tmpdir=$TD"
+JAVA_IO_TMPDIR=`mktemp -d -p $TMPDIR -t SANYXXXXXXXXXX`
 
 # Check whether the CLI args contains the debug flag
 if [[ "$*" =~ '--debug' ]]
@@ -52,10 +51,11 @@ 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" "$@"

From f73b53136a81420ef4de1cac0c462017c9f9759c Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 13 Dec 2024 18:35:31 +0100
Subject: [PATCH 5/6] fix an error on empty TMPDIR

---
 src/universal/bin/apalache-mc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/universal/bin/apalache-mc b/src/universal/bin/apalache-mc
index 0bf1985b99..e530d42661 100755
--- a/src/universal/bin/apalache-mc
+++ b/src/universal/bin/apalache-mc
@@ -39,7 +39,7 @@ then
 fi
 
 # Avoid SANY concurrency issues: https://github.com/tlaplus/tlaplus/issues/688
-if [ -z "$TMPDIR" ]; then
+if [ -z "${TMPDIR:-}" ]; then
     TMPDIR="$(pwd)/tmp"
     mkdir -p "$TMPDIR"
 fi

From 4e6279d749abbd5a47f99b8488f1abe5c5a92197 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 13 Dec 2024 18:58:36 +0100
Subject: [PATCH 6/6] try it without -p

---
 src/universal/bin/apalache-mc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/universal/bin/apalache-mc b/src/universal/bin/apalache-mc
index e530d42661..e9e5dfc32f 100755
--- a/src/universal/bin/apalache-mc
+++ b/src/universal/bin/apalache-mc
@@ -43,7 +43,7 @@ if [ -z "${TMPDIR:-}" ]; then
     TMPDIR="$(pwd)/tmp"
     mkdir -p "$TMPDIR"
 fi
-JAVA_IO_TMPDIR=`mktemp -d -p $TMPDIR -t SANYXXXXXXXXXX`
+JAVA_IO_TMPDIR=`mktemp -d -t SANYXXXXXXXXXX`
 
 # Check whether the CLI args contains the debug flag
 if [[ "$*" =~ '--debug' ]]