summaryrefslogtreecommitdiff
path: root/tools/check-v8
diff options
context:
space:
mode:
Diffstat (limited to 'tools/check-v8')
-rwxr-xr-xtools/check-v824
1 files changed, 24 insertions, 0 deletions
diff --git a/tools/check-v8 b/tools/check-v8
new file mode 100755
index 00000000..9dfa0be3
--- /dev/null
+++ b/tools/check-v8
@@ -0,0 +1,24 @@
+#!/bin/sh
+
+echo ------------------ Producing v8 files -------------------------
+if [ -e v8 ]; then rm -r v8; fi
+if [ -e /tmp/v8.$$ ]; then rm -r /tmp/v8.$$; fi
+cp -pr . /tmp/v8.$$
+mv /tmp/v8.$$ v8
+cd v8
+rm description
+make clean
+make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
+ { echo ---- Failed to translate; exit 1; }
+echo ------------------ Upgrading v8 files -------------------------
+v8files=`find . -name \*.v8`
+for i in $v8files; do
+ j=`dirname $i`/`basename $i .v8`.v
+ echo Upgrading $i
+ mv -u -f $i $j
+done
+echo ------------------ Recompiling v8 files -----------------------
+make clean
+make || { echo ---- Failed to recompile; exit 1; }
+make clean # to save disk space
+echo ------------------ Translation completed ----------------------