diff options
author | Jason Gross <jgross@mit.edu> | 2016-02-23 16:18:41 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-02-23 16:20:01 -0500 |
commit | f2dc40687111f23af0c5c0efa48399253e8d34fa (patch) | |
tree | 953e8c391ef452dcde3c94a3c0b56bc998f9b5b0 /etc | |
parent | a46dbbec5fc2cd3ffc5c6d4be751e42aa2b7cafb (diff) |
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.
Diffstat (limited to 'etc')
-rwxr-xr-x | etc/freshen-bedrock-files.sh | 52 |
1 files changed, 52 insertions, 0 deletions
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 |