isabelle: don't use /tmp as a temp directory
Isabelle uses `/tmp` no matter what on Unix platforms, apparently because using an arbitrary `$TMPDIR` can cause "path too long" errors on macOS (https://isabelle.in.tum.de/repos/isabelle/rev/ff92d6edff2c). However, when not using the sandbox (i.e. on Darwin), this causes the build to fail if its temp directory (`/tmp/isabelle-`) has already been created by a previous build using a different build user. For example, this is the cause of https://hydra.nixos.org/build/321069301. So, this PR changes it to use `$TMPDIR` during the build of Isabelle itself (but still use `/tmp` when using Isabelle normally). I had initially hoped this would also enable Isabelle to build within the Darwin sandbox, but something else seems to be wrong (I get an opaque `I/O error: Operation not permitted`).
This commit is contained in:
@@ -31,9 +31,14 @@ stdenv.mkDerivation rec {
|
||||
|
||||
installPhase = ''
|
||||
mkdir -pv "$out"
|
||||
export HOME="$out"
|
||||
export HOME="$TMPDIR"
|
||||
export PATH=$out/bin:$PATH
|
||||
|
||||
# Stop Isabelle trying to use `/tmp`.
|
||||
user_home="$(isabelle getenv -b ISABELLE_HOME_USER)"
|
||||
mkdir -p "$user_home/etc"
|
||||
echo 'ISABELLE_TMP_PREFIX="$TMPDIR/isabelle"' > "$user_home/etc/settings"
|
||||
|
||||
pushd zenon
|
||||
./configure --prefix $out
|
||||
make
|
||||
|
||||
@@ -266,6 +266,11 @@ stdenv.mkDerivation (finalAttrs: {
|
||||
export HOME=$TMP # The build fails if home is not set
|
||||
setup_name=$(basename contrib/isabelle_setup*)
|
||||
|
||||
# Stop Isabelle trying to use `/tmp`.
|
||||
user_home="$(bin/isabelle getenv -b ISABELLE_HOME_USER)"
|
||||
mkdir -p "$user_home/etc"
|
||||
echo 'ISABELLE_TMP_PREFIX="$TMPDIR/isabelle"' > "$user_home/etc/settings"
|
||||
|
||||
#The following is adapted from https://isabelle.sketis.net/repos/isabelle/file/Isabelle2021-1/Admin/lib/Tools/build_setup
|
||||
TARGET_DIR="contrib/$setup_name/lib"
|
||||
rm -rf "$TARGET_DIR"
|
||||
|
||||
Reference in New Issue
Block a user