1 files changed, 41 insertions, 0 deletions
diff --git a/tools/translate-v8 b/tools/translate-v8
new file mode 100755
index 00000000..7d71bea9
--- /dev/null
+++ b/tools/translate-v8
@@ -0,0 +1,41 @@
+#!/bin/sh
+
+if [ -e v7 ]; then
+  echo "Warning: v7 directory found, the files are maybe already translated";
+  sleep 5;
+fi
+echo --------- Producing v8 files in the translation directory -------------
+if [ -e v8 ]; then rm -r v8; fi
+if [ -e /tmp/v7.$$ ]; then rm -r /tmp/v7.$$; fi
+cp -pr . /tmp/v7.$$
+cp -pr /tmp/v7.$$ v8
+cd v8
+rm description toto
+make clean
+make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
+ { echo ---- Failed to translate; exit 1; }
+echo --------- Upgrading files in the translation directory ----------------
+v8files=`find . -name \*.v8`
+for i in $v8files; do
+  j=`dirname $i`/`basename $i .v8`.v
+  echo Upgrading $j in the translation directory
+  mv -u -f $i $j
+done
+echo --------- Recompiling v8 files in the translation directory -----------
+make clean
+make || { echo ---- Failed to recompile; exit 1; }
+echo --------- Saving v7 files in directory v7 -----------------------------
+/bin/rm -r ../v7
+mv /tmp/v7.$$ ../v7
+echo Saving v7 files done
+echo --------- Upgrading files in current directory ------------------------
+vfiles=`find . -name \*.v`
+cd ..
+for i in $vfiles; do
+  echo Upgrading $i in current directory
+  mv -u -f v8/$i $i
+done
+echo --------- Translation completed ---------------------------------------
+echo Old files are in directory '"v7"'
+echo New files are in current directory
+echo You can now remove the translation directory '"v8"'