From f2dc40687111f23af0c5c0efa48399253e8d34fa Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 23 Feb 2016 16:18:41 -0500
Subject: Add etc/freshen-bedrock-files.sh

It is used on smithers to remove .vo files which are older than relevant
Bedrock .vo files.  This prevents version mismatches when updating Bedrock on
smithers.
---
 etc/freshen-bedrock-files.sh | 52 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100755 etc/freshen-bedrock-files.sh

(limited to 'etc')

diff --git a/etc/freshen-bedrock-files.sh b/etc/freshen-bedrock-files.sh
new file mode 100755
index 000000000..08e0435d7
--- /dev/null
+++ b/etc/freshen-bedrock-files.sh
@@ -0,0 +1,52 @@
+#!/usr/bin/env bash
+
+MYDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+pushd "$MYDIR" 1>/dev/null
+
+ROOT_DIR="$(git rev-parse --show-toplevel)"
+cd "$ROOT_DIR"
+
+FILES="$(git grep --name-only "Bedrock\.")"
+
+COQLIB="$(${COQBIN}coqc -config | grep 'COQLIB=' | sed s'/^COQLIB=//g')"
+
+MYCOQPATH="$COQPATH${COQPATH:+:}$COQLIB"
+
+echo "My COQPATH is $MYCOQPATH"
+
+for VFILE in $FILES; do
+  if [ ! -e "$VFILE" ]; then
+    echo "Could not find $VFILE"
+    continue
+  elif [ ! -e "${VFILE}o" ]; then
+    echo "Already going to rebuild ${VFILE}o"
+    continue
+  fi
+
+  VOFILES="$(grep -o "Bedrock\.[^ ]*" "$VFILE" | sed s'/\.$//g' | sed s'|\.|/|g' | sed s'/$/.vo/g' | sort | uniq)"
+  for VOFILE in $VOFILES; do
+    if [ ! -e "${VFILE}o" ]; then # we already got rid of it
+      break
+    fi
+    FOUND=""
+  ( IFS=:
+    for DIR in $MYCOQPATH; do
+      if [ -e "$DIR/$VOFILE" ]; then
+        FOUND=1
+        if [ "$DIR/$VOFILE" -nt "${VFILE}o" ]; then
+          echo "Now going to rebuild ${VFILE}o; $DIR/$VOFILE is newer"
+          rm -f "${VFILE}o"
+        else
+          echo "Not necessarily rebuilding ${VFILE}o; $DIR/$VOFILE is older"
+        fi
+        break
+      fi
+    done
+  )
+    if [ -z "$FOUND" ]; then
+      echo "WARNING: Could not find $VOFILE, which $VFILE depends on"
+    fi
+  done
+done
+
+popd 1>/dev/null
-- 
cgit v1.2.3