From a8cb273e9058f29d0b3178dcd00fd1c3b25f5ec6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas.schaertl@fau.de>
Date: Mon, 4 May 2020 14:00:45 +0200
Subject: [PATCH] ulo/scripts: fix prepare scripts

---
 ulo/scripts/isabelle-prepare-directory.sh | 11 ++++++++---
 ulo/scripts/isabelle-prepare-file.sh      |  4 ++--
 ulo/scripts/reset-libraries.sh            |  8 ++++----
 3 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/ulo/scripts/isabelle-prepare-directory.sh b/ulo/scripts/isabelle-prepare-directory.sh
index 9d76e4a..f712f4e 100755
--- a/ulo/scripts/isabelle-prepare-directory.sh
+++ b/ulo/scripts/isabelle-prepare-directory.sh
@@ -15,10 +15,15 @@ if [ ! $# -eq 1 ]; then
     exit 1
 fi
 
-directory="$1"
-threads=6
+directory="$(realpath "$1")"
+threads=8
 
 script_dir=$(dirname "$0")
 cd "$script_dir"
 
-find "$directory" -name "*.rdf.xz" -print0 -exec xargs -0 -P $threads ./isabelle-prepare-file.sh {} \;
+# Recurse in $directory and pass each found item to
+# isabelle-prepare-file.sh. We use xargs(1) to seep this up by
+# exploiting parallelism.
+#
+# We also run it with niceness 15 as to not annoy other CIP users.
+find "$directory" -name "*.rdf.xz" -print0 | nice -n 15 xargs -0 -P $threads -I {} ./isabelle-prepare-file.sh {}
diff --git a/ulo/scripts/isabelle-prepare-file.sh b/ulo/scripts/isabelle-prepare-file.sh
index e778f7e..5b23b9e 100755
--- a/ulo/scripts/isabelle-prepare-file.sh
+++ b/ulo/scripts/isabelle-prepare-file.sh
@@ -11,11 +11,11 @@ if [ ! $# -eq 1 ]; then
     exit 1
 fi
 
+file="$(realpath "$1")"
+
 script_dir=$(dirname "$0")
 cd "$script_dir"
 
-file="$1"
-
 echo "$file" 1>&2
 
 # the filename of the extracted (uncompressed) file
diff --git a/ulo/scripts/reset-libraries.sh b/ulo/scripts/reset-libraries.sh
index 6f5182d..a5da14c 100755
--- a/ulo/scripts/reset-libraries.sh
+++ b/ulo/scripts/reset-libraries.sh
@@ -1,6 +1,6 @@
 #! /bin/sh
 
-# reset git submodules in this directory
+# Reset git submodules in /ulo/libraries directory
 
 set -eu
 
@@ -14,7 +14,7 @@ reset_repo() {
 
 base=$(dirname "$0")
 
-reset_repo "$base"/libraries/coq
-reset_repo "$base"/libraries/isabelle-distribution
-reset_repo "$base"/libraries/isabelle-afp
+reset_repo "$base"/../libraries/coq
+reset_repo "$base"/../libraries/isabelle-distribution
+reset_repo "$base"/../libraries/isabelle-afp
 
-- 
GitLab